Students Receiving Ph.D Degree
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 NEC Labs, Princeton, NJ.
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; Currently at JPL, NASA, CA.
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.
W. Marrero, BRUTUS: A Model Checker for Security Protocols, June, 2001; Current Position: Assistant Professor, DePaul University, Chicago, IL.
Y. Lu, Automatic
Abstraction for Model Checking, May 2000; Current Position:
Broadcom,
San Jose, CA.
M. Minea, Model Checking with Partial Order Reduction for Real-Time Systems, December 1999; Current Position: Postdoctoral Researcher in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley.
V. Hartonas-Garmhausen, Probabilistic Symbolic Model Checking with Engineering Models and Applications, Engineering and Public Policy, Carnegie Mellon University, April, 1998.
S. 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.
X. Zhao, Verification
of Arithmetic Circuits, August 1996; Current Position:
Intel Corporation, Beaverton, OR.
D.E. Long, Model Checking, Abstraction and Modular Verification, August 1993; Current Position: AT&T Bell Laboratories, Murray Hill, NJ.
J.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.
K.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: Cadence Berkeley Laboratories.
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.
D.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).
B. 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.
Ph.D Thesis Committees
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
Post-Docs
Visitors
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