Calculational design of a regular model checker by abstract interpretation

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish (US)
Pages (from-to)62-84
Number of pages23
JournalTheoretical Computer Science
Volume869
DOIs
StatePublished - May 12 2021

Keywords

  • Abstract interpretation
  • Calculational design
  • Model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Calculational design of a regular model checker by abstract interpretation'. Together they form a unique fingerprint.

Cite this