Calculational Design of a Regular Model Checker by Abstract Interpretation

Patrick Cousot

doi:10.1007/978-3-030-32505-3_1

Calculational Design of a Regular Model Checker by Abstract Interpretation

Patrick Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English (US)
Title of host publication	Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings
Editors	Robert Mark Hierons, Mohamed Mosbah
Publisher	Springer
Pages	3-21
Number of pages	19
ISBN (Print)	9783030325046
DOIs	https://doi.org/10.1007/978-3-030-32505-3_1
State	Published - 2019
Event	16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019 - Hammamet, Tunisia Duration: Oct 31 2019 → Nov 4 2019

Publication series

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

Conference

Conference	16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019
Country/Territory	Tunisia
City	Hammamet
Period	10/31/19 → 11/4/19

Keywords

Abstract interpretation
Calculational design
Model checking

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-32505-3_1

Cite this

Cousot, P. (2019). Calculational Design of a Regular Model Checker by Abstract Interpretation. In R. M. Hierons, & M. Mosbah (Eds.), Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings (pp. 3-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11884 LNCS). Springer. https://doi.org/10.1007/978-3-030-32505-3_1

Calculational Design of a Regular Model Checker by Abstract Interpretation. / Cousot, Patrick.
Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings. ed. / Robert Mark Hierons; Mohamed Mosbah. Springer, 2019. p. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11884 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cousot, P 2019, Calculational Design of a Regular Model Checker by Abstract Interpretation. in RM Hierons & M Mosbah (eds), Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11884 LNCS, Springer, pp. 3-21, 16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019, Hammamet, Tunisia, 10/31/19. https://doi.org/10.1007/978-3-030-32505-3_1

Cousot P. Calculational Design of a Regular Model Checker by Abstract Interpretation. In Hierons RM, Mosbah M, editors, Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings. Springer. 2019. p. 3-21. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-32505-3_1

Cousot, Patrick. / Calculational Design of a Regular Model Checker by Abstract Interpretation. Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings. editor / Robert Mark Hierons ; Mohamed Mosbah. Springer, 2019. pp. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9a78182a3ad84085a45a6a5e3f56fe07,

title = "Calculational Design of a Regular Model Checker by Abstract Interpretation",

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",

author = "Patrick Cousot",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019 ; Conference date: 31-10-2019 Through 04-11-2019",

year = "2019",

doi = "10.1007/978-3-030-32505-3_1",

language = "English (US)",

isbn = "9783030325046",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--21",

editor = "Hierons, {Robert Mark} and Mohamed Mosbah",

booktitle = "Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings",

}

TY - GEN

T1 - Calculational Design of a Regular Model Checker by Abstract Interpretation

AU - Cousot, Patrick

N1 - Publisher Copyright: © Springer Nature Switzerland AG 2019.

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Abstract interpretation

KW - Calculational design

KW - Model checking

UR - http://www.scopus.com/inward/record.url?scp=85076147086&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076147086&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-32505-3_1

DO - 10.1007/978-3-030-32505-3_1

M3 - Conference contribution

AN - SCOPUS:85076147086

SN - 9783030325046

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 21

BT - Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings

A2 - Hierons, Robert Mark

A2 - Mosbah, Mohamed

PB - Springer

T2 - 16th International Colloquium on Theoretical Aspects of Computing, ICTAC 2019

Y2 - 31 October 2019 through 4 November 2019

ER -

Calculational Design of a Regular Model Checker by Abstract Interpretation

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this