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

Patrick Cousot.
Calculational Design of a Regular Model Checker by Abstract Interpretation
In Proceedings of the 16th International Colloquium on Theoretical Aspects of Computing, R. M. Hierons and M. Mosbah (Eds.): ICTAC 2019, Hammamet, Tunisia, October 31—November 4, 2019, Springer LNCS, 2019. LNCS 11884, pp. 3—21, © Springer, 2019.
Paper:
- PDF (291 KB)
Slides of the 55mn presentation at ICTAC'19:
- 1 slide per landscape page, (295 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.

Bibliographic reference:

@inproceedings{DBLP:conf/ictac/Cousot19,
  author    = {Patrick Cousot},
  title     = {Abstract Semantic Dependency},
  booktitle = {{ICTAC}},
  series    = {Lecture Notes in Computer Science},
  volume    = {11884},
  pages     = {3--21},
  publisher = {Springer},
  year      = {2019}
}

copyright notice, Springer copyright notice
Last modified: Fri Nov 1 17:57:11 CET 2019