Edmund Clarke
Edmund Clarke
University Professor Emeritus at Carnegie Mellon University
Verified email at cs.cmu.edu - Homepage
TitleCited byYear
Model checking
EM Clarke Jr, O Grumberg, D Kroening, D Peled, H Veith
MIT press, 2018
131032018
Automatic verification of finite-state concurrent systems using temporal logic specifications
EM Clarke, EA Emerson, AP Sistla
ACM Transactions on Programming Languages and Systems (TOPLAS) 8 (2), 244-263, 1986
49591986
Design and synthesis of synchronization skeletons using branching time temporal logic
EM Clarke, EA Emerson
Workshop on Logic of Programs, 52-71, 1981
40421981
Symbolic model checking: 1020 states and beyond
JR Burch, EM Clarke, KL McMillan, DL Dill, LJ Hwang
Information and computation 98 (2), 142-170, 1992
39531992
Symbolic model checking without BDDs
A Biere, A Cimatti, E Clarke, Y Zhu
International conference on tools and algorithms for the construction and …, 1999
26661999
Model checking and abstraction
EM Clarke, O Grumberg, DE Long
ACM transactions on Programming Languages and Systems (TOPLAS) 16 (5), 1512-1542, 1994
20321994
Counterexample-guided abstraction refinement
E Clarke, O Grumberg, S Jha, Y Lu, H Veith
International Conference on Computer Aided Verification, 154-169, 2000
19472000
Nusmv 2: An opensource tool for symbolic model checking
A Cimatti, E Clarke, E Giunchiglia, F Giunchiglia, M Pistore, M Roveri, ...
International Conference on Computer Aided Verification, 359-364, 2002
19042002
Formal methods: State of the art and future directions
EM Clarke, JM Wing
ACM Computing Surveys (CSUR) 28 (4), 626-643, 1996
18211996
The complexity of propositional linear temporal logics
AP Sistla, EM Clarke
Journal of the ACM (JACM) 32 (3), 733-749, 1985
13871985
A tool for checking ANSI-C programs
E Clarke, D Kroening, F Lerda
International Conference on Tools and Algorithms for the Construction and …, 2004
13752004
Counterexample-guided abstraction refinement for symbolic model checking
E Clarke, O Grumberg, S Jha, Y Lu, H Veith
Journal of the ACM (JACM) 50 (5), 752-794, 2003
9542003
Bounded model checking.
A Biere, A Cimatti, EM Clarke, O Strichman, Y Zhu
Advances in computers 58 (11), 117-148, 2003
9232003
Using branching time temporal logic to synthesize synchronization skeletons
EA Emerson, EM Clarke
Science of Computer programming 2 (3), 241-266, 1982
9091982
Symbolic model checking using SAT procedures instead of BDDs
A Biere, A Cimatti, EM Clarke, M Fujita, Y Zhu
Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), 317-320, 1999
8981999
Symbolic model checking for sequential circuit verification
JR Burch, EM Clarke, DE Long, KL McMillan, DL Dill
IEEE Transactions on Computer-Aided Design of Integrated Circuits and …, 1994
7791994
Bounded model checking using satisfiability solving
E Clarke, A Biere, R Raimi, Y Zhu
Formal methods in system design 19 (1), 7-34, 2001
7752001
NuSMV: A new symbolic model verifier
A Cimatti, E Clarke, F Giunchiglia, M Roveri
International conference on computer aided verification, 495-499, 1999
7721999
NuSMV: a new symbolic model checker
A Cimatti, E Clarke, F Giunchiglia, M Roveri
International Journal on Software Tools for Technology Transfer 2 (4), 410-425, 2000
7042000
Sequential circuit verification using symbolic model checking
JR Burch, EM Clarke, KL McMillan, DL Dill
Proceedings of the 27th ACM/IEEE Design Automation Conference, 46-51, 1991
6591991
The system can't perform the operation now. Try again later.
Articles 1–20