Details

Autor(en) / Beteiligte

• Cousot, Patrick

Titel

Calculational design of a regular model checker by abstract interpretation

Ist Teil von

• Theoretical computer science, 2021-05, Vol.869, p.62-84

Ort / Verlag

Elsevier B.V

Erscheinungsjahr

2021

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• •Abstract interpretation-based sound and complete calculational design methodology.•Regular expression trace property specification.•Trace property model-checker algorithm.•Verification of a safety property. 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.