Model checking

By Edmund M. Clarke, E. Emerson, Joseph Sifakis, Eric Allen, Emerson Joseph Sifakis. Communications of the ACM, 2009

3,149 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/79cadc74d31453332cde42ebfddcaae5bb86ed1a

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Helen Schonenberg
2. Maja Pesic
3. Wil M.P. van der Aalst
4. Hadas Kress-Gazit
5. George Pappas
6. Dorsa Sadigh
7. Georgios Fainekos
8. Sanjit A. Seshia

In Computational Theory and Mathematics

1. Hadas Kress-Gazit
2. Helen Schonenberg
3. Sanjit A. Seshia
4. Dirk Beyer
5. Georgios Fainekos
6. Ranjit Jhala
7. Rupak Majumdar
8. Thomas A. Henzinger

In Software

1. Dirk Beyer
2. Sanjit A. Seshia
3. Rupak Majumdar
4. Ranjit Jhala
5. Thomas A. Henzinger
6. Mark Harman
7. Georgios Fainekos
8. Hadas Kress-Gazit

Citations in the corpus

• Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools (2014, neutral): “BDDs are heavily used in model checking, to efficiently represent the state space and transition relation [35, 48].”
• Temporal-Logic-Based Reactive Mission and Motion Planning (2009, methodology): “Following the work in [5], we utilize atomic controllers that satisfy the so-called bisimulation property [31], [32], [34].”
• Runtime Verification for LTL and TLTL (2011, methodology): “complementing other verification techniques such as model checking [Clarke et al. 1999] and testing.”
• Petri Nets for Systems and Synthetic Biology (2008, background): “The behaviour of such a net forms a discrete state space, which can be analysed in the bounded case, for example, by a branching time temporal logic, one instance of which is Computational Tree Logic (CTL), see [CGP01].”
• Using formal specifications to support testing (2009, methodology): “These decision procedures conduct a systematic generation and exploration of the underlying system’s state space [Clarke et al. 1999; Manna and Pnueli 1995].”
• The worst-case execution-time problem—overview of methods and survey of tools (2008, methodology): “The remaining test data are generated using formal test data generation based on model checking [Clarke et al. 1999].”
• Towards Verified Artificial Intelligence (2016, methodology): “s, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. A spectrum of formal methods, from specification-driven testing and simulation [29], to model checking [14,62,15] and theorem proving (see, e.g. [58,43,37]) are used routinely in the computeraided design”
• Declarative workflows: Balancing between flexibility and support (2009, methodology): “To achieve this we use an approach similar to [17; 24].”
• The software model checker Blast (2007, methodology): “Model checking is an algorithmic technique to verify a system description against a specification [20,22,75].”