article · 1999

Model Checking

Edmund M. Clarke

Cited by 0Abstract and details only

Abstract

“When the time is ripe for certain things, these things appear in different places in the manner of violets coming to light in early spring. ” (Wolfgang Bolyai to his son Johann in urging him to claim the invention of non-Euclidean geometry without delay [Vit88]) 1 Model Checking Model Checking did not arise in a historical vacuum. There was an important problem that needed to be solved, namely Concurrent Program Verification. Concurrency errors are particularly difficult to find by program testing, since they are often hard to reproduce. Most of the formal research on this topic in-volved constructing proofs by hand using a Floyd-Hoare style logic. Probably, the best known formal system was the one proposed by Owicki and Gries [OG76] for reasoning about Conditional Critical Regions. Although I had written my thesis on the meta-theory of Hoare Logic [Cla77a,Cla77b,Cla78,Cla79a,Cla79c,Cla80] and was very familiar with the Owick-Gries proof methodology, I was quite skeptical about the scalability of hand constructed proofs. There had been some practical research on state exploration methods for communication protocols by Gregor Bochmann and others, but it was largely ignored by the “Formal Veri-fication Community”. Also, in the late 1970’s, Pnueli [Pnu77] and Owicki and Lamport [OL82] had proposed the use of Temporal Logic for specifying con-current programs. Although they still advocated hand constructed proofs, their work demonstrated convincingly that Temporal Logic was ideal for expressing concepts like mutual exclusion, absence of deadlock, and absence of starvation. Allen Emerson and I combined the state-exploration approach with Temporal Logic in an efficient manner and showed that the result could be used to solve non-trivial problems. Here is a quote from our original 1981 paper [CE81]:

Cite this paper

APA 7

Clarke, E. M. (1999). Model Checking.

MLA 9

Clarke, Edmund M. “Model Checking.” 1999.

Chicago

Clarke, Edmund M. 1999. “Model Checking.”

Harvard

Clarke, E.M. (1999) ‘Model Checking’.

BibTeX

@article{clarke1999model,
  title = {{Model Checking}},
  author = {Clarke, Edmund M.},
  year = {1999}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.