Edmund Clarke's Students, Post-Docs, & Visitors
Current Graduate Students Current Post-Docs and Visitors

Ph.D. Students

  • 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 CMU.

  • 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: Fellow, Avnera Corp., Portland Oregon

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

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

    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