Computer Science Department
Edmund M. Clarke
Current Graduate Students
Current Post-Docs and Visitors
Former Graduate Students, Post-Docs, and Visitors

Students Receiving Ph.D Degree

Will Klieber Formal Verification using Quantified Boolean Formulas (QBF), August 2013, Currently at the Software Engineering Institute, Carnegie Mellon

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

Himanshu Jain, Verification Using Satisfiability Checking, Abstraction, and Craig Interpolation; Currently at Synopsis, Portland OR

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.

Sergey Berezin, Model Checking and Theorem Proving: a Unified Framework, January 2002; 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: Atrenta

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.

Sergios 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: Bohai University, China

David E. Long, Model Checking, Abstraction and Modular Verification, August 1993; Current Position: Integrated Software

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

Christos 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. Allen 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.


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


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


Content for class "clear" Goes Here