Edmund Melson Clarke

Note: When work was published in both a conference proceedings and a journal, I have summarized the journal form due to its more polished and archival nature. Two exceptions to this are the original conference papers defining model checking (1981) and symbolic model checking (1990), for which I cite the conference version.

1. Clarke, E. M., "Synthesis of resource invariants for concurrent programs", ACM Transactions on Programming Languages and Systems, Vol. 2 No. 3, July 1980, pp. 338–358, DOI: 10.1145/357103.357109This is an early bridge from programmer-derived proofs of correctness to machine-derived proofs. Owicki and Gries had proposed resource invariants as an approach to proving correctness of concurrent programs. Clarke presents an algorithm for deriving such invariants. Clarke’s elaboration of this work ultimately led to his development of model-checking with E. Allen Emerson.
2. Clarke, E. M. and E. A. Emerson, "Design and synthesis of synchronization skeletons using branching time temporal logic", Proceedings of Workshop on Logic of Programs, 1981, pp. 52–71.The focus of this work is the synthesis of concurrent programs from specifications written in temporal logic, with model checking presented as a secondary result. The early algorithm presented here was quadratic in the number of states. It was quickly improved to the more efficient one described in the next paper. Together with the independent work by Quielle and Sifakis, this paper represents the first description of model checking.
3. Clarke, E. M., E. A. Emerson and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986, pp. 244–263, DOI: 10.1145/5397.5399.This is the first complete and efficient explicit-state model checking algorithm. This paper reflects the recognition, incomplete as of the writing of the 1981 paper, that checking the properties of previously-written algorithms was more broadly applicable than the synthesis of algorithms from specifications in temporal logic.
4. Burch, J. R., E. M. Clarke, K. L. McMillan, D. L. Dill and L. J. Hwang, "Symbolic model checking: 10²⁰ states and beyond," Information and Computation: Selections from the 1990 IEEE Symposium on Logic In Computer Science (LICS), 33 pp.Symbolic model checking uses the binary decision diagram (BDD) representation to radically expand the state space that can be realistically analyzed by model checkers. This paper was awarded the Logic In Computing Science (LICS) 2010 Test-of-Time award.
5. Clarke, E. M., O. Grumberg, H. Hiraishi, S. Jha, D. E.Long, K. L.McMillan and L. A. Ness, "Verification of the Futurebus+ cache coherence protocol," Formal Methods in System Design, 6, 1995, pp. 217–232, DOI: 10.1007/BF01383968. This documents a landmark effort: applying the symbolic model checking methods described in the previous paper to a large, industrially significant bus protocol. The authors verified configurations with as many as 10³⁰ states. This was the first formal analysis to find errors in a proposed IEEE standard.
6. Clarke, E., A. Biere, R. Raimi and Y. Zhu, “Bounded model checking using satisfiability solving,” Formal Methods in System Design, Vol. 19, 2001, pp. 7–34. DOI: 10.1023/A:1011276507260 An introduction to bounded model checking, which uses SAT solvers to rapidly search for counterexamples to a proposed system property. The SAT solvers can often find counterexamples more quickly than the BDD-based implementations of earlier symbolic checkers. The SAT-based methods are limited, however, by the requirement to set a prior bound on the length of counterexamples. For most systems and their properties, a bounded model checker will not be able to rule out the existence of counterexamples, as a counterexample may exist that is longer than the bound set for the checker.
7. Clarke, E. M., O.Gumberg, S. Jha, Y. Lu and H. Veith, "Counterexample-guided abstraction refinement for symbolic model checking," Journal of the ACM, Vol. 50, No. 5, September 2003, pp. 752—794, DOI: 10.1145/876638.876643. CEGAR—CounterExample-Guided Abstraction Refinement—is another technique addressing the state space explosion. A system is initially represented in highly simplified form, for which counterexamples are found. A counterexample to this approximation may not in fact be a counterexample to the full system. CEGAR checkers verify whether such a counterexample to the simplified system also is a counterexample to the full system. If it is not a counterexample, the simplified representation is made more precise, allowing it to accept the former counterexample. Checking then proceeds with this refined, more precise form.