TY - JOUR
T1 - Calculational design of a regular model checker by abstract interpretation
AU - Cousot, Patrick
N1 - Funding Information:
Supported by NSF Grant CCF-1617717 .
Publisher Copyright:
© 2021 Elsevier B.V.
PY - 2021/5/12
Y1 - 2021/5/12
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=85101886290&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85101886290&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2021.01.037
DO - 10.1016/j.tcs.2021.01.037
M3 - Article
AN - SCOPUS:85101886290
SN - 0304-3975
VL - 869
SP - 62
EP - 84
JO - Theoretical Computer Science
JF - Theoretical Computer Science
ER -