Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Program verification can be described as the problem of deciding whether a given program exhibits a desired behaviour, often called its specification. Temporal logic, in its various flavours [24], is a very popular and widely studied specification formalism due to its relative simplicity and expressive power: a wide variety of safety (“something bad cannot happen”) and liveness properties (“something good eventually happens”) can be captured [20].

Historically, perhaps the most popular approach to automatically verify temporal properties of programs has been model checking: one first builds an abstract model that overapproximates all possible executions of the program, and then checks that the desired temporal property holds for this model (see e.g. [10, 13, 15]). However, this approach has been applied mainly to integer programs; the situation for memory-aware programs over heap data structures becomes significantly more challenging, mainly because of the difficulties in constructing suitable abstract models. One possible approach is simply to translate such heap-aware programs into integer programs, in such a way that properties such as memory safety or termination of the original program follow from corresponding properties in its integer translation [13, 15, 22]. However, for more general temporal properties, this technique can produce unsound results. In general, it is not clear whether it is feasible to provide suitable translations from heap to integer programs for any given temporal property; in particular, numerical abstraction of heap programs often removes important information about the exact shape of heap data structures, which might be needed to prove some temporal properties.

Thus, although it is often possible to provide numeric abstractions to suit specific programs and temporal properties, it is not clear that this is so for arbitrary programs and properties.

In this article, we instead approach the above problem via the main (perhaps less fashionable) alternative to model checking, namely the direct deductive verification. Common limitations of previous temporal logic proof systems include restriction to finite state transition systems [4, 18, 19] and/or a reliance on complex verification conditions that are seemingly difficult to fully automate [23, 29], the latter being arguably the most cited argument against deductive verification. In contrast, our proof system can handle infinite state systems, and an automated implementation is directly derivable from the proof rules and automata-based soundness checks, showing that temporal logic proof systems can indeed work in practice.

Our proof system manipulates temporal judgements about programs, and employs automatic proof search in this system to verify that a program has a given temporal property. Given some fixed program, the judgements of our system assert a temporal property of the program whose initial state satisfies some precondition, written in a fragment of separation logic [26], a well-known language for describing heap memory; in particular we also permit user-defined (inductive) predicates. The core of the proof system is a set of logical rules that operate on common logical connectives and unfold temporal modalities and predicate definitions, along with a set of symbolic execution rules that simulate program execution steps. To handle the fact that symbolic execution can in general be applied ad infinitum, we employ cyclic proof [6, 7, 9, 30], in which proofs are finite cyclic graphs subject to a global soundness condition. Using this approach, we are frequently able to verify temporal properties of heap programs in an automatic and sound way without the need of numeric abstractions or program translations. Moreover, our analysis has the added benefit of producing independently checkable proof objects.

We provide an implementation of our proof system as an automated verification tool within the Cyclist theorem proving framework [9] and evaluate its performance on a range of examples. The source code, benchmark and executable binaries of the implementation are publicly available online [1]. Our tool is able to discover surprisingly complex cyclic proofs of temporal program properties, with times often in the millisecond range. Practically speaking, the advantages and disadvantages of our approach are entirely typical of deductive verification: on the one hand, we do not need to employ abstraction or program translation, and we guarantee soundness; on the other hand, our algorithms might fail to terminate, and (at least currently) we do not provide counterexamples in case of failure. Thus we believe our approach should be understood as a useful complement to, rather than a replacement for, model checking.

The remainder of this paper is structured as follows. Section 2 introduces our programming language, the memory state assertion language, and temporal (CTL) assertions over these. Section 3 introduces our proof system for verifying temporal properties of programs, and Sect. 4 modifies this system to account for fair program executions. Section 5 presents our implementation and experimental evaluation, Sect. 6 discusses related work and Sect. 7 concludes.

This is an expanded journal version of our previous conference paper [31]. In the present paper we have endeavoured to include as much of the technical detail of our development (particularly our soundness proofs) as space permits.

In this section we introduce our programming language, our language of assertions about memory states (based on a fragment of separation logic) and our language for expressing temporal properties of programs, given by CTL over memory assertions.

Programming language We use a simple language of while programs with pointers and (de)allocation, but without procedures. We assume a countably infinite set Var of variables and a first-order language of expressions over \(\textsf {Var}\). Branching conditionsB and commandsC are given by the following grammar:where \(x \in \textsf {Var}\) and E ranges over expressions. We write \(\mathsf {*}\) for a nondeterministic condition, and [E] for dereferencing of expression E; in particular, the assignment forms \(\text {x}:=[E]\) and \([E] := E\) respectively read from and write to heap cells.

We define the semantics of the language in a stack-and-heap model employing heaps of records. We fix an infinite set Val of values, of which an infinite subset \(\textsf {Loc} \subset \textsf {Val}\) are addressable memory locations. A stack is a map \(s: \textsf {Var} \rightarrow \textsf {Val}\) from variables to values. The semantics \(\llbracket {E}\rrbracket s\) of expression E under stack s is standard; in particular, \(\llbracket {x}\rrbracket s = s(x)\) for \(x \in \textsf {Var}\). Assuming some fixed interpretation for any function symbols in the expression language, s can then be extended to all expressions in the usual way \(\llbracket {f(E_1, \ldots , E_n)}\rrbracket s = f(\llbracket {E_1}\rrbracket s, \ldots , \llbracket {E_n}\rrbracket s)\). We extend stacks pointwise to act on tuples of terms. A heap is a partial, finite-domain function \(h : \textsf {Loc} \rightharpoonup _{\text {fin}} (\textsf {Val}\ \textsf {List})\), mapping finitely many memory locations to records, i.e. arbitrary-length tuples of values; we write \(\mathrm {dom}(h)\) for the set of locations on which h is defined. We write e for the empty heap, and \(\uplus \) to denote composition of domain-disjoint heaps: \(h_1 \uplus h_2\) is the union of \(h_1\) and \(h_2\) when \(\mathrm {dom}(h_1) \cap \mathrm {dom}(h_2) = \emptyset \) (and undefined otherwise). If f is a stack or a heap then we write \(f[x \mapsto v]\) for the stack or heap defined as f except that \(f[x \mapsto v](x) = v\). A paired stack and heap, (s, h), is called a (memory) state.

A (program) configuration\(\gamma \) is a triple \(\langle {C} , {s} , {h} \rangle \) where C is a command, s a stack and h a heap. If \(\gamma \) is a configuration, we write \(\gamma _{\mathrm {C}}, \gamma _{\mathrm {s}}\), and \(\gamma _{\mathrm {h}}\) respectively for its first, second and third components. A configuration \(\gamma \) is called final if \(\gamma _{\mathrm {C}} = \mathbf skip \).

The small-step operational semantics of programs is given by a binary relation \(\leadsto \) on program configurations, where \(\gamma \leadsto \gamma '\) holds if the execution of the command \(\gamma _{\mathrm {C}}\) in the state \((\gamma _{\mathrm {s}},\gamma _{\mathrm {h}})\) can result in a new program configuration \(\gamma '\). We write \(\leadsto ^*\) for the reflexive-transitive closure of \(\leadsto \). The special configuration \(\mathsf {fault}\) is used to denote a memory fault, which results when a command tries to access non-allocated memory. The operational semantics of our programming language is shown in Fig. 1.

An execution path is a (maximally finite or infinite) sequence \((\gamma _i)_{i \ge 0}\) of configurations such that \(\gamma _i \leadsto \gamma _{i+1}\) for all \(i \ge 0\). If \(\pi \) is a path, then we write \(\pi _i\) for the ith element of \(\pi \). A path \(\pi \)starts from configuration \(\gamma \) if \(\pi _0 = \gamma \).

Memory state assertions We express properties of memory states (s, h) using a standard symbolic-heap fragment of separation logic (cf. [2]) extended with user-defined (inductive) predicates, typically used to express data structures in the memory.

We assume a fixed first-order logic language\(\varSigma _{\mathrm {log}}\) that extends the expression language of our programming language (i.e. \(\varSigma _{\mathrm {log}} \supseteq \varSigma _{\mathrm {exp}}\)). The terms of \(\varSigma _{\mathrm {log}}\) are defined as usual, with variables drawn from \(\mathsf {Var}\). We write \(t(x_1,\ldots , x_k)\) for a term t all of whose variables occur in \(\{x_1, \ldots , x_k\}\) and we use vector notation to abbreviate sequences. The interpretation \(\llbracket {t}\rrbracket s\) of a term t of \(\varSigma _{\mathrm {log}}\) in a stack s is then defined in the same way as expressions, provided we are given an interpretation for any constant or function symbol that is not in \(\varSigma _{\mathrm {exp}}\).

As usual in separation logic, the separating conjunction \(*\) is easily seen by the above definition to be associative and commutative, with unit \(\mathsf {emp}\). In the remainder of this paper, we take these laws for granted.

It remains to define the interpretation \(\llbracket {\varPsi }\rrbracket \) of each inductive predicate symbol \(\varPsi \), which is determined by a given inductive definition for \(\varPsi \). Our inductive definition schema follows closely the one formulated in e.g. [6, 8].

The standard interpretation of all inductive predicate symbols \(\varPsi _1, \ldots , \varPsi _n\) is then the least prefixed point of a mutual monotone operator constructed from the inductive definitions of all inductive predicate symbols.

We note that the operators \(\chi _i\) in Definition 4 are all monotone [6] and consequently the least prefixed point \(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi \) indeed exists. Moreover, this least prefixed point can be iteratively approached in approximant stages.

It is a standard fact that, for some ordinal \(\alpha \), the prefixed point \(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi \) is equal to the approximant \(\llbracket {\varvec{\varPsi }}\rrbracket ^{\alpha })\); in [6] it is shown that for our definition schema the closure ordinal is at most \(\omega \).

Temporal assertions We describe temporal properties of our programs using temporal assertions, built from the memory state assertions given above using standard operators of computation tree logic (CTL) [11], where the temporal operators quantify over execution paths from a given configuration.

Note that \(\mathsf {final}\) and \(\mathsf {error}\) denote final, respectively faulting configurations.

Judgements in our system are given by \(P \vdash C : \varphi \), where P is a symbolic heap, C is a command sequence and \(\varphi \) is a CTL assertion.

In this section, we present a cyclic proof system for establishing the validity of our CTL judgements on programs, as described in the previous section.

Our proof rules for CTL judgements are shown in Fig. 2. The symbolic execution rules for commands are adapted from those in the proof system for program termination in [7], accounting for whether a diamond \(\Diamond \) or box \(\Box \) property is being established. The dichotomy between \(\Diamond \) and \(\Box \) is only visible for the nondeterministic components of our programs, namely: (i) nondeterministic while; (ii) nondeterministic if; and (iii) memory allocation. It is only for these constructs that we need a specific symbolic execution rule for \(\Box \) and \(\Diamond \) properties. Incidentally, the difference between E properties and A properties is basically the same as the difference between \(\Diamond \) and \(\Box \), but extended to execution paths rather than individual steps. We also introduce faulting execution rules to allow us to prove that a program faults. The logical rules comprise rules for the standard logical connectives, analogous to those found in standard Hoare logic, and unfolding rules for the temporal operators and inductive predicates in memory assertions. The ( Cons ) rule is analogous to the rule of consequence in standard Hoare logic, appealing to entailment \(\vDash \) between symbolic heaps, and between CTL assertions. In particular, the (Unfold-Pre) rule performs a case-split on an inductive predicate in the precondition by replacing the predicate with the body of each clause of its inductive definition. For example, the inductive definition of the linked list segment predicate from Example 2 determines the following (Unfold-Pre) rule:Proofs in our system are cyclic proofs: standard derivation trees in which open subgoals can be closed either by applying an axiom or by forming a back-link to an identical interior node. To ensure that such structures correspond to sound proofs, a global soundness condition is imposed. The following definitions, adaptations of similar notions in e.g. [6‐9, 27], formalise this notion.

A pre-proof \({\mathcal {P}} = (\mathcal {D,L})\) can be seen as a finite cyclic graph by identifying each open leaf of \({\mathcal {D}}\) with its companion. A path in\({\mathcal {P}}\) is then simply a path in this graph with no further implications. It is easy to see that a path in a pre-proof corresponds to one or more paths in the execution of a program, interleaved with logical inferences.

We remark that CTL formulas with an outermost AF / EF quantifier never form part of a trace. Such properties, which express that something will eventually happen, are typically proven by appealing to an infinite descent in the precondition. To this end, we also introduce precondition traces as employed in [7]. Roughly speaking, a precondition trace tracks an occurrence of an inductive predicate in the preconditions of the judgements along the path, progressing whenever the predicate occurrence is unfolded.

While admittedly not the most interesting program in itself, the following simple example has been designed to illustrate complex cycle structures that arise from the nesting of temporal operators to provide a non-trivial satisfaction of the soundness condition.

For a more realistic example, we now present a proof of a heap-aware server program that nondeterministically alternates between adding an arbitrary number of “job requests” to the head of a linked-list and processing job requests by means of deleting them from the list.

We now show that our proof system is sound.

We remark that the dichotomy between inductive and coinductive arguments can be discerned in our trace condition. Coinductive (G) properties need to show that something happens infinitely often whereas inductive (F) properties have to show that something cannot happen infinitely often. Both cases give us a progress condition: for coinductive properties, we essentially need infinite program progress on the right of judgements, whereas for inductive properties we need an infinite descent on the left of judgements (or the proof to be finite).

Readers familiar with Hoare-style proof systems might wonder about relative completeness of our system, i.e., whether all valid judgements are derivable if all valid entailments between formulas are derivable. Typically, such a result might be established by showing that for any program C and temporal property \(\varphi \), we can (a) express the logically weakest precondition for C to satisfy \(\varphi \), say \(wp(C,\varphi )\), and (b) derive \(wp(C,\varphi ) \vdash C : \varphi \) in our system. Relative completeness then follows from the rule of consequence, (Cons). Unfortunately, it seems certain that such weakest preconditions are not expressible in our language. For example, in [7], the multiplicative implication of separation logic, , is needed to express weakest preconditions, whereas it is not present in our language due to the problems it poses for automation (a compromise typical of most separation logic analyses). Indeed, it seems likely that we would need to extend our precondition language well beyond this, since [7] only treats termination, whereas we treat arbitrary temporal properties. Since our focus in this paper is on automation, we leave such an analysis to future work.

These fairness constraints are usually categorised as weak and strong fairness [20]. However, since weak fairness requirements are usually restricted to the parallel composition of processes, a property that our programming language lacks, we limit ourselves to the treatment of strong fairness.

Note that every finite program execution is trivially fair. Also, for the purposes of fairness, we consider program commands to be uniquely labelled (to avoid confusion between different instances of the same command).

We now modify our cyclic CTL system to treat fairness constraints. First, we adjust the interpretation of judgements to account for fairness, then we lift the definition of fairness from program executions to paths in a pre-proof.

Intuitively, to account for fairness constraints, we simply need to restrict the global soundness condition from Definition 12 so that it quantifies over all fair infinite paths in a pre-proof, ignoring unfair paths. However, as it stands, this intuition is not quite correct. Consider the programUnder precondition \(x=1\), this program has the CTL property \(EG(x=1)\) owing precisely to the unfair execution that always favours the first branch of the nondeterministic if. We can witness this using a cyclic proof with a single loop that invokes the rule \((\text {If*}\Diamond \text {1})\) infinitely often. The infinite path created by this loop is unfair and thus such a proof should not count as a “fair” cyclic proof. However, if we simply ignore this infinite path, the only one in the pre-proof, then the global soundness condition is trivially satisfied! Our answer is to take a more subtle view of the roles played by existential \((EG/EF/\Diamond )\) and universal \((AG/AF/\Box )\) properties; unfair paths created by the former must be disallowed, whereas unfair paths created by the latter can simply be disregarded.

To illustrate the concepts introduced in this section, we show a fair cyclic CTL proof of the following example.

We implement our proof systems on top of the Cyclist [9], a mechanised cyclic theorem proving framework. The implementation, source code and benchmarks are publicly available at [1].

Our implementation performs iterative depth-first search, aimed at closing open nodes in the proof by either applying an inference rule or forming a back-link. If an open node cannot be closed, we attempt to apply symbolic execution; if this is not possible, we try unfolding temporal operators and inductive predicates in the precondition to enable symbolic execution to proceed. Forming back-links typically requires the use of the consequence rule (i.e. a lemma proven on demand) to re-establish preconditions altered by symbolic executions (as can be seen in Figs. 5 and 7). When forming a back-link, we check automatically that the global soundness condition is satisfied. Entailment queries over symbolic heaps in separation logic, which arise at backlinks and when applying the (Check) axiom or checking rule side conditions, are handled by a separate instantiation of \(\textsc {Cyclist }\) for separation logic entailments [9].

We evaluate the implementation on handcrafted nondeterministic and nonterminating programs similar to Example 1. Our test suite is essentially an adaptation of the model checking benchmarks in [14, 15] for temporal properties of nondeterministic programs. Roughly speaking, we replace operations on integer variables by analogous operations on heap data structures.

Our test suite comprises the following programs:

We show the results of the evaluation of the CTL system and its fair extension in Table 1. For each test, we report whether fairness constraints were needed to verify the desired property and the time taken in seconds (we use TO in case the tool failed to produce a proof within 60 seconds). The tests were carried out on an Intel x-64 i5 system at 2.50 GHz.

Our experiments demonstrate the viability of our approach: our runtimes are mostly in fractions of seconds and show similar performance to existing tools for the model checking benchmarks. Overall, the execution times in the evaluation are quite varied, as they depend on factors such as the complexity of the program and temporal property in question, but sources of potential slowdown can be witnessed by different test cases. Even at the level of pure memory assertions, the base case rule (Check) has to check entailments \(P \vDash Q\) between symbolic heaps, which involves calling an inductive theorem prover; this is reasonably fast in some cases, but very costly in others (e.g. the Append-List example). Another source of slowdown is in attempting to form back-links too eagerly (e.g. when encountering the same command at two different program locations); since we check soundness when forming a back-link, which involves calling a model checker (cf. [9]), this too is an expensive operation, as can be seen in the runtimes of test cases with suffix Branch.

Notwithstanding the broadly encouraging results, our implementation is not without limitations; in some cases, the proof search will fail to terminate. Some of this cases are due to the invalidity of the jugment that is intended to be demonstrated (as in is the case of Exmp, Fin-Lock and Nd-In-Lock) whereas in some other cases we fail to establish a sufficiently general “invariant” to form backlinks in the proof (the case of Inf-BinTree).

Related work on the automated verification of temporal program properties can broadly be classified into two main schools, model checking and deductive verification. In recent years, model checking has been the more popular of these two. Although earlier work in model checking focused on finite-state transition systems (e.g. [11, 25]), recent advances in areas such as state space restriction [3], precondition synthesis [13], CEGAR [15], bounded model checking [10] and automata theory [12] have enabled the treatment of infinite transition systems.

The present paper takes the deductive verification approach. In the realm of infinite state, previous proof systems for verifying temporal properties of arbitrary transition systems [23, 29] have shed some light on the soundness and relative completeness of deductive verification. Of particular relevance here are those proof systems for temporal properties based on cyclic proof.

Our work can be seen as an extension to arbitrary temporal properties of the cyclic termination proofs in Brotherston et al. [7]. A procedure for the verification of CTL* properties that employs a cyclic proof system for LTL as a sub-procedure was developed by Bath et al. [4]. A subtle but important difference when compared with our work is the lack of cut/consequence rule (used e.g. to generalise precondition formulas or to apply intermediary lemmas). A side benefit of this restriction is a simplification of the soundness condition on cyclic proofs.

A cyclic proof system for the verification of CTL* properties of infinite-state transition systems is presented in Sprenger’s PhD thesis [29]. Focusing on generality, this system avoids considering details of state formulas and their evolution throughout program execution by assuming an oracle for a general transition system. The system relies on a soundness condition that is similar to Definition 12, but does not track progress in the same way, imposing extra conditions on the order in which rules are applied. The success criterion for validity of a proof also presents some differences; it relies on finding ranking functions, intermediate assertions and checking for the validity of Hoare triples, and it is far from clear that such checks can be fully automated. In contrast, we rely on a relatively simple \(\omega \)-regular condition, which is decidable and can be automatically checked by \(\textsc {Cyclist }\) [5, 9, 30].

Our main contribution in this paper is the formulation, implementation and evaluation of a deductive cyclic proof system for verifying temporal properties of pointer programs, building on previous systems for separation logic and for other temporal verification settings [4, 7, 29]. We present two variants of our system and prove both systems sound. We have implemented these proof systems, and proof search algorithms for them, in the \(\textsc {Cyclist }\) theorem prover, and evaluated them on benchmarks drawn from the literature.

The main advantage of our approach is that we never obtain false positive results. This advantage is not in fact exclusive to deductive verification: some automata-theoretic model checking approaches are also proven to be sound [33]. Nonetheless, when compared to such approaches, our treatment of the temporal verification problem has the advantage of being direct. Owing to our use of separation logic and a deductive proof system, we do not need to apply approximation or transformations to the program as a first step; in particular, we avoid the translation of temporal formulas into complex automata [34] and the instrumentation of the original program with auxiliary constructs [12].

One natural direction for future work is to develop improved mechanised techniques, such as generalisation / abstraction, to enhance the performance of proof search in our system(s). Another possible direction is to consider larger classes of programs. In particular, concurrency is one very interesting such possibility, perhaps building on existing verification techniques for concurrency in separation logic (e.g. [32]). A different direction to explore is the enrichment of our assertion language, for example to CTL* [17] or \(\mu \)-calculus [16]. The structure of CTL* formulas and their classification into path and state subformulas suggest a possible combination of our CTL system with an LTL system to produce a proof object composed of smaller proof structures (cf. [4, 29]). The encoding of CTL* into \(\mu \)-calculus [16] and the applicability of cyclic proofs for the verification of \(\mu \)-calculus properties (see e.g. [28]) hint at the feasibility of such an extension.