- Sicun (Sean) Gao
- Fuyuan Zhang
- Bing Liu
Students Receiving Ph.D Degree
Sicun Gao, Computable Analysis, Hybrid Automata, and Decision Procedures: A New Framework for the Formal Verification of Cyber-Physical Systems. Currently Postdoc at CMU.
Himanshu Jain, Verification Using Satisfiability Checking, Abstraction, and Craig Interpolation; Currently at Synopsys, Inc.
Nishant Sinha, Automated Compositional Analysis for Checking Component Substitutability, December 2007; Currently at IBM IRL
Pankaj Chauhan, Verification of Large Industrial Circuits Using SAT Based Reparameterization and Abstraction-Refinement, April 2007; Currently at Calypto Design Systems, Inc., Santa Clara, CA.
Muralidhar Talupur, Abstraction Techniques for Parameterized Verification, December 2006; Currently at Intel Research, Portland, OR.
Anubhav Gupta, Learning Abstractions for Model Checking, June 2006; Currently at Cadence Berkeley Labs, CA.
Alex Groce, Error Explanation and Fault Localization with Distance Metrics, March 2005; Assistant Professor of Computer Science at Oregon State University
Sagar Chaki, A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs, January 2005; Currently at SEI, CMU, Pittsburgh.
Dong Wang , SAT based Abstraction Refinement for Hardware Verification, May 2003; Current Position: Synopsis, CA.
Wilfredo Marrero, BRUTUS: A Model Checker for Security Protocols, June, 2001; Current Position: Associate Professor, DePaul University, Chicago, IL.
Yuan Lu, Automatic Abstraction for Model Checking, May 2000; Current Position: School of Sciences, Shenyang University, Shenyang 110044, China
Marius Minea, Model Checking with Partial Order Reduction for Real-Time Systems, December 1999; Current Position: Associate Professor Department of Computer and Software Engineering Politehnica University of Timişoara
Vicky Hartonas-Garmhausen, Probabilistic Symbolic Model Checking with Engineering Models and Applications, Engineering and Public Policy, Carnegie Mellon University, April, 1998.
Somesh Jha, Symmetry and Induction in Model Checking, October 1996; Current Position: Assistant Professor, University of Wisconsin, Madison, WI.
S. Campos, A Quantitative Approach to the Formal Verification of Real-Time Systems, September 1996; Current Position: Associate Professor at the Computer Science Department of the Universidade Federal de Minas Gerais, city of Belo Horizonte, Brasil.
Xudong Zhao, Verification of Arithmetic Circuits, August 1996; Current Position:
College of Information and Control Engineering, China University of Petroleum, Qingdao, 266555, China
D. E. Long, Model Checking, Abstraction and Modular Verification, August 1993; Current Position: AT&T Bell Laboratories, Murray Hill, NJ.
Jerry. R. Burch, Trace Algebra for Automatic Verification of Real-Time Concurrent Systems, August 1992; First Position: Post-Doctoral Research, Department of Computer Science, Stanford University; Current Position: Cadence Berkeley Laboratories.
Ken L. McMillan, Symbolic Model Checking, May 1992; First Position: AT&T Bell Laboratories, Murray Hill, NJ. (McMillan's thesis was a co-winner of the 1992 ACM Doctoral Dissertation Award); Current Position: Microsoft Research
M.C. Browne, Automatic Verification of Sequential Circuits, Carnegie Mellon University, January 1989; First Position: Project Scientist on Warp and Nectar projects, Carnegie Mellon University; Current Position: Sun Computer Corporation, CA.
David L. Dill, Automatic Verification of Asynchronous Circuits using Automata, Carnegie Mellon University, August 1987; Current Position: Tenured Full Professor, Stanford University. (Dill's thesis tied for second place in the ACM Dissertation Award Contest and published as an ACM Distinguished Dissertation).
Bud Mishra, Graph Theoretic Algorithms and the Design of VLSI Systems, Carnegie Mellon University, September 1985; Current Position: Tenured Full Professor, Courant Institute of Mathematical Sciences, New York University.
A.P. Sistla, Theoretical Issues in the Design and Verification of Distributed Systems, Harvard University, July 1983; First position: Assistant Professor, University of Massachusetts, Amherst; Current Position: Full Professor, CS Dept., University of Illinois at Chicago.
C.N. Nikolaou, Reliability Issues in Distributed Systems, Harvard University, June 1982; First Position: Manager, Multi-systems Resource Management group, IBM T.J. Watson Research Center, Yorktown Heights, New York; Current Position: University of Crete, Greece.
E.A. Emerson, Branching Time Temporal Logic and the Design of
Correct Concurrent Programs, Harvard University, August 1981; Current
Position: Tenured Full Professor, University of Texas, Austin.
Students Receiving M.S. Degree
Anneliese K. von Mayrhauser, Proving Parallel Programs Correct, Duke University, July 1978. Currently Assistant vice President for Research Colorado State University.
Bruce W. Ballard, Systematic Removal of Recursion for a Class of Lisp-like Recursion Schemes, Duke University, May 1977.
Haijun Gong - 2009-2012
Michael Wang - 2012
Paolo Zuliani - 2008-2012
Silke Wagner - 2008
Axel Legay - 2008-2009
Kwang Kuen Yi-2008
Lei Bu - 2007-2008
Alexandre Donze - 2007-2008
Azadeh Farzan - 2007-2008
James Kapinski - 2007
Alexandre Donze - 2007-2008
Wolfgang Windsteiger - 2006
Catalin Ionescu - 2006-2007
Tamir Heyman - 2005-2007
Haifeng Zhu - 2005-2006
Constantinos Bartzis - 2004-2007
Aleksandar Nanevski - 2005
Prasanna Thati - 2005
Daniel Milam - 2005
Ansgar Fehnker - 2003-2004
Michael Theobald - 2001-2004
Joel Ouaknine - 2002-2004
Tayssir Touili - 2003-2004
Daniel Kroening - 2001-2004
Karen Yorav - 2002-2003
Ofer Strichman - 2001-2003
K. Schmidt - 2000-2001
Helmut Veith - 1999-2000
Armin Biere - 1997-1998
W. Heinle - 1997-1998
S. Shankar - 1997-1998
Y. Zhu 1997 - 1998
D. Deharbe - 1995-1997
Orna Grumberg - 2011, 2012
Qiusong Yang - 2011, 2012
Fuyan Zhang - 2012
Marius Minea - 2012, 2013
Daniel Kroenig - 2012
Qinxiang Cao - 2012
Zhengwei Qi - 2011
Fei He - 2010
Jinn-Shu Chang - 2009
Kwang Keun Yi - 2008
Lei Bu - 2008
Ming-Hsien Tsai - 2008
Bow-Yaw Wang - 2008
Yu-Fang Chen - 2008
Ingo Feinerer 2007
F. Wang 2001
G.H. Kwon 1999-2000, 2006
P. Williams 1999-2000
S. Shanker 1997
S. Krischner 1993
H. Hamaguchi 1993
P. Granger 1992
T. Filkorn 1992
Holger Schlingloff 1991
H. Hiraishi 1988, 1994
J. P. Vidal 1990
O. Grumberg 1985-1987, Summers 1988-2000
T. Yoneda 1990
S. Kimura 1989
T. Tang 1986
Y. Q. Sun 1986
Y. Feng 1985
A.L. Turk, Advisor: Gary J. Powers, Chemical Engineering Department, Carnegie Mellon University.
M. Velev, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.
A. Chutinan, Advisor: Bruce Krogh, Electrical and Computer Engineering Department, Carnegie Mellon University.
Y.-A. Chen, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.
K. Stirewalt, Advisor: Gregory Abowd, Department of Computer Science, Georgia Institute of Technology.
A. Jain, Advisor: Randy Bryant, Electrical and Computer Engineering Department, Carnegie Mellon University.
J. Dingel, Advisor: Steve Brookes, Computer Science Department, Carnegie Mellon University.
S. Older, Advisor: Steve Brookes, Computer Science Department, Carnegie Mellon University.
M. Kaltenbach, Advisor: J. Mishra, Computer Science Department, University of Texas, Austin, 1996.
S. Probst, Advisor: Gary Powers, Chemical Engineering, Carnegie Mellon University.
A. Gupta, Advisor: Allan Fisher, Computer Science Department, Carnegie Mellon University.
D. Beatty, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.
I. Moon, Automatic Verification of Discrete Chemical Process Control Systems, August 1992; Advisor: Gary Powers, Chemical Engineering, Carnegie Mellon University.
O. Coudert, SIAM: A Toolbox for the Formal Proof of Sequential Systems, L'Ecole National Superieure Des Telecommunications, Paris, France, October 1991.M. Petkovsek, Finding Closed-Form Solutions of Difference Equations by Symbolic Methods, September 1990; Advisor: Dana Scott, Computer Science Department, Carnegie Mellon University