• Soon Ho Kong
• Qinsi Wang

Students Receiving Ph.D Degree

Anvesh Komuravelli Compositional Verification with Abstraction, Learning, and SAT Solving, March 2015

Will Klieber Formal Verification using Quantified Boolean Formulas (QBF), August 2013.

Sicun Gao, Computable Analysis, Hybrid Automata, and Decision Procedures: A New Framework for the Formal Verification of Cyber-Physical Systems. .

Himanshu Jain, Verification Using Satisfiability Checking, Abstraction, and Craig Interpolation; .

Nishant Sinha, Automated Compositional Analysis for Checking Component Substitutability, December 2007; .

Pankaj Chauhan, Verification of Large Industrial Circuits Using SAT Based Reparameterization and Abstraction-Refinement, April 2007.

Muralidhar Talupur, Abstraction Techniques for Parameterized Verification, December 2006.

Anubhav Gupta, Learning Abstractions for Model Checking, June 2006.

Alex Groce, Error Explanation and Fault Localization with Distance Metrics, March 2005.

Sagar Chaki, A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs, January 2005.

Dong Wang , SAT based Abstraction Refinement for Hardware Verification, May 2003.

Sergey Berezin, Model Checking and Theorem Proving: a Unified Framework, January 2002.

Wilfredo Marrero, BRUTUS: A Model Checker for Security Protocols, June, 2001.

Yuan Lu, Automatic Abstraction for Model Checking, May 2000.

Marius Minea, Model Checking with Partial Order Reduction for Real-Time Systems, December 1999.

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.

Sergios Campos, A Quantitative Approach to the Formal Verification of Real-Time Systems, September 1996.

Xudong Zhao, Verification of Arithmetic Circuits, August 1996.

David E. Long, Model Checking, Abstraction and Modular Verification, August 1993.

Jerry. R. Burch, Trace Algebra for Automatic Verification of Real-Time Concurrent Systems, August 1992.

Ken L. McMillan, Symbolic Model Checking, May 1992.

M.C. Browne, Automatic Verification of Sequential Circuits, Carnegie Mellon University, January 1989.

David L. Dill, Automatic Verification of Asynchronous Circuits using Automata, Carnegie Mellon University, August 1987.

Bud Mishra, Graph Theoretic Algorithms and the Design of VLSI Systems, Carnegie Mellon University, September 1985.

A. Prasad Sistla, Theoretical Issues in the Design and Verification of Distributed Systems, Harvard University, July 1983.

Christos N. Nikolaou, Reliability Issues in Distributed Systems, Harvard University, June 1982. (deceased, 2015)

E. Allen Emerson, Branching Time Temporal Logic and the Design of Correct Concurrent Programs, Harvard University, August 1981.

Students Receiving M.S. Degree

Anneliese K. von Mayrhauser, Proving Parallel Programs Correct, Duke University, July 1978.

Bruce W. Ballard, Systematic Removal of Recursion for a Class of Lisp-like Recursion Schemes, Duke University, May 1977.

Post-Docs

Leonid Ryzhyk - 2014 - 2015
Nina Narodytska - 2014 - 2015
Natasa Miskov-Zivanov - 2014-2015
Kyungmin Bae - 2014-2015
Sicun (Sean) Gao - 2012 - 2014
Fuyuan Zhang - 2013-2014
Bing Liu - 2010-2013
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
Karsten Schmidt - 2000-2001
Helmut Veith - 1999-2000
Armin Biere - 1997-1998
Wolfgang Heinle - 1997-1998
Subash Shankar - 1997-1998
Yunshan Zhu 1997 - 1998
David Deharbe - 1995-1997
Orna Grumberg 1985-1987

Visitors

Peng Wu - 2014
Xudong He - 2014
Orna Grumberg - 1988-1999, summers 2001-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
Andre Platzer 2006
F. Wang 2001
Gi-Hwon Kwon 1999-2000, 2006
P. Williams 1999-2000
Subash Shanker 1997
S. Krischner 1993
Kiyoharu Hamaguchi 1993
P. Granger 1992
Thomas Filkorn 1992 
Holger Schlingloff 1991
Hiromi Hiraishi 1988, 1994
J. P. Vidal 1990
T. Yoneda 1990
S. Kimura 1989
T. Tang 1986
Y. Q. Sun 1986
Yulin Feng 1985 

Ph.D Thesis Committees

A.L. Turk, Advisor: Gary J. Powers, Chemical Engineering Department, Carnegie Mellon University.

Miroslav Velev, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.

Alongkarn Chutinan, Advisor: Bruce Krogh, Electrical and Computer Engineering Department, Carnegie Mellon University.

Y.-A. Chen, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.

Kurt Stirewalt, Advisor: Gregory Abowd, Department of Computer Science, Georgia Institute of Technology.

Alok Jain, Advisor: Randy Bryant, Electrical and Computer Engineering Department, Carnegie Mellon University.

Jurgen Dingel, Advisor: Steve Brookes, Computer Science Department, Carnegie Mellon University.

S. Older, Advisor: Steve Brookes, Computer Science Department, Carnegie Mellon University.

Markus Kaltenbach, Advisor: J. Mishra, Computer Science Department, University of Texas, Austin, 1996.

S. Probst, Advisor: Gary Powers, Chemical Engineering, Carnegie Mellon University.

Aarti Gupta, Advisor: Allan Fisher, Computer Science Department, Carnegie Mellon University.

D. L. Beatty, Advisor: Randy Bryant, Computer Science Department, Carnegie Mellon University.

Il 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.

Marko Petkovsek, Finding Closed-Form Solutions of Difference Equations by Symbolic Methods, September 1990; Advisor: Dana Scott, Computer Science Department, Carnegie Mellon University