This paper presents an interactive proof method for the verification of temporal properties of concurrent systems based on symbolic execution. Symbolic execution is a well known and very intuitive strategy for the verification of sequential programs. We have carried over this approach to the interactive verification of arbitrary linear temporal logic properties of (infinite state) parallel programs. The resulting proof method is very intuitive to apply and can be automated to a large extent. It smoothly combines first order reasoning with reasoning in temporal logic. The proof method has been implemented in the interactive verification environment KIV and has been used in several case studies.
Compared to sequential programs, both the design and the verification of concurrent systems is more
difficult, mainly because the control flow is more complex. Particularly, for reactive systems, not only
the final result of execution but the sequence of output over time is relevant for system behavior. Finding
errors by means of testing strategies is limited, because, especially for interleaved systems, an
exponential amount of possible executions must be considered. The execution is nondeterministic, making
it difficult to reproduce errors. An alternative to testing is the use of formal methods to specify and
verify concurrent systems with mathematical rigor. Automatic methods – especially model checking –
have been applied successfully to discover flaws in the design and implementation of systems. Starting
from systems with finite state spaces of manageable size, research in model checking aims at mastering
ever more complex state spaces and to reduce infinite state systems by abstraction. In general, systems
must be manually abstracted to ensure that formal analysis terminates. An alternative approach to large
or infinite state spaces are interactive proof calculi. They directly address the problem of infinite state
spaces. Here, the challenge is to achieve a high degree of automation. Existing interactive calculi to
reason in temporal logic about concurrent systems are generally difficult to apply. The strategy of symbolic
execution, on the other hand, has been successfully applied to the interactive verification of sequential
programs (e.g. Dynamic Logic [
Combining Dynamic Logic and temporal logic has already been investigated, e.g. Process Logic [
Our logic is based on Interval Temporal Logic (ITL) [
A short overview of our logic is given in Section 2. The calculus for symbolic execution is described
in Section 3. The strategy has been implemented in KIV (see Section 4). Section 6 concludes. For more
details on the logic and calculus, especially on induction and double primed variables to decompose
proofs, we refer to [
Similar to [
p(e1, . . . , en) | ¬ ! | !1 ∧ !2 | ∃ v. ! | step | !1; !2 | ! ∗ | %A1, . . . , An& | !1 !< !2 Dynamic variables can be primed and double primed. It is possible to quantify both static and dynamic variables. The chop operator !1; !2 directly corresponds to the sequential composition of programs. The star operator !∗ is similar to a loop. We have added an operator %A1, . . . , An& to define an explicit frame assumption. Furthermore, operator !1 !< !2 can be used to interleave two “processes”. The basic operator !< gives precedence to the left process, i.e., a transition of !1 is executed first.
State: #0 # ! 0 #1 # ! 1 #2 # ! 2 #3 # ! 3 #4 Interval I: = system transition = environment transition
In ITL, an interval is considered to be a finite or infinite sequence of states, where a state is a mapping from variables to their values. In our setting, we introduce additional intermediate states #i! to distinguish between system and environment transitions. For intuition, compare the following to Figure 1. Let n ∈ N$. An interval
I = (#0,#0! ,#1, . . . ,#n!−1,#n) consists of an initial state #0, and a finite or infinite and possibly empty sequence of transitions (#i!,#i+1)in=−01. In the intermediate states #i! the values of the variables after a system transition are stored. The following states #i+1 reflect the states after an environment transition. In this manner, system and environment transitions alternate. An empty interval consists only of an initial state #0. Given an interval I, variables are evaluated as follows:
Static and unprimed dynamic variables are evaluated in the initial state. Primed variables are evaluated in #0! and double primed variables in #1. In the last state, i.e. if I is empty, the value of a primed or double primed variable is equal to the unprimed variable. It is assumed that after a system has terminated, the variables do not change.
The semantics of the standard ITL operators can be carried over one-to-one to our notion of an
interval, and is therefore omitted here. In [
I |= %A1, . . . , An& iff
#0! (A) = #0(A) for all A )∈ {A1, . . . , An}
The interleaving operator ! !< " interleaves arbitrary formulas ! and " . The two formulas represent sets of intervals. We have therefore defined the semantics of ! !< " relative to the interleaving [[I1 !< I2]] of two concrete intervals I1 and I2.
I |= ! !< " iff there exist I1, I2
with I ∈ [[I1 !< I2]] and I1 |= ! and I2 |= " For nonempty intervals I1 = (#0,#0! ,#1, . . . ), and I2 = (%0,%0! ,%1, . . . ), interleaving of intervals adheres to the following recursive equations.
[[I1 !< I2]] =
(#0,#0! ) ⊕ [[(#1, . . . ) ! I2]], if I1 is not blocked
(%0,%0! ) ⊕ [[(#1, . . . ) ! (%1, . . . )]], if I1 is blocked, #0 = %0
0/, otherwise
[[I1 " I2]] = [[I1 !< I2]] ∪ [[I2 !< I1]]
Interval I1 is blocked, if #0! (blk) )= #0(blk) for a special dynamic variable blk. The system transition
toggles the variable to signal that the process is currently blocked (see await statement below). If I1
is not blocked, then the first transition of I1 is executed and the system continues with interleaving the
remaining interval with I2. (Function ⊕ prefixes all of the intervals of a given set with the two additional
states.) If I1 is blocked, then a transition of I2 is executed instead. However, the blocked transition of I1
is also consumed. A detailed definition of the semantics can be found in [
Additional common logical operators can be defined as abbreviations. A list of frequently used abbreviations is contained in Table 1, where most of the abbreviations are common in ITL. The next operator comes in two flavors. The strong next ◦ ! requires that there is a next step satisfying ! , the weak next • ! only states that if there is a next step, it must satisfy ! .
As can be seen in Table 1, the standard constructs for sequential programs can be derived. Executing an assignment requires exactly one step. The value of e is “assigned” to the primed value of A. Other variables are unchanged (%A&). Note that for conditionals and loops, the condition " evaluates in a single more :≡ last :≡ inf :≡ finite :≡ step; true ¬ more true; false ¬ inf A := e :≡
skip :≡ if " then !1 else !2 ≡ while " do ! :≡ var A in ! :≡
bskip :≡ await ! do " :≡ await ! :≡ ! ! " :≡ ! ! :≡ " ! :≡ ◦ ! :≡ • ! :≡ finite; ! ¬ ! ¬ ! step; ! ¬ ◦ ¬ ! A! = e ∧ %A& ∧ step %& ∧ step " ∧ (skip; !1) ∨ ¬ " ∧ (skip; !2) ((" ∧ (skip; ! ))∗ ∧ " (last → ¬ " )); skip " A! = A ∧ ∃ A. ! ∧ " A!! = A! blk! )= blk ∧ %blk& ∧ step ((¬ ! ∧ bskip)∗ ∧ " (last → ! )); " await ! do skip ! !< " ∨ " !< ! step. For local variable definitions, the local variable is quantified (∃ A), in addition, the environment cannot access the local variable (" A!! = A!). The global value of the variable is unchanged (" A! = A).
Parallel programs communicate using shared variables. In order to synchronize execution, the operator await " do ! can be used. A special dynamic variable blk is used to mark whether a parallel program is blocked. The await operator behaves like a loop waiting for the condition to be satisfied. While the operator waits, no variable is changed except for variable blk which is toggled. In other words, a process guarded with an await operator actively waits for the environment to satisfy its condition. Immediately after condition " is satisfied, construct ! is executed. 3
Our proof method is based on a sequent calculus with calculus rules of the following form: Rules are applied bottom-up. Rule name refines a given conclusion & 0 ' with n premises &i 0 'i. We also rely heavily on rewriting with theorems of the form ! ↔ " . These allow to replace instances of ! with instances of " anywhere in a sequent. 3.1
Our proof strategy is symbolic execution of temporal formulas, parallel programs being just a special case thereof. In Dynamic Logic, the leading assignment of a DL formula 2v := e;( 3 ! is executed as follows: The sequential composition is normalized and is replaced with a succession of diamond operators. Afterwards, the assignment is “executed” to compute the strongest postcondition &vv0 , v = evv0 (The substitution &vv0 means that variable v is replaced with variable v0 in &). In our setting, we normalize all the temporal &vv0 , v = evv0 0 2( 3 ! asg r & 0 2v := e3 2( 3 ! & 0 2v := e;( 3 !
normalize ! , & 0 ' " , & 0 ' ! ∨ " , & 0 ' dis l
!aa0 , & 0 ' ∃ a. ! , & 0 ' %Aa,,Aa,!a,A!! 0 % , last 0 lst (a ∈/ free(% )) %Aa,1A,a!,2A,A!! ,! % , ◦ ! 0 ex l (a0 ∈/ free(! ) \ {a} ∪ free(&, '))
stp (a1, a2 ∈/ free(% ,! )) formulas of a given sequent by rewriting the formulas to a so called normal form which separates the possible first transitions and the corresponding temporal formulas describing the system in the next state. Afterwards, an overall step for the whole sequent is executed (see below). More formally, a program (or temporal formula) is rewritten to a formula of the following type
% ∧ ◦ ! where % is a predicate logic formula that describes a transition as a relation between unprimed, primed and double primed variables while ! describes what happens in the rest of the interval. A program may also terminate, i.e., under certain conditions, the current state may be the last. Furthermore, the next transition can be nondeterministic, i.e., different %i with corresponding !i may exist describing the possible transitions and corresponding next steps. Finally, there may exist a link between the transition %i and system !i which cannot be expressed as a relation between unprimed, primed, and double primed variables in the transition alone. This link is captured in existentially quantified static variables ai which occur in both %i and !i. The general pattern to separate the first transitions of a given temporal formula is %0 ∧ last ∨ % n
i=1(∃ ai. %i ∧ ◦ !i) .
3.2
Assume that the antecedent of a sequent has been rewritten to normal form. Further assume – to keep it simple – that the succedent is empty. (This can be assumed as formulas in the succedent are equivalent to negated formulas in the antecedent. Furthermore, several formulas in the antecedent can be combined to a single normal form.) With the two rules dis l and ex l of Table 2, disjunction and quantification can be eliminated. For the remaining premises, %0 ∧ last ∨ % n
i=1(∃ ai. %i ∧ ◦ !i) 0 %0 ∧ last 0 %i ∧ ◦ !i 0 the two rules lst and stp can be applied. If execution terminates, all free dynamic variables A – no matter, if they are unprimed, primed or double primed – are replaced by fresh static variables a. The result is a formula in pure predicate logic with static variables only, which can be proven with standard first order reasoning. Rule stp advances a step in the trace. The values of the dynamic variables A and A! in the old state are stored in fresh static variables a1 and a2. Double primed variables are unprimed variables in the next state. Finally, the leading next operators are discarded. The proof method now continues with the execution of !i. alw: ev: " ! ! ! ↔ ↔ ! ∧ • " ! ! ∨ ◦ ! ! The idea of symbolic execution can be applied to formulas of temporal logic. For example, operator " ! is similar to a loop in a programming language: formula ! is executed in every step. An appropriate rewrite rule is alw of Table 3. Formula ! must hold now, and in the next step " ! holds again. To arrive at a formula in normal form, the first conjunct of the resulting formula ! ∧ • " ! must be further rewritten. The rewrite rule above corresponds to the recursive definition of " ! . Other temporal operators can be executed similarly. 3.4
The execution of sequential composition of programs ! ; " is more complicated as we cannot give a simple equivalence which rewrites a composition to normal form. The problem is that the first formula ! could take an unknown number of steps to execute. Only after ! has terminated, we continue with executing " .
Rules for the execution of ! ; " are given in Table 4. In order to execute composition, the idea is to first rewrite formula ! to normal form &
' %0 ∧ last ∨ % (∃ ai. %i ∧ ◦ !i) ; " The first sub-formula ! can be rewritten with rule chp lem of Table4. If it is valid that !1 implies !2, then !1; " also implies !2; " . (This rule is a so-called congruence rule.) After rewriting the first sub-formula to normal form, we rewrite the composition operator. According to rules chp dis and chp ex, composition distributes over disjunction and existential quantification. If we apply these rules to the formula above, we receive a number of cases
(%0 ∧ last);" ∨ % ∃ ai,0. (%i,0 ∧ ◦ !i,0); " In the first case, program ! terminates, in the other cases, the program takes a step %i and continues with program !i. Rules chp lst and chp stp can be used to further rewrite the composition. Dynamic variables A stutter in the last step, and therefore the primed and double primed variables A! and A!! of % are replaced by the corresponding unprimed variables if the first sub-formula terminates. The two rules give %0AA,!A,A!! ∧ " ∨ % ∃ ai,0. %i,0 ∧ ◦ (!i,0; " ) 0 !1 → !2 0 !1 !< " → !2 !< "
ilvl lem ilvl dis: (!1 ∨ !2) !< " ↔ !1 !< " ∨ !2 !< " ilvl ex: (∃ a. ! ) !< " ↔ ∃ a0. !aa0 !< "
a0 fresh with respect to (free(! ) \ {a}) ∪ free(" ) ilvl lst: (% ∧ last) !< " ↔ %AA!,,AA!! ∧ " ilvl stp: (% ∧ ¬ blocked ∧ ◦ ! ) !< "
↔ ∃ a2. (%Aa!2! ∧ ¬ blocked ∧ ◦ ((A = a2 ∧ ! ) ! " )) ilvl blk: (% ∧ blocked ∧ ◦ ! ) !< "
↔ ∃ a2,1. (∃ a1. %Aa!1,,Aa!2!,1 ) ∧ (A = a2,1 ∧ ! ) !b< " In the first case, ! has terminated and we still need to execute " to arrive with a formula in normal form. In the other cases, we have successfully separated the formula into the first transition %i,0 and the corresponding rest of the program !i,0; " . As with sequential composition, the interleaving of programs cannot be executed directly, but the subformulas need to be rewritten to normal form first. The basic operator for interleaving is the left interleaving operator ! !< " which gives precedence to the left process. In order to execute !<, the first sub-formula must be rewritten to normal form before the operator itself can be rewritten.
For left interleaving, the rules of Table 5 are similar to the rules for sequential composition. Congruence rule ilvl lem makes it possible to rewrite the first sub-formula to normal form. Similar to chop, left interleaving also distributes over disjunction (ilvl dis) and existential quantifiers (ilvl ex). If the first formula terminates, execution continues with the second (ilvl lst). This is similar to rule chp lst. Otherwise, execution depends on the first process being blocked. If it is not blocked, rule ilvl stp executes the transition and continues with interleaving the remaining ! with " . Note that the double primed variables of % are replaced by static variables a2 which must be equal to the unprimed variables the next time a transition of the first process is executed. This is to establish the environment transition of the first process as a relation which also includes transitions of the second. If the first process is blocked, then rule ilvl blk executes the blocked transition; the process actively waits while being blocked. However, the primed variables of % are replaced by static variables a1: the blocked transition of the first process does not contribute to the transition of the overall interleaving. Instead, a transition of the other process is executed. ilvlb dis: " !b< (!1 ∨ !2) ↔ " !b< !1 ∨ " !b< !2 ilvlb ex: " !b< (∃ a. ! ) ↔ ∃ a0. " !b< !aa0
a0 fresh with respect to (free(! ) \ {a}) ∪ free(" ) ilvlb lst: " !b< (% ∧ last) ↔ false ilvlb stp: " !b< (% ∧ ◦ ! ) ↔ ∃ a2,2. %Aa!2!,2 ∧ ◦ (" ! (A = a2,2 ∧ ! )) use as Proof Lemma X = 1,Y = 2, (( ! ) ) 0 X = 1, (( ! Y := 2;) ) 0
X = 1,Y = 2, (( ! ) ) 0
Y = 2, (X := 1;( ! ) ) 0
X := 1;( ! Y := 2;) 0
The situation where the first process is blocked and it remains to execute a transition of the second process is represented by a derived operator ! !b< " which is defined ! !b< " :≡
(blocked ∧ ◦ ! ) !< " and for which the rules of Table 6 are applicable. Again, the rules are very similar to the rules above. A congruence rule ilvlb lem ensures that the second sub-formula can be rewritten to normal form. With rules ilvlb dis and ilvlb ex, the operator distributes over disjunction and existential quantification. If the second process terminates, ilvlb lst is applicable, otherwise ilvlb stp can be applied.
Similar rules have been defined for all the operators of our logic [
To prove programs with loops, an inductive argument is necessary. Just as for sequential progams, we use well-founded and structural induction over datatypes. A specific rule for temporal induction over the interval is unnecessary: if a liveness property ! ! is known, the equivalence
! ! ↔ ∃N. N!! = N − 1 until (N = 0 ∧ ! ) can be used to induce over the number of steps N it takes to reach the first state satisfying ! . To prove a safety property such a liveness property can be derived by using the equivalence " ! ↔ ¬ ! ¬ ! . The proof is then by contradiction, assuming there is a number N of steps, after which ! is violated.
Execution of interleaved programs often leads to the same sequent occurring in different branches of
the proof tree. Normally, the user would specify a lemma which can be applied to all these sequents. To
simplify this, we allow that a premise of the proof tree can automatically used as lemma to close another
goal. An example is shown in Figure 2. This generalisation of proof trees to (acyclic) proof graphs
allows the dynamic construction of verification diagrams [
The interactive proof method has been implemented in KIV [
We have successfully carried over the strategy of symbolic execution to verify arbitrary temporal properties for concurrent systems. The proof method is based on symbolic execution, sequencing, and induction. How to symbolically execute arbitrary temporal formulas – parallel programs being just a special case thereof – has been explained in this paper.
Our proof method is easily extendable to other temporal operators. For every operator, a set of rules
must be provided to rewrite the operator to normal form. With rules similar to the ones of Tables 4
and 5, we support in KIV operators for Dijkstra’s choice, synchronous parallel execution, and interrupts.
Furthermore, we have integrated STATEMATE state charts [
Using double primed variables, we have defined a compositional semantics for every operator
including interleaving of formulas. This allowed us to find a suitable assumption-guarantee theorem to
apply compositonal reasoning [
The implementation in KIV has shown that symbolic execution can be automated to a large extent.
We have applied the strategy to small and medium size case studies. Currently, the strategy is applied in a
European project called Protocure to verify medical guidelines which can be seen as yet another form of
concurrent system [