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

A grouping.

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

Symbolic model checking using SAT procedures instead of BDDs

Armin Biere and others (1999) · ACM

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

Compositional reasoning in model checking

Sergey Berezin and others (1997) · International Symposium on Compositionality · Springer

Computer-aided verification

E. M. Clarke and others (1996) · IEEE Spectrum · Institute of Electrical and Electronics Engineers

Formal methods: State of the art and future directions

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

Verifying the SRT division algorithm using theorem proving techniques

E. M. Clarke and others (1996) · Springer Berlin Heidelberg

Word Level Model Checking -- Avoiding the Pentium FDIV Error

E. M. Clarke and others (1996) · 33rd Design Automation Conference (DAC '96) · 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

Symbolic model checking for sequential circuit verification

J.R. Burch and others (1994) · Institute of Electrical and Electronics Engineers (IEEE)

Another look at LTL Model Checking

E. M. Clarke and others (1994) · CAV’94

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

Exploiting symmetry in temporal logic model checking

E. M. Clarke and others (1993) · Springer Berlin Heidelberg

Verification of the Futurebus1 cache coherence protocol

E. M. Clarke and others (1993) · Proceedings CHDL

Symbolic model checking: 10^20 States and beyond

J. R. Burch and others (1992) · Information and Computation · Elsevier BV

Automatic verification of sequential circuit designs

E. M. Clarke and others (1992) · Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences · Royal Society

Model checking and abstraction

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

Representing circuits more efficiently in symbolic model checking

Jerry R. Burch and others (1991)

Symbolic model checking with partitioned transition relations

J. R. Burch and others (1991) · Proceedings of the IFIP International Conference on Very Large Scale Integration (VLSI 91), Edinburgh

Symbolic model checking with partitioned transition relations

J. R. Burch and others (1991) · Technical Report CMU-CS-9 1-195

Symbolic model checking: 10^20 states and beyond

Jerry R. Burch and others (1990) · Proceedings - Symposium on Logic in Computer Science · Institute of Electrical and Electronics Engineers

A unified approach for showing language containment and equivalence between various types of ω-automata

E. M. Clarke and others (1990) · Springer Berlin Heidelberg

A parallel algorithm for constructing binary decision diagrams

S. Kimura and others (1990) · IEEE Comput. Soc. Press

Compositional model checking

E. M. Clarke and others (1989)

A language for compositional specification and verification of finite state hardware controllers

E. M. Clarke and others (1989) · 9th International Symposium on Hardware Description Languages and their Applications

A synthesis of two approaches for verifying finite state concurrent systems

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

Characterizing Kripke Structures in Temporal Logic.

M. C. Browne and others (1987) · Defense Technical Information Center

Automatic Verification of Sequential Circuits Using Temporal Logic

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

Automatic verification using temporal logic: two new examples

M. C. Browne and others (1986) · Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI · North-Holland

Reasoning about networks with many identical finite state processes

M. C. Browne and others (1986) · ACM Symposium on Principles of Distributed Computing (PODC 1986)

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

D.L. Dill and others (1986) · Institution of Engineering and Technology (IET)

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

The characterization problem for Hoare logics

Edmund M. Clarke Jr. (1984) · Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences · The Royal Society

Automatic verification of finite state concurrent system using temporal logic specifications

E. M. Clarke and others (1983) · ACM Press

Effective axiomatizations of Hoare logics

Edmund M. Clarke Jr. and others (1983) · Journal of the ACM

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

Programming language constructs for which it is impossible to obtain good Hoare axiom systems

Edmund M. Clarke Jr. (1979) · Journal of the ACM