Model checking: Algorithmic verification and debugging

Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis
[doi] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 09 July 2020

Communications of the ACM 52(11)
Association for Computing Machinery
New York, NY, USA
Pages 74-84
November 2009
Note(s): survey, model checking, temporal logic, bounded model checking, symbolic model checking, partial order reduction, CEGAR, abstract interpretation, Turing Award

This Turing Award paper/talk is a great overview of [model checking: definition, temporal logic, what it is good for, challenges (mostly state-space explosion), tricks (like symbolic model checking, bounded model checking, partial order reduction and CEGAR).

It also talks about the problems creating specifications. As well as challenges understanding subtle details of temporal logic, there are challenges specifying extra-functional requirements for security properties, reconfigurability properties, quality of service (e.g., jitter).

And it talks about problems verifying real world systems: mixed hardware-software systems, using abstraction to scale (using hybrid model checking / abstract interpretation methods and compositional reasoning) and exploiting design-time architectural choices to improve verifiability.

Model checking, Temporal logic