This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Edmund M. Clarke

Edmund M. Clarke: where Hoare-style proof stops (incompleteness, constructs with no good axiomatisation, the characterisation problem) and the alternative he built: synchronisation skeletons, model checking, symbolic model checking.

Handbook of Model Checking

Edmund M. Clarke and others (2018) · Springer International Publishing

dReal: An SMT Solver for Nonlinear Theories over the Reals

Sicun Gao and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Model Checking and the State Explosion Problem

Edmund M. Clarke and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Analog Circuit Verification by Statistical Model Checking

Ying-Chih Wang and others (2011) · 16th Asia and South Pacific Design Automation Conference (ASP-DAC 2011)

The Localization Reduction and Counterexample-Guided Abstraction Refinement

Edmund M. Clarke and others (2010) · Springer Berlin Heidelberg

Model checking: Algorithmic verification and debugging

Edmund M. Clarke and others (2009) · Communications of the ACM · Association for Computing Machinery

Bounded Model Checking

Armin Biere and others (2003) · Advances in computers · Elsevier BV

Symbolic Model Checking without BDDs

Armin Biere and others (1999) · Tools and Algorithms for the Construction and Analysis of Systems (TACAS) · Springer Science+Business Media

Model Checking

Edmund M. Clarke and others (1999) · MIT Press

Program Slicing of Hardware Description Languages

Edmund M. Clarke and others (1999) · School of Computer Science, Carnegie Mellon University

Formal methods: State of the art and future directions

Edmund M. Clarke and others (1996) · ACM Computing Surveys · Association for Computing Machinery (ACM)

Equivalence Checking Using Abstract BDDs

Somesh Jha and others (1996) · School of Computer Science, Carnegie Mellon University

Verification of the Futurebus+ cache coherence protocol

Edmund M. Clarke and others (1995) · Formal Methods in System Design · Springer Science+Business Media

Automatic verification of finite-state concurrent systems

Edmund M. Clarke (1994) · Lecture notes in computer science · Springer Science+Business Media

Model checking and abstraction

Edmund M. Clarke and others (1994) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery

Model checking and abstraction

Edmund M. Clarke and others (1992) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

Automatic Verification of Sequential Circuits Using Temporal Logic

Michael C. Browne and others (1986) · IEEE Transactions on Computers

Automatic verification of finite-state concurrent systems using temporal logic specifications

Edmund M. Clarke and others (1986) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery

Automatic verification of asynchronous circuits using temporal logic

David L. Dill and others (1985) · 1985 Chapel Hill Conference on VLSI · Computer Science Press

Hierarchical Verification of Asynchronous Circuits Using Temporal Logic

Bud Mishra and others (1985) · Theoretical Computer Science · North-Holland

Using branching time temporal logic to synthesize synchronization skeletons

E.Allen Emerson and others (1982) · Elsevier BV

Design and synthesis of synchronization skeletons using branching time temporal logic

Edmund M. Clarke and others (1981) · Logic of Programs · Springer

Characterizing correctness properties of parallel programs using fixpoints

E. Allen Emerson and others (1980) · Automata, Languages and Programming · Springer Berlin Heidelberg