Reasoning about sequences of memory states

Motivated by the verification of 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 analyze 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. We provide a complete picture based on these criteria. Our main decidability result is PSPACE-completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic. Sigma(0)(1)-completeness or E-1(1)-completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results. (C) 2009 Elsevier B.V. All rights reserved.