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

• Type: Conference
• Year: 2007
• Where: LFCS
• Authors: Rémi Brochenin, Stéphane Demri, Étienne Lozes
• Keywords: LFCS 2007, Separation Logic, Temporal Logic, Temporal Logic Ltlmem