zbMATH — the first resource for mathematics

Reasoning about sequences of memory states. (English) Zbl 1132.68335
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 100-114 (2007).
Summary: In order to verify programs with pointer variables, we introduce a temporal logic LTL\(^{\text{mem}}\) 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 LTL\(^{\text{mem}}\), 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 \(\Sigma^{1}_{1}\)-completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results.
For the entire collection see [Zbl 1121.03005].
Reviewer: Reviewer (Berlin)

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI