An Abstract Interpretation-based Model for Safety Semantics

By: Roberto Giacobazzi and Isabella Mastroeni

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
roberto.giacobazzi@univr.it

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
isabella.mastroeni@univr.it

Abstract:

In this paper we describe safety semantics as abstract interpretation of a trace-based operational semantics of a transition system. Intuitively, a property is safety if "nothing bad will happen". Formally this is described by saying that a property is safety if it is maximal with respect to a given set of allowed partial executions. We show that this can be specified in the standard Cousot's framework of abstract interpretation. We characterize the structure of safety properties as abstract domains and their basic algebraic properties, like the absence of meet-irreducible elements. Then we derive fix-point safety semantics of a transition system by abstract interpretation in a hierarchy of semantics for programming languages. Moreover we use this construction in order to generate other safety semantics such as strong safety and safety without stuttering. They are all derived as abstractions of the safety semantics. Moreover we obtain the one without stuttering as fix-point semantics.