← Back to program

Model Checking and Exchange Formats

Session introduction · Wednesday, 09:00-10:30 · Chair: Dirk Beyer

Model checking is an automatic verification technique: a tool takes a model of a system and a property, then checks that property against every reachable state [1, 2]. This differs from testing, which only tries some runs, and from interactive proof, which needs a person to guide each step. Properties usually come in two kinds - a safety property says that a bad state is never reached, and a liveness property says that a good event happens eventually [1]. The central obstacle is the state-space explosion problem: the number of reachable states grows very fast with the number of variables and parallel components, so a plain search soon runs out of memory [1, 2]. Several methods in this session fight that explosion. Symbolic techniques store a whole set of states as one formula or one decision diagram instead of listing states individually, and decision diagrams are the classic structure for this [3]. Saturation is a state space exploration strategy tuned for asynchronous systems, where each event touches only a few variables, first developed on Petri nets [4]. A different route, SMT based techniques encodes the model as formulas and call an SMT solver, for example in bounded model checking [5, 6].

Abstraction offers another way to shrink the state space: it deliberately drops detail while keeping enough information to decide the property [1]. Counterexample-guided abstraction refinement (CEGAR) automates this by starting coarse and adding detail only when a counterexample proves to be spurious [7]. What an abstraction currently tracks is its precision, and precision reuse carries that information from one program version to the next, so a changed program need not be re-verified from scratch [8]. Reuse of this kind is one case of cooperative verification, where separate tools help each other by exchanging artifacts [9]. For that exchange to work, tools need common formats. A verification witness is a machine-checkable record that justifies a verdict, so an independent validator can re-check the result - a correctness witness supports a "true" verdict, and a violation witness describes a counterexample [10]. These shared formats are driven in large part by SV-COMP, the annual competition on software verification [11], and other competitions, such as HWMCC (Hardware Model Checking Competition).

The final theme is termination, the question of whether a program always halts, which is a common liveness property. No single algorithm can decide this for every program - this is the classical undecidability of the halting problem. In practice, a termination proof often relies on a ranking function, a quantity that strictly decreases at each step and cannot decrease forever, which forces the program to stop. Transition invariants are a more general argument of the same kind, and they can act as a termination witness that another tool is able to validate [12].

Keywords to look up: model checking · state-space explosion · reachability analysis · symbolic model checking · BDD / decision diagram · saturation · Petri net · SMT / SMT-LIB · bounded model checking · abstraction · CEGAR · precision reuse · cooperative verification · verification witness · SV-COMP · termination · ranking function · transition invariant.

Sources

  1. C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. ISBN 978-0-262-02649-9.
  2. E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem (eds.). Handbook of Model Checking. Springer, 2018. doi.org/10.1007/978-3-319-10575-8
  3. R. E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation." IEEE Trans. Computers, 1986. doi.org/10.1109/TC.1986.1676819
  4. G. Ciardo, G. Lüttgen, R. Siminiceanu. "Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation." TACAS, 2001. doi.org/10.1007/3-540-45319-9_23
  5. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. "Symbolic Model Checking without BDDs." TACAS, 1999. doi.org/10.1007/3-540-49059-0_14
  6. C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard: Version 2.6. 2017. smt-lib.org
  7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. "Counterexample-Guided Abstraction Refinement for Symbolic Model Checking." JACM, 2003. doi.org/10.1145/876638.876643
  8. D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, P. Wendler. "Precision Reuse for Efficient Regression Verification." ESEC/FSE, 2013. doi.org/10.1145/2491411.2491429
  9. D. Beyer, H. Wehrheim. "Verification Artifacts in Cooperative Verification." ISoLA, 2020. doi.org/10.1007/978-3-030-61362-4_8
  10. D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, A. Stahlbauer. "Witness Validation and Stepwise Testification across Software Verifiers." ESEC/FSE, 2015. doi.org/10.1145/2786805.2786867
  11. D. Beyer. Competition on Software Verification (SV-COMP), annual reports, TACAS. sv-comp.sosy-lab.org
  12. A. Podelski, A. Rybalchenko. "Transition Invariants." LICS, 2004. doi.org/10.1109/LICS.2004.1319598