Calculational Design of a Regular Model Checker by Abstract Interpretation

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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)
Title of host publicationTheoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings
EditorsRobert Mark Hierons, Mohamed Mosbah
Number of pages19
ISBN (Print)9783030325046
StatePublished - 2019
Event16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019 - Hammamet, Tunisia
Duration: Oct 31 2019Nov 4 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11884 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019


  • Abstract interpretation
  • Calculational design
  • Model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Calculational Design of a Regular Model Checker by Abstract Interpretation'. Together they form a unique fingerprint.

Cite this