Patrick Cousot, Calculational Design of a Regular Model Checker by Abstract Interpretation

Patrick Cousot.
Calculational Design of a Regular Model Checker by Abstract Interpretation
Theoretical Computer Science, Volume 869, 12 May 2021, Pages 62-84.
Paper:
- PDF (436 KB)
Abstract:
Security monitors have been used to check for safety program properties at runtime, that is for any given execution trace. Such security monitors check a safety temporal property specified by a finite automaton or, equivalently, a regular expression. Checking this safety temporal specification for all possible execution traces, that is the program semantics, is a static analysis problem, more precisely a model checking problem, since model checking specializes in temporal properties. We show that the model checker can be formally designed by calculus, by abstract interpretation of a formal trace semantics of the programming language. The result is a structural sound and complete model checker, which proceeds by induction on the program syntax (as opposed to the more classical approach using computation steps formalized by a transition system). By Rice theorem, further hypotheses or abstractions are needed to get a realistic model checking algorithm.
Keywords:
Abstract interpretation, Calculational design, Model checking, Regular expression trace property specification.

Bibliographic reference:

@article{DBLP:journals/tcs/Cousot21,
  author    = {Patrick Cousot},
  title     = {Calculational Design of a Regular Model Checker by Abstract Interpretation},
  journal   = {Theor. Comput. Sci.},
  volume    = {869},
  month     = {May 12th},
  pages     = {62--84},
  year      = {2021},
  url       = {https://doi.org/10.1016/j.tcs.2021.01.037},
}

copyright notice
Last modified: Sun May 2 14:30:34 EDT 2021