Software model checking

Ranjit Jhala, Rupak Majumdar
[doi] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 16 July 2020

ACM Computing Surveys 41(4)
Association for Computing Machinery
New York, NY, USA
October 2009
Note(s): survey, model checking, bounded model checking, partial order reduction, symbolic evaluation, symbolic execution, symbolic model checking, reachability, interpolation, separation logic, alias analysis, shape analysis, temporal logic, buchi automaton, kripke structure, BDD, CEGAR, BLAST verifier, CBMC verifier, KLEE verifier

This 2009 survey of software model checking covers a lot of ground from the roots in hardware model checking through to its application to software. A number of the key algorithms are described in pseudocode.

The sections give a good sense of what is covered

  • Introduction
  • Preliminary definitions
    • Simple programs
    • Properties
    • Organization

  • Concrete enumerative model checking

    (For small, finite state spaces)

    • Stateful search

      Forward and backward algorithms, Partial order reduction, compositional techniques, assume-guarantee

    • Systematic execution exploration

      Test amplification

    • Stateless search

    • Execution-based tools

      VeriSoft, JavaPathFinder, Cmc, MaceMC

  • Concrete symbolic model checking

    • The region data structure

      SymbolicReachability algorithm, reachability

    • Example: propositional logic

      BDDs

    • Example: first order logic with interpreted theories

    • Bounded model checking

      symbolic execution

    • Invariants and invariant synthesis

      abstraction techniques for invariant synthesis, k-induction, template-based synthesis

  • Model checking and abstraction

    reachability,

    • Abstract reachability analysis

      Finite height domains; infinite height domains and widening operators

    • Example: polyhedral domains

    • Example: predicate abstraction

      SLAM verifier, BLAST verifier, cartesian predicate abstraction

    • Example: control abstraction

      sequential programs, concurrent programs

    • Combined abstractions

      Gulwani and Tiwari shows a general framework for combining abstract interpretations for different theories, analogous to the manner in which decision procedures for different theories are combined.

  • Abstraction refinement

    CEGAR

    • Counterexamples and refinement
      • Counterexamples
      • Trace formulas
      • Syntax-based refinement
      • Interpolation-based refinement
      • Relative completeness
      • Refining multiple paths
      • Refining other domains
    • Abstraction-refinement-based model checkers
      • SLAM verifier and BEBOP
      • BLAST verifier and lazy refinement
      • Magic and concurrent, message-passing C programs
      • F-Soft
      • IMPACT
      • ARMC
  • Procedural abstraction
    • Programs with procedures

    • InterProcedural reachability

      memoization

      • Graph-based algorithms
      • Symbolic algorithms
      • Abstraction
      • Top-down vs. Bottom-up
      • Saturn
      • Houdini
    • Concurrency and recursion
  • Heap data structures
  • Liveness and termination
  • Model checking and software quality

    • Model checking and testing

      underapproximation

    • Model checking and type systems

      • Typestates
      • Dependent types
      • Hybrid type checking
  • Conclusion

Bounded model-checking, Model checking