09.08.2019  Ausgabe 3/2020 Open Access
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
 Zeitschrift:
 Journal of Automated Reasoning > Ausgabe 3/2020
Wichtige Hinweise
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
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 memoryaware 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 heapaware 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.
Anzeige
Example 1
Consider a “server” program that, given an acyclic linked list with head pointer
\(\mathtt {x}\), nondeterministically alternates between adding an arbitrary number of “job requests” to the head of the list and removing all requests in the list:
×
Memory safety of this program can be proven using a simple numeric abstraction recording emptiness/nonemptiness of the list. Proving instead that throughout the program execution it is always possible for the heap to become empty, expressed in CTL as
\(AGEF(\mathsf {emp})\), requires a finer abstraction, recording the length of the list. However, such an abstraction is still not sufficient to prove shape analysis properties of the heap, say that the heap is always a nilterminating acyclic list from
x, expressed in CTL as
AG(
ls(
x,
nil)) (where
ls is the standard list segment predicate of
separation logic [
26]), because the information about acyclicity and head/tail pointer values is lost, begging the question: how to differentiate cyclic from acyclic lists using only their length?
\(\square \)
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 automatabased soundness checks, showing that temporal logic proof systems can indeed work in practice.
Anzeige
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 wellknown language for describing heap memory; in particular we also permit userdefined (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.
Our proof system is tailored to proving standard CTL program properties over separation logic assertions; subsequently, we show how to adapt this system to handle
fairness constraints, where nondeterministic branching may not unfairly favour one branch over another. We have also adapted our system to (fair) LTL properties, though we do not present this adaptation in this paper due to space constraints. The details of our LTL cyclic proof systems will appear in the first author’s forthcoming PhD thesis.
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.
2 Programs and Assertions
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 firstorder language of
expressions over
\(\textsf {Var}\).
Branching conditions
B and
commands
C 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
stackandheap 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, finitedomain function
\(h : \textsf {Loc} \rightharpoonup _{\text {fin}} (\textsf {Val}\ \textsf {List})\), mapping finitely many memory locations to
records, i.e. arbitrarylength 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
domaindisjoint 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 smallstep 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 reflexivetransitive closure of
\(\leadsto \). The special configuration
\(\mathsf {fault}\) is used to denote a memory fault, which results when a command tries to access nonallocated 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 \).
Remark 1
In temporal program verification, it is common to consider all program execution paths to be infinite, and all temporal operators to quantify over infinite paths. This can be achieved either (
i) by modifying programs to contain an infinite loop at every exit point, or (
ii) by modifying the operational semantics so that final configurations loop infinitely (i.e.
\(\langle \mathbf{skip } , {s} , {h} \rangle \leadsto \langle \mathbf{skip } , {s} , {h} \rangle \)).
Here, instead, our temporal assertions quantify over paths that are either infinite or else maximally finite. This has the same effect as directly modifying programs or their operational semantics, but seems to us slightly cleaner.
An
execution tree, arising from the nondeterministic and branching nature of program executions, is a directed rooted tree in which any two vertices are connected by an execution path.
Memory state assertions We express properties of memory states (
s,
h) using a standard
symbolicheap fragment of separation logic (cf. [
2]) extended with userdefined (inductive) predicates, typically used to express data structures in the memory.
We assume a fixed firstorder
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}}\).
Definition 1
A
symbolic heap is given by a disjunction of assertions each of the form
\(\varPi : \varSigma \), where
\(\varPi \) is a finite set of
pure formulas of the form
\(E = E\) or
\(E \ne E\), and
\(\varSigma \) is a
spatial formula given by the following grammar:
where
E ranges over expressions,
\(\mathbf {E}\) over tuples of expressions and
\(\varPsi \) over predicate symbols (of arity matching the length of
\(\mathbf {E}\) in
\(\varPsi (\mathbf {E})\)). A
symbolic heap singleton is a symbolic heap composed of a single assertion.
$$\begin{aligned} \varSigma {:}{:}= \mathsf {emp}\mid E \mapsto \mathbf {E} \mid \varSigma *\varSigma \mid \varPsi (\mathbf {E}) , \end{aligned}$$
Definition 2
The satisfaction relation
\(s,h \vDash \phi \) between program states (
s,
h) and pure or spatial formulas
\(\phi \) is given inductively as follows:
where the definition of
\(\llbracket {\varPsi }\rrbracket ^\varPhi \), the interpretation of inductive predicate
\(\varPsi \) according to inductive definition(s)
\(\varPhi \), is given below. We extend satisfaction conjunctively from pure formulas to sets of pure formulas, and then to full symbolic heaps by
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].
Definition 3
(
Inductive definition) An
inductive definition of an inductive predicate symbol
\(\varPsi \) is a finite set of inductive rules, each of the form
\(\varPi :\varSigma \Rightarrow \varPsi (\mathbf {E})\), where
\(\varPi :\varSigma \) is a symbolic heap singleton and
\(\varPsi (\mathbf {E})\) is a predicate formula.
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.
Definition 4
(
Interpretation of inductive predicates) Let inductive definitions of predicate symbols
\(\mathbf {\varPsi }=(\varPsi _1, \ldots , \varPsi _n)\), with arities
\(a_1, \ldots , a_n\) respectively, be given. We may write the inductive definition for any such symbol, say
\(\varPsi _i\), in the form
We define a corresponding
nary function
\(\chi _i\) by
where
\(\mathbf {X}=(X_1,\ldots ,X_n)\) with each
\(X_i \subseteq \mathsf {Val}^{a_i} \times \mathsf {Heaps}\) and
s is an arbitrary stack and
\(\vDash _{\mathbf {X}}\) is exactly the satisfaction relation given above, except that
\(\llbracket {\varPsi _i}\rrbracket ^{\mathbf {X}} = X_i\). We then write
\(\llbracket {\varPsi _i}\rrbracket ^\varPhi \) for the
ith component of
\(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi = \mu \mathbf {X}.\ (\chi _1(\mathbf {X}), \ldots , \chi _n(\mathbf {X}))\).
$$\begin{aligned} \varPi _1 : \varSigma _1 \Rightarrow \varPsi _i(\mathbf {E}_1), \ldots , \varPi _k : \varSigma _k \Rightarrow \varPsi _i(\mathbf {E}_k)\ . \end{aligned}$$
$$\begin{aligned} \chi _i(\mathbf {X}) = \textstyle \bigcup _{1 \le j \le k}\ \{ (\llbracket {\mathbf {E}_j}\rrbracket s, h) \mid s,h \vDash _{\mathbf {X}} \varPi _j : \varSigma _j \} \end{aligned}$$
Example 2
Consider the following inductive definition for a binary inductive predicate symbol
ls denoting singlylinked list segments:
Then
\(\llbracket {ls}\rrbracket \) is the least (pre)fixed point of the following operator, which has domain and codomain
\(\mathrm {Pow}({\mathsf {Val}}^{2} \times \mathsf {Heaps})\):
$$\begin{aligned} \begin{array}{rcl} \mathsf {emp}&{}\Rightarrow &{} ls(x,x) \\ x \mapsto x' *ls(x',y) &{}\Rightarrow &{} ls(x,y) \end{array} \end{aligned}$$
$$\begin{aligned} \begin{array}{rcl} \chi _{\mathrm {ls}}(X) &{}=&{} \{((v,v),\mathsf {emp}) \mid v \in \mathsf {Val} \} \\ &{}\quad \cup &{} \{((v,v'), h_1 \uplus h_2) \mid \exists w.\ \mathsf {dom}(h_1) = {v} \text { and } h_1(v) = w \\ &{}&{} \qquad \text { and } ((w,v'),h_2) \in X \}\ . \end{array} \end{aligned}$$
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.
Definition 5
(Approximants) Let
\(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi \) be as given in Definition
4, and write
\(\chi (\mathbf {X}) = (\chi _1(\mathbf {X},\ldots ,\chi _k(\mathbf {X})\), so that
\(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi =\mu \mathbf {X}.\ \chi (\mathbf {X})\). Define a chain of ordinalindexed sets
\(\llbracket {\varvec{\varPsi }}\rrbracket ^{\alpha })_{\alpha \ge 0}\) by transfinite induction :
\(\llbracket {\varvec{\varPsi }}\rrbracket ^{\alpha } = \bigcup _{\beta < \alpha } \chi (\chi ^{\beta })\). Then, for each
\(i \in {1, \ldots , n}\), the set
\(\llbracket {\varvec{\varPsi }}\rrbracket ^{\alpha })\) is called the
\(\alpha \)th
approximant of
\(\llbracket {\varvec{\varPsi }}\rrbracket ^\varPhi \).
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.
Definition 6
CTL assertions are described by the following grammar:
where
P ranges over symbolic heaps (Definition.
1).
Note that
\(\mathsf {final}\) and
\(\mathsf {error}\) denote final, respectively faulting configurations.
×
Definition 7
A configuration
\(\gamma \) is a
model of the CTL assertion
\(\varphi \) if the relation
\(\gamma \vDash \varphi \) holds, defined by structural induction on
\(\varphi \) as follows:
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.
Definition 8
(Validity) A CTL judgement
\(P \vdash C \;:\varphi \) is
valid if and only if, for all memory states (
s,
h) such that
\(s,h \vDash P\), we have
\(\langle {C} , {s} , {h} \rangle \vDash \varphi \).
3 A Cyclic Proof System for Verifying CTL Properties
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 (UnfoldPre) rule performs a casesplit 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 (UnfoldPre) 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
backlink 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.
$$\begin{aligned} \frac{{{x=y,\varPi } \;:{\mathsf {emp}*F}} \vdash {C} \;:{\varphi } \quad \; {{\varPi } \;:{F *x \mapsto x' *ls(x',y)}} \vdash {C} \;:{\varphi }}{{{ \varPi } \;:{F *ls(x,y)}} \vdash {C} \;:{\varphi }} ( \text {UnfoldPre} ) \end{aligned}$$
Definition 9
(
Preproof) A
leaf of a derivation tree is called
open if it is not the conclusion of an axiom. A
preproof is a pair
\({\mathcal {P}} = (\mathcal {D,L})\), where
\({\mathcal {D}}\) is a finite derivation tree constructed according to the proof rules and
\({\mathcal {L}}\) is a
backlink function assigning to every open leaf of
\({\mathcal {D}}\) a
companion: an interior node of
\({\mathcal {D}}\) labelled by an identical proof judgement.
A preproof
\({\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 preproof corresponds to one or more paths in the execution of a program, interleaved with logical inferences.
To qualify as a proof, a cyclic preproof must satisfy a global soundness condition, defined using the notion of a
trace along a path in a preproof.
Definition 10
(
Trace) Let
\((J_i = P_{i} \vdash C_{i} :\varphi _{i})_{i \ge 0}\) be a path in a preproof
\({\mathcal {P}}\). The sequence of temporal formulas along the path,
\((\varphi _{i})_{i \ge 0}\), is a
\(\Box \)
trace (
\(\Diamond \)
trace) following that path if there exists a formula
\(\psi \) such that, for all
\(i \ge 0\):
We say that a trace
progresses whenever a symbolic execution rule is applied. A trace is
infinitely progressing if it progresses at infinitely many points.

the formula \(\varphi _i\) is of the form \(AG \psi \) ( \(EG \psi \)) or \(\Box AG \psi \) ( \(\Diamond EG \psi \)); and

\(\varphi _{i+1} = \varphi _i\) whenever \(J_i\) is the conclusion of (Cons).
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.
Definition 11
(
Precondition trace) Let
\((J_i = {P_{i}} \vdash {C_{i}} \;:{\varphi _{i}})_{i \ge 0}\) be a path in a preproof
\({\mathcal {P}}\). A sequence of inductive predicate formulas,
\((\varPsi _{i})_{i \ge 0}\), is a
precondition trace following that path
\((J_{i})_{i \ge 0}\) if
\(\varPsi _i\) occurs in
\(P_i\) for each
i and
We say that a precondition trace
progresses whenever (UnfoldPre) is applied. A precondition trace is
infinitely progressing if it progresses at infinitely many points.
(i)
whenever
\(J_i\) is the conclusion of the (UnfoldPre) rule, the predicate formula
\(\varPsi _i\) is the predicate in the spatial formula of
\(P_i\) being unfolded and
\(\varPsi _{i+1}\) is obtained in the premise
\(J_{i+1}\) by unfolding
\(\varPsi _i\); and
(ii)
\(\varPsi _i = \varPsi _{i+1}\) for all other rules, modulo any substitutions applied by rules (Assign), (Read), (Alloc
\(\Box \)), (Alloc
\(\Diamond \)) and (Subst). (For example, if the rule
\(( \text {Subst} )\) is applied with conclusion
\(J_i\) and substitution [
E /
x], then we must also have
\(\varPsi _i = \varPsi _{i+1}[E/x]\).)
Definition 12
(
Cyclic proof) A preproof
\({\mathcal {P}}\) is a
cyclic proof if it satisfies the following
global soundness condition: for every infinite path
\((P_{i} \vdash C_{i} :\varphi _{i})_{i \ge 0}\) in
\({\mathcal {P}}\), there is an infinitely progressing
\(\Box \)trace,
\(\Diamond \)trace or precondition trace following some tail
\((P_{i} \vdash C_{i} :\varphi _{i})_{i \ge n}\) of the path.
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 nontrivial satisfaction of the soundness condition.
Example 3
Consider the following program, where each atomic command is labelled with a program counter:
One can observe that, under the precondition
\(P = (x = 1)\), the program has the invariant property
\(\text{ AG(x } \text{= } \text{1) }\), since the assignment command on line 2 does not break the invariant and the variable will not be updated throughout the rest of the program execution. Moreover, since there exists at least one program execution in which the invariant holds, the program satisfies the formula
\(EG AG (x=1)\).
×
Figure
3 shows the proof of this property in our system, including the six cycles that are formed during the proof search, with traces that follow the infinite paths. For the rightmost cycle in the lower branch of the figure we note that the temporal components of the sequents in the infinite proof path are all of the form
\(EG \psi \) or
\( \Diamond EG \psi \), where
\(\psi = AG (x=1)\), so that there is a
\(\Diamond \)trace following the proof path as per Definition
10. Moreover, due to the application of symbolic execution rules
\(( \text {Wh} )\) and
\(( \text {Skip} )\) along the infinite proof path, the trace progresses infinitely often. Similarly, for the leftmost cycle in the top branch of the figure, we note that the temporal components of the sequents in the infinite proof path are of the form
\(AG \psi \) or
\(\Box AG \psi \), where
\(\psi = (x=1)\), so that there is a
\(\Box \)trace following the proof path. Moreover, due to the application of symbolic execution rules
\(( \text {Wh} )\) and
\(( \text {Skip} )\) along the infinite proof path, the trace progresses infinitely often. Contrary to the previous two cycles, the remaining 4 backlinks shown in the proof do not match their corresponding leaf node to a direct ancestor. Nevertheless, these infinite paths are, too, followed by
\(\Box \)traces that progress infinitely often. Consequently, our preproof qualifies as a valid cyclic proof.
\(\square \)
×
×
For a more realistic example, we now present a proof of a heapaware server program that nondeterministically alternates between adding an arbitrary number of “job requests” to the head of a linkedlist and processing job requests by means of deleting them from the list.
Example 4
Consider the following serverlike program
C from Example
1 in the Introduction, restated here with line numbers for convenience:
First we show that, given that the heap is initially a linked list from
\(\mathtt {x}\) to
\(\mathsf {nil}\), it is possible for the heap to become empty when running the program. Writing
\(C_i\) for the program from line
i, this property is expressed as the judgement
\(ls(x,nil) \vdash C_1:EF(\mathsf {emp})\). We show a cyclic proof of this property in Fig.
4, relying on a precondition trace over
ls(
x,
nil), which is unfolded during the proof.
×
Using this proof as a lemma, we can then show that it is
always possible for the heap to become empty at any point during program execution:
\(ls(x,nil) \vdash C_1: AG EF(\mathsf {emp})\). Essentially, given the above lemma, the remaining proof burden consists in showing that line 1 is reachable from any other program point. Figure
5 shows an outline cyclic proof of this judgement in our system (we suppress the internal judgements for space reasons, but show the cycle structure and rule applications). Note that the backlinks depicted in blue all point to a companion in the proof of our auxiliary lemma, and do not yield any new infinite paths. The red backlinks do give rise to new infinite paths; one can see that the preproof qualifies as a valid cyclic proof since there is an infinitely progressing
\(\Box \)trace along every one of these paths.
\(\square \)
×
Proposition 1
(Decidable soundness condition) It is decidable whether a preproof is a cyclic proof.
Proof
(Sketch) Given a preproof
\({\mathcal {P}}\), we construct two Büchi automata over strings of nodes of
\({\mathcal {P}}\). The first automaton
\(B_1\) accepts all infinite paths of
\({\mathcal {P}}\). The second automaton
\(B_2\) accepts all infinite paths of
\({\mathcal {P}}\) such that an infinitely progressing
\(\Box \),
\(\Diamond \) or preconditiontrace exists on some tail of the path. We then simply check
\({\mathcal {L}}(B_1) \subseteq {\mathcal {L}}(B_2)\), which is decidable.
\(\square \)
We now show that our proof system is sound.
Lemma 1
Let
\(J = (P \vdash C :\varphi )\) be the conclusion of an instance of a proof rule
R. If
J is invalid under (
s,
h), then there exists a premise of the rule
\(J' = P' \vdash C' : \varphi '\) and a model
\((s',h')\) such that
\(J'\) is not valid under
\((s',h')\) and, furthermore,
1.
if there is a
\(\Box \)trace following the edge
\((J, J')\) then, letting
\(\psi \) be the subformula of
\(\varphi \) given by Definition
10, there is a configuration
\(\gamma \) such that
\(\gamma \not \vDash \psi \), and the finite execution path
\(\pi ' = \langle {C'} , {s'} , {h'} \rangle \ldots \gamma \) is welldefined and a subpath of
\(\pi = \langle {C} , {s} , {h} \rangle \ldots \gamma \). Therefore
\(\mathrm {length}(\pi ') \le \mathrm {length}(\pi )\). Moreover,
\(\mathrm {length}(\pi ') < \mathrm {length}(\pi )\) when
R is a symbolic execution rule.
2.
if there is a
\(\Diamond \)trace following the edge
\((J,J')\) then, letting
\(\psi \) be the subformula of
\(\varphi \) given by Definition
10, there is a smallest finite execution tree
\(\kappa \) with root
\(\langle {C} , {s} , {h} \rangle \), each of whose leaves
\(\gamma \) satisfies
\(\gamma \not \vDash \psi \). Moreover,
\(\kappa \) has a subtree
\(\kappa '\) with root
\(\langle {C'} , {s'} , {h'} \rangle \) and whose leaves are all leaves of
\(\kappa \). Therefore
\(\mathrm {height}(\kappa ') \le \mathrm {height}(\kappa )\). Moreover,
\(\mathrm {height}(\kappa ') < \mathrm {height}(\kappa )\) when
R is a symbolic execution rule.
3.
if there is a precondition trace
\((\varPsi (\mathbf {E}),\varPsi '(\mathbf {E'}))\) following the edge
\((J,J')\) then letting
\(\alpha \) (
\(\beta \)) be the index of the least approximant for which the inductive predicate
\(\varPsi (\mathbf {E})\) (
\(\varPsi '(\mathbf {E'})\)) is interpreted (i.e.
\((s,h_0) \vDash \varPsi ^\alpha (\mathbf {E})\) and
\((s',h'_0) \vDash \varPsi '^{\beta }(\mathbf {E'})\) for subheaps
\(h_0\) of
h and
\(h'_0\) of
\(h'\)), then
\(\alpha ,\beta \) are well defined and
\(\beta \le \alpha \). Moreover
\(\beta < \alpha \) when
R is the (UnfoldPre) rule.
Proof
We distinguish a case for each proof rule. Due to space constraints, we show only a few interesting cases: the symbolic execution rules
\((\text {If*}\Diamond \text {1})\) and
\((\text {If*}\Box )\), which provide progress for
\(\Diamond \) and
\(\Box \)traces respectively, and the unfolding rule (UnfoldPre), which provides progress for precondition traces.
Case (If*
\(\Diamond 1\))
Assume the conclusion of the rule is invalid. Pick an arbitrary program state such that
\((s,h) \vDash P\) but
\(\gamma = \langle {\mathbf{if \;{*}\;\mathbf then \;{C_1}\;\mathbf else \;{C_2}\;\mathbf fi } \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \Diamond \varphi \). By Definition
7, if
\(\gamma \not \vDash \Diamond \varphi \) then for all
\(\gamma '\) such that
\(\gamma \leadsto \gamma ', \gamma ' \not \vDash \varphi \). By the operational semantics of our programming language we know that there are two possible transitions:
\(\gamma \leadsto \langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \) and
\(\gamma \leadsto \langle {{C_2} \text { ; } {C_3}} , {s} , {h} \rangle \). Hence,
\(\langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \varphi \) and
\(\langle {{C_2} \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \varphi \). Consequently, since by our assumption
\((s,h) \vDash P\) but
\(\langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \varphi \) then the premise is invalid.
$$\begin{aligned} \frac{{P} \vdash {{C_1} \text { ; } {C_3}} \;:{\varphi }}{{P} \vdash {(\mathbf{if \;{*}\;\mathbf then \;{C_1}\;\mathbf else \;{C_2}\;\mathbf fi } \text { ; } {C_3})} \;:{\Diamond \varphi }}(\text {If*}\Diamond \text {1}) \end{aligned}$$
Given the structure of the temporal formula
\(\varphi /\Diamond \varphi \), there cannot be a
\(\Box \)trace following the edge.
If there is a
\(\Diamond \)trace following the edge, then by Definition
10,
\(\varphi = EG\psi \). Since
\(\gamma \not \vDash EG\psi \), by Definition
7 we know that for all paths
\(\pi '\) starting from
\(\gamma \) there exists
\({\bar{\gamma }} \in \pi \) such that
\({\bar{\gamma }} \not \vDash \psi \). In other words, there is a finite execution tree
\(\kappa \) with root
\(\gamma \) and whose leaves all fail to satisfy
\(\psi \). Moreover, since
\(\gamma \leadsto \langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \) by the operational semantics, there is a maximal subtree
\(\kappa '\) of
\(\kappa \) with root
\(\langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \) and whose leaves also all fail to satisfy
\(\psi \). Clearly
\(\mathrm {height}(\kappa ') < \mathrm {height}(\kappa )\).
Finally, if there is a precondition trace
\((\varPsi (\mathbf {E}),\varPsi '(\mathbf {E}))\) following the edge then
\(\varPsi (\mathbf {E})=\varPsi '(\mathbf {E'})\) by Definition
11. Since
\((s,h) \vDash P\) and
\(\varPsi (\mathbf {E})\) is a predicate formula in
P, we have
\((s,h_0) \vDash \varPsi (\mathbf {E})\) for some subheap
\(h_0\) of
h. Therefore a smallest approximant
\(\alpha \) such that
\((s,h_0)\vDash \varPsi ^\alpha (\mathbf {E})\). Since here our
\((s',h')\) is just (
s,
h) and our
\(\varPsi '(\mathbf {E'})\) is just
\(\varPsi (\mathbf {E})\), we trivially have the required
\(\beta =\alpha \le \alpha \).
Case (If*
\(\Box \))
Assume the conclusion of the rule is invalid. Pick an arbitrary program state such that
\((s,h) \vDash P\) but
\(\gamma = \langle {\mathbf{if \;{*}\;\mathbf then \;{C_1}\;\mathbf else \;{C_2}\;\mathbf fi } \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \Box \varphi \). By Definition
7, if
\(\gamma \not \vDash \Box \varphi \) then there exists
\(\gamma '\) such that
\(\gamma \leadsto \gamma '\) and
\(\gamma ' \not \vDash \varphi \). By the operational semantics we know that there are two possibilities:
\(\gamma ' = \langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \) or
\(\gamma ' = \langle {{C_2} \text { ; } {C_3}} , {s} , {h} \rangle \). Hence, either
\(\langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \varphi \) or
\(\langle {{C_2} \text { ; } {C_3}} , {s} , {h} \rangle \not \vDash \varphi \). We show the first of these cases, the second being similar.
$$\begin{aligned} \frac{{P} \vdash {{C_1} \text { ; } {C_3}} \;:{\varphi } \quad {P} \vdash {{C_2} \text { ; } {C_3}} \;:{\varphi }}{{P} \vdash {(\mathbf{if \;{*}\;\mathbf then \;{C_1}\;\mathbf else \;{C_2}\;\mathbf fi } \text { ; } {C_3})} \;:{\Box \varphi }}(\text {If*}\Box ) \end{aligned}$$
Case
\(\gamma ' = \langle {{C_1} \text { ; } {C_3}} , {s} , {h} \rangle \).
By our assumption
\((s,h) \vDash P\) and invalidity result
\(\gamma ' \not \vDash \varphi \) then it is the case that the leftmost premise is invalid.
If there is a
\(\Box \)trace following the edge, then by Definition
10,
\(\varphi = AG\psi \). Furthermore, since
\(\gamma ' \not \vDash AG\psi \), then by Definition
7 we know that there exists
\({\bar{\gamma }}\) such that
\(\gamma ' \leadsto ^{*} {\bar{\gamma }}\) and
\({\bar{\gamma }} \not \vDash \psi \) (call this path
\(\pi '\)). Finally, since by the operational semantics
\(\gamma \leadsto \gamma '\), then
\(\pi '\) is a subpath of
\(\pi \) from
\(\gamma \) to
\(\gamma {\lnot }\), and moreover
\(\mathrm {length}(\pi ') < \mathrm {length}(\pi )\).
Given the structure of the temporal formula
\(\varphi /\Box \varphi \), there cannot be a
\(\Diamond \)trace following either of the edges.
The situation for precondition traces is similar to the previous case.
Case (UnfoldPre)
Assume the conclusion of the rule is invalid. Pick an arbitrary program state such that
\((s,h) \vDash {\varPi } \;:{\varPsi (\mathbf {E}) *\varSigma }\) but
\(\langle {C} , {s} , {h} \rangle \not \vDash \varphi \). By Definition
2 we can split
h into two disjoint subheaps
\(h = h' \uplus h''\) so that
\((s,h') \vDash {\varPi } \;:{\varPsi (\mathbf {E})}\) and
\((s,h'') \vDash {\varPi } \;:{\varSigma }\). Since
\((s,h') \vDash {\varPi } \;:{\varPsi (\mathbf {E})}\) then by Definition
2 we know that
\((\llbracket {\mathbf {E}}\rrbracket s,h') \in \llbracket {\varPsi }\rrbracket \). Moreover, by Definition
5 we know that the program state
\((s,h')\) is in the
\(\alpha \)th approximant of
\(\varPsi \) for some smallest
\(\alpha \) (i.e.
\((\llbracket {\mathbf {E}}\rrbracket s,h') \in \llbracket {\varPsi }\rrbracket ^{\alpha }\)). By construction of the definition set operator for
\(\varPsi \) (Definition
4), it follows that there is some inductive rule
\(\varPi _j : \varSigma _j \Rightarrow \varPsi (\mathbf {E}))\) such that
\((s,h') \vDash \varPi _j : \varSigma _j\) (we ignore variable renaming issues for simplicity). We choose
\(J_{i+1}\) to be the
jth premise of the rule,
\(\varPi \cup \varPi _j :\varSigma *\varSigma _j \vdash C \;:\varphi \), and our falsifying state to be (
s,
h). It follows that
\((s,h) \vDash \varPi \cup \varPi _j :\varSigma *\varSigma _j\), and so the premise
\(J_{i+1}\) is not valid, as required.
$$\begin{aligned} \frac{(\varPi \cup \varPi _i' :\varSigma *\varSigma _i' \vdash C \;:\varphi )_{1 \le i \le k}}{\varPi :\varPsi (\mathbf {E}) *\varSigma \vdash C \;:\varphi }( \text {UnfoldPre} ) \end{aligned}$$
If there is a
\(\Box \)trace following the edge
\((J_i,J_{i+1})\), then by Definition
10,
\(\varphi = AG\psi \) or
\(\varphi =\Box AG\psi \). Furthermore, since by our previous invalidity result
\(\langle {C} , {s} , {h} \rangle \not \vDash \varphi \), then by Definition
7 we know that there exists
\({\bar{\gamma }}\) such that
\(\langle {C} , {s} , {h} \rangle \leadsto ^{*} {\bar{\gamma }}\) and
\({\bar{\gamma }} \not \vDash \psi \) (call this path
\(\pi \)). Thus the paths
\(\pi '=\pi \) in item 1 of the lemma are well defined and, trivially,
\(\mathrm {length}(\pi ') \le \mathrm {length}(\pi )\).
If there is a
\(\Diamond \)trace following the edge
\((J_i,J_{i+1})\), then by Definition
10,
\(\varphi = EG\psi \) or
\(\varphi =\Diamond EG\psi \). Furthermore, since by our previous invalidity result
\(\langle {C} , {s} , {h} \rangle \not \vDash \varphi \), then by Definition
7 we know that for all paths
\(\pi \) starting from
\(\langle {C} , {s} , {h} \rangle \) there exists a configuration
\({\bar{\gamma }} \in \pi \) such that
\({\bar{\gamma }} \not \vDash \psi \) (call this tree
\(\kappa \). Thus the trees
\(\kappa =\kappa '\) in item 2 of the lemma are welldefined and, trivially,
\(\mathrm {height}(\kappa ') \le \mathrm {height}(\kappa )\).
If there is a precondition trace
\((\varPsi (\mathbf {E}),\varPsi '(\mathbf {E'}))\) following the edge then
\(\varPsi '(\mathbf {E'})\) is an unfolding of
\(\varPsi (\mathbf {E})\) appearing in
\(\varSigma _j\). Since
\((\llbracket {\mathbf {E}}\rrbracket s,h') \in \llbracket {\varPsi }\rrbracket ^{\alpha }\), it follows that
\((\llbracket {\mathbf {E'}}\rrbracket s,h_0) \in \llbracket {\varPsi '}\rrbracket ^\beta \) for some subheap
\(h_0\) of
\(h'\) and some approximant
\(\beta < \alpha \). This completes the case.
\(\square \)
Theorem 1
(Soundness) If
\(P \vdash C:\varphi \) is provable, then it is valid.
Proof
Suppose for contradiction that there is a cyclic proof
\({\mathcal {P}}\) of
\(J=P \vdash C:\varphi \) but
J is invalid. That is, for some stack
s and heap
h, we have
\((s,h) \vDash P\) but
\(\langle {C} , {s} , {h} \rangle \not \vDash \varphi \). Then, by local soundness of the proof rules (Lemma
1), we can construct an infinite path
\((P_i \vdash C_i :\varphi _i)_{i \ge 0}\) in
\({\mathcal {P}}\) of invalid judgements. Since
\({\mathcal {P}}\) is a cyclic proof, by Definition
12 there exists an infinitely progressing trace following some tail
\((P_{i} \vdash C_{i} :\varphi _{i})_{i \ge n}\) of this path.
If this trace is a
\(\Box \)trace, using condition 1 of Lemma
1, we can construct an infinite sequence of finite paths to a
fixed configuration
\(\gamma \) of infinitely decreasing length, contradiction. If the trace is a
\(\Diamond \)trace, we can construct an infinite sequence of execution trees (whose leaves are again fixed configurations) of infinitely decreasing height, contradiction. Finally, a precondition trace yields an infinitely decreasing sequence of ordinal approximations of some inductive predicate, also a contradiction. The conclusion is that
\(P \vdash C:\varphi \) must be valid after all.
\(\square \)
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 Hoarestyle 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.
4 Fairness
An important component in the verification of reactive systems is a set of
fairness requirements to guarantee that no computation is neglected forever. In this section, we show how our cyclic proof system for CTL program properties can be adapted to incorporate such fairness constraints when verifying nondeterministic programs.
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.
Definition 13
(
Fair execution) Let
C be a program command and
\(\pi = (\pi _i)_{i \ge 0}\) a program execution. We say that
\(\pi \)
visits C infinitely often if there are infinitely many distinct
\(i \ge 0\) such that
\(\pi _i = \langle {C} , {\_\ } , {\_\ } \rangle \). A program execution
\(\pi \) is
fair for commands
\(C_i, C_j\) if it is the case that
\(\pi \) visits
\(C_i\) infinitely often if and only if
\(\pi \) visits
\(C_j\) infinitely often. Furthermore,
\(\pi \) is
fair for a program C if it is fair for all pairs of commands
\(C_i,C_j\) such that
C contains a command of the form
\(\mathbf if \;{*}\;\mathbf then \;{C_i}\;\mathbf else \;{C_j}\;\mathbf fi \) or
\(\mathbf{while \;{*}\;\mathbf do \;{C_i}\;\mathbf od } \text { ; } {C_j}\).
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).
Remark 2
One can argue that Definition
13 does not consider programs of the form
\(\mathbf while \;{*}\;\mathbf do \;{C_i}\;\mathbf od \). Whereas this program, being finite, would be considered fair, one can also imagine more involved scenarios with nested branching commands which difficult the establishment of a clear continuation for a
while command.
In these cases, we can see programs of the form
\(\mathbf while \;{*}\;\mathbf do \;{C_i}\;\mathbf od \) as having a noop continuation resulting in programs of the form
\(\mathbf{while \;{*}\;\mathbf do \;{C_i}\;\mathbf od } \text { ; } \mathbf{skip }\) to avoid confusion.
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 preproof.
Definition 14
(
Fair CTL judgement) A fair CTL judgement
\({P} \vdash _{\mathrm {f}} {C} \;:{\varphi }\) is
valid if and only if, for all memory states (
s,
h) such that
\(s,h \vDash P\), we have
\(\langle {C} , {s} , {h} \rangle \vDash _{\mathrm {f}} \varphi \), where
\(\vDash _{\mathrm {f}}\) is the satisfaction relation obtained from
\(\vDash \) in Definition
7 by interpreting the temporal operators as quantifying over
fair paths, rather than all paths. For example, the clause for
AG becomes
Definition 15
A path in a preproof
\((J_i = {P_{i}} \vdash _{\mathrm {f}} {C_{i}} \;:{\varphi _{i}})_{i \ge 0}\) is said to
visit C infinitely often if there are infinitely many distinct
\(i \ge 1\) such that
\(J_{i_{\mathrm {C}}} = C\) and the rule applied at
\(J_{i1}\) is a symbolic execution rule. A path in a preproof is
fair for commands
\(C_i, C_j\) if it is the case that
\((J_i)_{i \ge 0}\) visits
\(C_i\) infinitely often if and only if it visits
\(C_j\) infinitely often. Finally, the path is
fair for program
C iff it is fair for all pairs of commands
\(C_i,C_j\) such that
C contains a command of the form
\(\mathbf if \;{*}\;\mathbf then \;{C_i}\;\mathbf else \;{C_j}\;\mathbf fi \) or
\(\mathbf{while \;{*}\;\mathbf do \;{C_i}\;\mathbf od } \text { ; } {C_j}\).
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 preproof, ignoring unfair paths. However, as it stands, this intuition is not quite correct. Consider the program
Under 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 preproof, 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.
$$\begin{aligned} \mathtt{while\ (true)\ do\ \{\ if\ (*)\ then\ x:=1\ else\ x:=2\ \}\ od} . \end{aligned}$$
Definition 16
A preproof
\({\mathcal {P}}\) is
bad if there is an infinite path
\((J_i = {P_{i}} \vdash _{\mathrm {f}} {C_{i}} \;:{\varphi _{i}})_{i \ge 0}\) in
\({\mathcal {P}}\) such that, given a program point
C, the rule
\((\text {Wh*}\Diamond \text {1})\) or
\((\text {If*}\Diamond \text {1})\) is applied to infinitely many distinct
\(J_i\) such that
\(J_{i_{\mathrm {C}}} = C\) and
\((\text {Wh*}\Diamond \text {2})\) or
\((\text {If*}\Diamond \text {2})\) is applied to only finitely many distinct
\(J_i\) such that
\(J_{i_{\mathrm {C}}} = C\) or vice versa.
Definition 17
(
Fair cyclic proof) A preproof
\({\mathcal {P}}\) is a
fair cyclic proof if it is not
bad in the sense of Definition
16 above and, for every infinite
fair path
\(({P_{i}} \vdash _{\mathrm {f}} {C_{i}} \;:{\varphi _{i}})_{i \ge 0}\) in
\({\mathcal {P}}\), there is an infinitely progressing
\(\Box \)trace,
\(\Diamond \)trace or precondition trace following some tail
\(({P_{i}} \vdash _{\mathrm {f}} {C_{i}} \;:{\varphi _{i}})_{i \ge n}\) of the path.
Proposition 2
(Decidable soundness condition) It is decidable whether a preproof is a valid fair cyclic proof.
Proof
(Sketch) Given a preproof
\({\mathcal {P}}\), we first have to check that it is not
bad in the sense of Definition
16. This can be done using Büchi automata: given a particular program point
C, one can construct automata
\(B_1\) and
\(B_2\) accepting the infinite paths in
\({\mathcal {P}}\) such that
\((\text {Wh*}\Diamond \text {1})\) or
\((\text {If*}\Diamond \text {1})\), respectively
\((\text {Wh*}\Diamond \text {2})\) or
\((\text {If*}\Diamond \text {2})\) are applied infinitely often to
C. We simply check
\({\mathcal {L}}({\mathcal {A}}_{B_1}) \subseteq {\mathcal {L}}({\mathcal {A}}_{B_2})\) and
\({\mathcal {L}}({\mathcal {A}}_{B_2}) \subseteq {\mathcal {L}}({\mathcal {A}}_{B_1})\), which is decidable (repeating this exercise for each needed program point).
It just remains to check that there exists an infinitely progressing trace along every infinite fair path of
\({\mathcal {P}}\). The argument is similar to the argument for our nonfair cyclic proofs, except that instead of an automaton accepting all infinite paths of
\({\mathcal {P}}\) we now require one accepting only
fair infinite paths. This can be done using a
Streett automaton with an acceptance condition of conjuncts of the form
\((\mathrm {Fin}(i) \vee \mathrm {Inf}(j)) \wedge (\mathrm {Fin}(j) \vee \mathrm {Inf}(i))\) for each pair of fairness constraints (
i,
j). We are then done since Streett automata can be transformed into Büchi automata [
21].
\(\square \)
×
To illustrate the concepts introduced in this section, we show a fair cyclic CTL proof of the following example.
Example 5
Consider the following labelled program
C:
While the property
\(AF(x=\textit{false})\) fails for this program in general, it becomes true under the fairness constraint
\((C_3,C_4)\). Figure
6 shows an abridged proof of this property in our fair cyclic CTL proof system, where the application of a
\(\vee \) rule following each
\(( \text {AF} )\) rule has been omitted from the proof for brevity. Note the formation of a cycle on the leftmost branch, along which there is no trace. Whereas this cycle invalidates the general CTL soundness condition, it does not invalidate the
fair CTL soundness condition, since the path in question visits
\(C_{3}\) infinitely often but not
\(C_{4}\); hence it is
unfair as per Definition
15 (but not
bad in the sense of Definition
16). Hence, the fair global soundness condition is trivially satisfied as there are only finite fair paths in the preproof. Consequently, the preproof qualifies as a fair CTL cyclic proof.
\(\square \)
×
Example 6
We return to our server program from Examples
1 and
4. Suppose we wish to prove, not that it is always
possible for the heap to become empty, i.e.
\(AG EF(\mathsf {emp})\), but that the heap will
always eventually become empty, i.e.
\(AG AF(\mathsf {emp})\). While the program does
not satisfy this property in general, it
does satisfy the property under the assumption of fair execution, which prevents the second loop from being executed infinitely often without executing the first loop.
Figure
7 shows an abridged proof of this property in the our fair cyclic CTL proof system. Adding the fairness constraints relaxes the conditions under which backlinks can be formed. The backlinks depicted in green induce infinite paths with no valid trace. However, because these infinite paths are
unfair (and not
bad), they are not considered in the global soundness condition. Our preproof thus qualifies as a fair cyclic proof since along every
fair infinite path there is either a
\(\Box \)trace or a precondition trace progressing infinitely often.
\(\square \)
×
Theorem 2
(Soundness) If
\({P} \vdash _{\mathrm {f}} {C} \;:{\varphi }\) is provable, then it is valid.
Proof
(Sketch) Suppose for contradiction that there is a fair cyclic proof
\({\mathcal {P}}\) of
\(J={P} \vdash _{\mathrm {f}} {C} \;:{\varphi }\) but
J is invalid. That is, for some stack
s and heap
h, we have
\((s,h) \vDash P\) but
\(\langle {C} , {s} , {h} \rangle \not \vDash _{\mathrm {f}} \varphi \). Then, by local soundness of the proof rules, we can construct an infinite path
\(\varPi = ({P_i} \vdash _{\mathrm {f}} {C_i} \;:{\varphi _i})_{i \ge 0}\) in
\({\mathcal {P}}\) of invalid sequents. We have an infinitely progressing trace along this path and can thus obtain a contradiction exactly as in the proof of soundness for the standard system (Theorem
1) provided that
\(\varPi \) is
fair.
Suppose therefore that
\(\varPi \) is unfair for commands
\((C_i,C_j)\) say. We consider the case in which
C contains the command
\(\mathbf if \;{*}\;\mathbf then \;{C_i}\;\mathbf else \;{C_j}\;\mathbf fi \) and
\(\varPi \) visits
\(C_i\) infinitely often and
\(C_j\) only finitely often; the
while case is similar. Using Definition
15 we know that
\(\mathbf if \;{*}\;\mathbf then \;{C_i}\;\mathbf else \;{C_j}\;\mathbf fi \) itself is symbolically executed infinitely often on
\(\varPi \). It cannot be that
\((\text{ If }*\Diamond 1)\) is applied infinitely often and
\((\text{ If }*\Diamond 2)\) only finitely often on
\(\varPi \), since
\(\varPi \) would in that case be a
bad path, which is specifically excluded by Definition
16. Nor can it be that both rules are applied infinitely often, since in that case
\(\varPi \) would be fair for
\((C_i,C_j)\), contrary to assumption.
The only remaining possibility is that
\((\text{ If }*\Box )\) is applied infinitely often on
\(\varPi \). In that case it must be that
\(\varPi \) contains infinitely many occurrences of the left premise of the rule and only finitely many instances of the right premise (or vice versa). Hence the program execution underlying the preproof path
\(\varPi \) is also unfair. Since the satisfaction relation
\(\vDash _{\mathrm {f}}\) is restricted to fair program executions, this contradicts the assumption that
\(\langle {C} , {s} , {h} \rangle \not \vDash _{\mathrm {f}} \varphi \). (The full justification of this last step requires the observation that, in order to produce a
\(\Box \) infinitely often, the underlying temporal property must contain an outermost
AF or
AG quantifier.)
\(\square \)
5 Implementation and Evaluation
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 depthfirst search, aimed at closing open nodes in the proof by either applying an inference rule or forming a backlink. 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 backlinks typically requires the use of the consequence rule (i.e. a lemma proven on demand) to reestablish preconditions altered by symbolic executions (as can be seen in Figs.
5 and
7). When forming a backlink, 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:

Examples discussed in the paper are named Exmp;

FinLock  a finite program that acquires a lock and, once obtained, proceeds to free from memory the elements of a list and reset the lock;

InfLock wraps the previous program inside an infinite loop;

NdInLock is an infinite loop that nondeterministically acquires a lock, then proceeds to perform a nondeterministic number of operations before releasing the lock;

InfList is an infinite loop that nondeterministically adds a new element to the list or advances the head of the list by one element on each iteration;

InsertList has a nondeterministic if statement that either adds a single elements to the head of the list or deletes all elements but one, and is followed by an infinite loop;

AppendList appends the second argument to the end of the first argument;

CyclicList is a nonterminating program that iterates through a nonempty cyclic list;

InfBinTree is an infinite loop that nondeterministically inserts nodes to a binary three or performs a random walk of the three;

The programs named with Branch define a somewhat arbitrary nesting of nondeterministic if and while statements, aimed at testing the capability of the tool in terms of lines of code and nesting of cycles;

Finally we also cover sample programs taken from the Windows Update system ( Win Update), the backend infrastructure of the PostgreSQL database server ( PostgreSQL) and an implementation of the acquirerelease algorithm taken from the aforementioned benchmarks ( AcqRel).
Table 1
Experimental results. Time is listed in miliseconds. TO indicated the experiment failed to produce a proof in under 60 seconds
Program

Precondition

Property

Fairness

Time (s)


Exmp

ls(x,nil)

AGEF emp

No

2.43

Exmp

ls(x,nil)

AGAF emp

Yes

4.29

Exmp

ls(x,nil)

AGAF (ls(x,nil))

No

0.26

Exmp

ls(x,nil)

AGEG (ls(x,nil))

No

0.44

Exmp

ls(x,nil)

AF emp

Yes

0.77

Exmp

ls(x,nil)

AFEG emp

Yes

0.86

Exmp

ls(x,nil)

AGAF emp

No

TO

FinLock

l
\(\mapsto \)0 * ls(x,nil)

AF (l
\(\mapsto \)1 * emp)

No

0.20

FinLock

l
\(\mapsto \)0 * ls(x,nil)

AGAF(l
\(\mapsto \)1 * emp)

No

0.62

FinLock

l
\(\mapsto \)0 * ls(x,nil)

AGAF(l
\(\mapsto \)1 * emp
\(\wedge \)
\(\Diamond \)l
\(\mapsto \)0)

No

0.24

FinLock

l
\(\mapsto \)0 * ls(x,nil)

AF (l
\(\mapsto \)1 * ls(x,nil))

No

TO

InfLock

l
\(\mapsto \)0 * ls(x,nil)

AGAF(l
\(\mapsto \)1 * emp)

No

1.52

InfLock

l
\(\mapsto \)0 * ls(x,nil)

AGAF(l
\(\mapsto \)1 * emp
\(\wedge \)
\(\Diamond \)l
\(\mapsto \)0))

No

3.26

InfLock

d = f : l
\(\mapsto \)0 * ls(x,nil)

AG(d! = t
\(\vee \) AF (l
\(\mapsto \)1 * emp))

No

3.87

NdInfLock

l
\(\mapsto \)0

AF(l
\(\mapsto \)1)

Yes

0.15

NdInfLock

l
\(\mapsto \)0

AGAF(l
\(\mapsto \)1)

Yes

0.25

NdInfLock

l
\(\mapsto \)0

AF(l
\(\mapsto \)1)

No

TO

InfList

ls(x,nil)

AG ls(x,nil)

No

0.21

InfList

ls(x,nil)

AGEF x = nil

No

4.39

InfList

ls(x,nil)

AGAF x = nil

Yes

8.10

InsertList

ls(three,zero)

EF ls(five,zero)

No

0.14

InsertList

ls(three,zero)

AF ls(five,zero)

Yes

0.26

InsertList

ls(n,zero)

AGAF n! = zero

Yes

17.21

AppendList

ls(y,x) * ls(x,nil)

AF (ls(y,nil))

No

12.67

CyclicList

cls(x,x)

AG cls(x,x)

No

0.88

CyclicList

cls(x,x)

AGEG cls(x,x)

No

0.34

InfBinTree

x! = nil : bintree(x)

AGEG x! = nil

No

0.72

InfBinTree

x! = nil : bintree(x)

AGAF bintree(x)

No

TO

AFAG Branch

x
\(\mapsto \)zero

AFAG x
\(\mapsto \)one

No

1.80

EGAG Branch

x
\(\mapsto \)zero

EGAG x
\(\mapsto \)one

No

0.23

EGAF Branch

x
\(\mapsto \)zero

EGAF x
\(\mapsto \)one

No

15.48

EG
\(\Rightarrow \)
EF Branch

p = z
\(\wedge \) q = z : ls(z,n)

EG(p! = one
\(\vee \) EF q = one)

No

1.60

EG
\(\Rightarrow \)
AF Branch

p = z
\(\wedge \) q = z : ls(z,n)

EG(p! = one
\(\vee \) AF q = one)

Yes

5.33

AG
\(\Rightarrow \)
EG Branch

p = z
\(\wedge \) q = one : ls(z,n)

AG(p! = one
\(\vee \) EG q = one)

No

0.36

AG
\(\Rightarrow \)
EF Branch

p = z
\(\wedge \) q = one :u ls(z,n)

AG(p! = one
\(\vee \) EF q = one)

No

1.53

Acqrel

ls(zero,three)

AG(acq = 0
\(\vee \) AF rel! = 0)

No

1.25

Acqrel

ls(zero,three)

AG(acq = 0
\(\vee \) EF rel! = 0)

No

1.25

Acqrel

ls(zero,three)

EF acq! = 0
\(\wedge \) EF AG rel = 0

No

0.33

Acqrel

ls(zero,three)

AF AG rel = 0

Yes

0.42

Acqrel

ls(zero,three)

EF acq! = 0
\(\wedge \) EF EG rel = 0

No

0.25

Acqrel

ls(zero,three)

AF EG rel = 0

Yes

0.33

PostgreSQL

w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

AGAF w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

No

0.27

PostgreSQL

w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

AGEF w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

No

0.26

PostgreSQL

w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

EFEG w = false
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

No

0.44

PostgreSQL

w = true
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

EFAG w = false
\(\wedge \) s = s
\(^{\prime }\)
\(\wedge \) f = f
\(^{\prime }\)

No

0.77

Win Update

W! = nil : ls(W,nil)

AGAF W! = nil : ls(W,nil)

No

1.50

Win Update

W! = nil : ls(W,nil)

AGEF W! = nil : ls(W,nil)

No

1.00

Win Update

W! = nil : ls(W,nil)

EFEG W = nil : emp

No

3.60

Win Update

W! = nil : ls(W,nil)

AFEG W = nil : emp

Yes

3.70

Win Update

W! = nil : ls(W,nil)

EFAG W = nil : emp

No

3.15

Win Update

W! = nil : ls(W,nil)

AFAG W = nil : emp

Yes

4.16

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 x64 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
AppendList example). Another source of slowdown is in attempting to form backlinks too eagerly (e.g. when encountering the same command at two different program locations); since we check soundness when forming a backlink, 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,
FinLock and
NdInLock) whereas in some other cases we fail to establish a sufficiently general “invariant” to form backlinks in the proof (the case of
InfBinTree).
6 Related Work
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 finitestate 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 subprocedure 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 infinitestate 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].
7 Conclusions and Future Work
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 automatatheoretic 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.
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.