Reasoning About Sequences of Memory States

13 years 4 months ago
Reasoning About Sequences of Memory States
Abstract. In order to verify programs with pointer variables, we introduce a temporal logic LTLmem whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We state the complexity of various model-checking and satisfiability problems for LTLmem , considering various fragments of separation logic (including pointer arithmetic), various classes of models (with or without constant heap), and the influence of fixing the initial memory state. Our main decidability result is pspace-completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic. Σ0 1 -completeness or Σ1 1 -completeness results are established for various problems, and underline the tightness of our decidability results. This paper is a preliminary version of [BDL07].
Rémi Brochenin, Stéphane Demri, &Eac
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LFCS
Authors Rémi Brochenin, Stéphane Demri, Étienne Lozes
Comments (0)