Publications and Presentations

Pei-Hsin Ho

Physical Implementation of VLSI designs

• On Improving Optimization Effectiveness in Interconnect-Driven Physical Synthesis, in Proceedings of ISPD 2009. Co-authored with P. Saxena, V. Khandelwal, C. Qiao, J.-C. Lin and M. Iyer.

• Automatic Register Banking for Low-Power Clock Trees, in Proceedings of ISQED 2009. Co-authored with W. Hou.

• Future of Low Power, SNUG Europe Tutorial; SNUG Taiwan Keynote; SNUG India Keynote, 2008. Ppt slides (Synopsys SolvNet access required).

• Techniques for effective distributed physical synthesis, in Proceedings of DAC 2007. Co-authored with F. Y.C. Mang and W. Hou. Pdf.

• Power-aware placement, in Proceedings of DAC 2005. Co-authored with Y. Cheon, A.B. Kahng, S. Reda and Q. Wang. Pdf.

Formal Verification of VLSI designs

• Intelligent random vector generator based on probability analysis of circuit structure, in Proceedings of ISQED 2007. Co-authored with Y. Kuo, C. Lin, C. Wang and S. Chang. Pdf.

• Supporting sequential assumptions in hybrid verification, in Proceedings of ASPDAC 2005. Co-authored with E. Cerny, A. Dsouza, K. Harer and T. Ma. Pdf.

• Abstraction Refinement, ATVA 2004 Keynote. Abstract in Proceedings of ATVA 2004, Lecture Notes in Computer Science 3299, Springer-Verlag, 2004, pp. 7. Pdf.

• Abstraction refinement by controllability and cooperativeness analysis, in Proceedings of DAC 2004. Co-authored with F. Mang. Pdf.

• Recent advances in formal verification, ICCAD2003 Tutorial. Co-presented with K. McMillan and V. Sighal. Pdf slides.

• Formal property verification by abstraction refinement with formal, simulation and hybrid engines, in Proceedings of DAC 2001. Co-authored with D. Wang, J. Long, J. Kukula, Y. Zhu, T. Ma and R. Damiano. Pdf.

• Smart simulation using collaborative formal and simulation Engines, in Proceedings of ICCAD 2000. Co-authored with T. Shiple, K. Harer, J. Kukula, R. Damiano, V. Bertacco, J. Taylor and J. Long. Pdf.

• Coverage estimation for symbolic modle checking, in Proceedings of DAC 1999 (Best Paper Award), pp. 300-305. Co-authored with Y. Hoskote, T. Kam and X. Zhao. Pdf.

• Formal verification of pipeline control using token semantics and data abstraction, in Proceedings of ICCAD 1998. pp. 529-536. Co-authored with A. Isles and T. Kam. Pdf.

• Verification of a complete floating-point unit using word-level model checking, in Proceedings of FMCAD 1996, Lecture Notes in Computer Science 1166, Springer-Verlag, 1996, pp. 19-33. Co-authored with Y-A. Chen, E. Clarke, Y. Hoskote, T. Kam, M. Khaira, J. O'Leary and X. Zhao. Postscript.

Formal Verification of Hybrid Systems

• Algorithmic Analysis of Nonlinear Hybrid Systems, in IEEE Transactions on Automatic Control, Vol.43, No.4, pp. 540--554, 1998. A preliminary version appeared in Proceedings of the Conference on Computer-Aided Verification (CAV95), Lecture Notes in Computer Science 939, Springer-Verlag, 1995, pp. 225-238. Co-authored with T.A. Henzinger and H. Wong-Toi. Html.

• HyTech, A Model Checker for Hybrid Systems, in Software Tools for Technology Transfer, Vol.1, No.1, pp. 110-122, 1998. A preliminary version appeared in Proceedings of the Conference on Computer-Aided Verification (CAV97), Lecture Notes in Computer Science 1254, Springer-Verlag, 1997, pp. 460-464. Co-authored with T.A. Henzinger and H. Wong-Toi. Html.

• Automatic Symbolic Verification of Embedded Systems, in IEEE Transactions on Software Engineering, Vol. 22, No.3, 1996, pp 181--201. A preliminary version appeared in Proceedings of the 14th Annual IEEE Real-time Systems Symposium (RTSS93), 1993. Co-authored with R. Alur and T.A. Henzinger. Html.

• The Algorithmic Analysis of Hybrid Systems, in Theoretical Computer Science, Vol. 138, 1995, pp 3--34. A preliminary version appeared in Proceedings of the 11th International Conference on Analysis and Optimization of Systems: Discrete-event Systems, Lecture Notes in Control and Information Sciences 199, Springer-Verlag, 1994, pp. 331-351. Co-authored with R. Alur, C. Courcoubetis, T.A. Henzinger, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine. Html.

• Automated analysis of an audio control protocol, in Proceedings of the Conference on Computer-Aided Verification (CAV95), Lecture Notes in Computer Science 939, Springer-Verlag, 1995, pp. 381-394. Co-authored with H. Wong-Toi. Postscript.

• HyTech : The next generation, in Proceedings of the 16th Annual IEEE Real-time Systems Symposium (RTSS95), 1995. Co-authored with T.A. Henzinger and H. Wong-Toi. Html.

• A user guide to HyTech, in Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS95), Lecture Notes in Computer Science 1019, Springer-Verlag, 1995, pp. 41-71. Co-authored with T.A. Henzinger and H. Wong-Toi. Html.

• A note on abstract-interpretation strategies for hybrid automata, in Proceedings of the Hybrid System Workshop, Lecture Notes in Computer Science 999, Springer-Verlag, 1995. Co-authored with T.A. Henzinger. Html.

• HyTech: the Cornell HYbrid TECHnology tool, in Proceedings of the Hybrid System Workshop, Lecture Notes in Computer Science 999, Springer-Verlag, 1995. Co-authored with T.A. Henzinger. Html.

• Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, in Proceedings of Hybrid Systems Workshop, Lecture Notes in Computer Science 736, Springer-Verlag, 1993, pp. 209--229. Co-authored with R. Alur, C. Courcoubetis and T.A. Henzinger Html.

Graph Algorithms

• The Beta-Assignment Problems, in European Journal of Operation Research, Vol. 104, No.3, pp 593-600, 1998 Co-authored with G.J. Chang. Postscript.

• The Beta-Assignment Problem in General Graphs, in Computers and Operation Research, Vol. 24, No. 8, pp.757-765, 1997. Co-authored with G.J. Chang. Postscript.

• The Domatic Problems on Interval Graphs, in SIAM Journal of Discrete Mathematics, 3(4). pp.531--536, 1990. Co-authored with T.-L. Lu and G.J. Chang.

Last Modified JAN 2009