CS-550 Formal Verification

September 20, 2019

Throughout these notes, vectors are denoted in bold and lowercase (e.g. $x$ ). Booleans are denoted interchangeably by $true$ and $false$ , or $⊤$ and $⊥$ . Generally, I try to use $\to$ and $\leftrightarrow$ for formulas, and $⟹$ and $⟺$ for mathematical notation¹.

Transition systems
Propositional logic
Bounded model checking
Satisfiability checking
Linear Temporal Logic
- Definition
Binary Decision Diagrams
Interpolation-based model checking
LCF Approach to Formal Proofs
First order logic
Converting imperative programs to formulas
Hoare Logic
Properties of program contexts
- Properties of relations
- Properties of expressions
More on mapping programs to formulas
Quantifier elimination in Presburger arithmetic

Transition systems

Definition

We’ll start by introducing transition systems, a generalization of DFAs. They may be not finite, and not deterministic.

Definition: Transition system

A transition system is a 4-tuple $M = (S, I, r, A)$ where:

$S$ is the set of states
$I \subseteq S$ is the set of starting states
$r \subseteq S \times A \times S$ is the transition relation
$A$ is the alphabet

For $s, s^{'} \in S$ and $a \in A$ , $(s, a, s^{'}) \in r$ means that ther is a transition from $s$ to $s^{'}$ on input $a$ .

A few special cases of this general form exist:

If $S$ is finite, we have a finite state machine
If $r : S \times A \to S$ and $| I | = 1$ , then the system is deterministic.

Traces and reachability

Definition: Trace

A trace is a finite or infinite sequence, describing steps taken by a transition system:

(s_{0}, a_{0}, s_{1}, a_{1}, s_{2}, \dots)

where we require, $\forall i$ :

$s_{0} \in I$
$s_{i} \in S$
$a_{i} \in A$
$(s_{i}, a_{i}, s_{i + 1}) \in r$

A trace may or may not be finite. If they are finite, we can assume that the trace ends with a state $s_{n}$ . We’ll introduce some notation for traces:

Definition: Trace of a transition system

$Traces (M)$ is the set of all traces of a transition system $M = (S, I, r, A)$ , starting from $I$ .

Definition: Reachable states of a transition system

The reachable states are states for which there exists a trace that ends in $s_{n}$ :

Reach (M) = {s_{n} ∣ \exists n . \exists (s_{0}, a_{0}, s_{1}, a_{1}, \dots, s_{n}) \in Traces (M)}

To check for reachability, for a finite $S$ , we can simply run DFS.

Relations

Let’s study relations more closely. A relation is a directed edge in the transition graph. We follow this edge when we see a given input $a \in A$ .

If we look at the graph, we may not be interested in the inputs associated to each edge. Therefore, we can construct the edge set $¯ r$ :

¯ r := {(s, s^{'}) ∣ \exists a \in A . (s, a, s^{'}) \in r}

Generally, we’ll use a bar for relations that disregard input. Note that even when $r$ is deterministic, $¯ r$ can become non-deterministic.

Composition

Relations can be composed:

Definition: Composition of relations

_{1} \circ_{2} = {(x, z) ∣ \exists y . (x, y) \in_{1} \land (y, z) \in_{2}}

Note that composition is not commutative, but is associative.

To understand what a composition means, intuitively, we’ll introduce a visual metaphor. Imagine the nodes of the graph as airports, and the edges as possible routes. Let $_{1}$ be the routes operated by United Airlines, and $_{2}$ be the routes operated by Delta. Then $_{1} \circ_{2}$ is the set of routes possible by taking a United flight followed by a Delta flight.

Iteration

Definition: Iteration

An iteration ${¯ r}^{n}$ describes paths of length $n$ in a relation $¯ r$ . It is defined recursively by:

\begin{matrix} {¯ r}^{0} & := Δ {¯ r}^{n + 1} & := ¯ r \circ {¯ r}^{n} \end{matrix}

Identity

In the above, $Δ$ describes the identity relation, i.e. a relation mapping every node to itself. We’ll see a small generalization below, which will be useful for the rest of the course:

Definition: Identity relation

The identity relation $Δ$ (also called “diagonal relation” or “triangular relation”) is the relation mapping every item in the universe $S$ to itself:

Δ = {(x, x) ∣ x \in S}

This relation can be conditioned, so as to only include elements in a set $A$ (or satisfying a condition $A$ ):

Δ_{A} = {(x, x) ∣ x \in A}

Transitive closure

Applying iteration an arbitrary number of times leads us to the transitive closure:

Definition: Transitive closure

The transitive closure ${¯ r}^{*}$ of a relation $¯ r$ is:

{¯ r}^{*} = ⋃ n \geq 0 {¯ r}^{n}

In our airport analogy, the transitive closure is the set of all airports reachable from our starting airports.

A few properties of transitive closure follow from the definition:

Reflexivity: $Δ \subseteq r^{*}$ , so every item is mapped back onto itself (among others, potentially)
Transitivity: $(a, b) \in r^{*} \land (b, c) \in r^{*} ⟹ (a, c) \in r^{*}$
Distributivity (under certain conditions): if $s$ is reflexive and transitive and $r \subseteq s$ , then $r^{*} \subseteq s$
Monotonicity: $r_{1} \subseteq r_{2} ⟹ r_{1}^{*} \subseteq r_{2}^{*}$

A few bonus facts:

$r^{*}$ is the smallest reflexive transitive relation containing $r$ .
${(r^{- 1})}^{*} = (r^{*})^{- 1}$
$r^{*} = Δ \cup (r \circ r^{*})$
$r^{*} = Δ \cup (r^{*} \circ r)$
An edge is in the transitive closure if and only if there is a path in the graph $r$ . In mathematical notation, this is:
$(x_{0}, x_{n}) \in r^{*} ⟺ \exists n \geq 0. \exists x_{1}, \dots, x_{n - 1} . \forall i \in {0, \dots, n - 1} . (x_{i}, x_{i + 1}) \in r$

Image

Finally, we’ll introduce one more definition:

Definition: Image of a set

The image $¯ r [X]$ of a state set $X$ under a relation $¯ r$ is the set of states reachable in one step from $X$ :

¯ r [X] := {y ∣ \exists x \in X . (x, y) \in ¯ r}

We also introduce an alternative notation:

X ∙ ¯ r := ¯ r [X]

The alternative notation may make it simpler to read images; $(X ∙_{1}) ∙_{2}$ can be read as “ $X$ following $_{1}$ then following $_{2}$ ”.

Reach

The above definitions lead us to a first definition of reach:

Theorem: Definition 1 of reach

Reach (M) = (¯ r)^{*} [I]

Post

We’ll introduce another definition in order to give an alternative definition of reach. We’re still considering a state system $M = (S, I, r, A)$ .

Definition: Post

If $X \subseteq S$ , define:

post (X) = ¯ r [X]

We also define:

\begin{matrix} {post}^{0} (X) & := X {post}^{n + 1} (X) & := post ({post}^{n} (X)) \end{matrix}

This definition of post leads us to another formulation of reach:

Theorem: Definition 2 of reach

⋃ n \geq 0 {post}^{n} (I) = Reach (M)

The proof is done by expanding the post:

\begin{matrix} ⋃ n \geq 0 {post}^{n} (I) (1) = ⋃ n \geq 0 ¯ r [\dots ¯ r [I] \dots] (2) = ⋃ n \geq 0 {¯ r}^{n} [I] (3) = (⋃ n \geq 0 {¯ r}^{n}) [I] (4) = {¯ r}^{*} [I] (5) = Reach (M) \end{matrix}

Where:

Step (1) is by the definition of $post$ .
Step (2) is by the definition of iteration, and using the identity $_{1} [_{2} [X]] = (_{1} \circ_{2}) [X]$ ².
Step (3) is done by moving terms around. We won’t go into too many details, but it’s easy to convince oneself of this step by thinking about what the terms mean intuitively: the union of states reachable in $1, 2, \dots, n$ steps is equal to the states reachable in the union of $1, 2, \dots, n$ steps.
Step (4) is by the definition of transitive closure.
Step (5) is by the first definition of reach.

$\begin{matrix} ■ \end{matrix}$

Invariants

Definition: Invariant

An invariant $P \subseteq S$ of a system $M$ is any superset of the reachable states:

Reach (M) \subseteq P

A way to think of invariants is that all the reachable states must “satisfy the invariant”, i.e. be included in $P$ .

Definition: Inductive Invariant

An inductive invariant $P \subseteq S$ is a set satisfying:

$I \subseteq P$
$s \in P \land (s, a, s^{'}) \in r ⟹ s^{'} \in P$

Intuitively, the second condition means that you can’t “escape” an inductive invariant by taking a step: there can be ingoing edges to an inductive invariant, but no edges exiting the set.

Note that every inductive invariant is also an invariant. Indeed, for an inductive invariant $P$ , if $I \subseteq P$ then we must also grow $P$ to include all states reachable from $I$ in order to satisfy the second property. Therefore, $Reach (M) \subseteq P$ and $P$ is an invariant.

Definition: Inductive strengthening

For an invariant $P$ , $P_{ind}$ is an inductive strengthening of $P$ if:

$P_{ind}$ is an inductive invariant
$P_{ind} \subseteq P$

In this case, we have:

Reach (M) \subseteq P_{ind} \subseteq P

Encoding and storage

Motivating example

Transition systems very quickly get out of hand. Suppose a snack dispenser has $4 \times 6$ different items, and has 10 of each. It can take 500 coins. It then has:

| S | = 10^{4 \cdot 6} \cdot 501 \cdot 2 > 10^{27}

They might not all be reachable, but reachability is a separate question. Here, we’re just defining the graph. In any case, this is too large to store explicitly. Therefore, we must find formulas and data structures to represent it more compactly.

Sequential circuit

We’ll consider a deterministic finite-state transition system $M = (S, I, r, A)$ . We will let $m, n \in N$ be such that $2^{n} \geq | S |$ , and $2^{m} \geq | A |$ , or in other words, $n \geq {log}_{2} | S |$ and $m \geq {log}_{2} | A |$ .

To encode the transition system in bits, we can think of it as 4-tuple of boolean functions:

We can represent the states $S$ on $n$ bits: $S = {0, 1}^{n}$
We can represent the alphabet $A$ on $m$ bits: $A = {0, 1}^{m}$
We can represent the set of initial states $I \subseteq S$ by the boolean function ${0, 1}^{n} \to {0, 1}$ , which maps each state to a boolean (“initial” or “not initial”).
We can represent the transition relation $r \subseteq S \times A \times S$ as a function $(S \times A) \to S$ , which is ${0, 1}^{n} \times {0, 1}^{m} \to {0, 1}^{n}$

We can think of these functions as a circuit receiving an input $¯ a \in {0, 1}^{m}$ , which alters the state $¯ s \in {0, 1}^{n}$ , which in turn alters the relation $r$ .

Example of a simple sequential circuit

Formula encoding of boolean functions

Both the initial states $I$ and the transition relation $r$ are boolean functions. We will often define them mathematically (e.g. $r (s, a) = s \oplus a$ or $I (s) = (s = 0)$ ), but how do we encode them in bits?

We can use a truth table. For instance, the truth table encoding of $r$ is a table mapping inputs $s \in {0, 1}^{n}$ and $a \in {0, 1}^{m}$ to outputs $r (s, a)$ . This is the most efficient encoding if we need to be able to encode any relation: there is no better general encoding. However, most functions can be stored more efficiently.

Let us consider the relation function $r \subseteq {0, 1}^{n} \times {0, 1}^{m} \times {0, 1}^{n}$ . We can consider an input-output pair as the following condition:

((s_{1}, \dots, s_{n}), (a_{1}, \dots, a_{m}), (s_{1}^{'}, \dots, s_{n}^{'})) \in r

We can write this as a propositional formula with variables $(s_{1}, \dots, s_{n}, a_{1}, \dots, a_{m}, s_{1}^{'}, \dots, s_{n}^{'})$ . This formula should be true exactly when the tuple belongs to $r$ .

Let $v \in {0, 1}$ , and let $p$ be a propositional variable. We can then define:

p^{v} = {\begin{matrix} p & if v = 1 \neg p & if v = 0 \end{matrix}

With this notation in hand, we can state the following:

Theorem: Formula encoding of boolean functions

We can always represent a transition relation $r$ as a propositional formula $F$ in disjunctive normal form, where:

F = ⋁ ((v_{1}, \dots, v_{n}), (u_{1}, \dots, u_{m}), (v_{1}^{'}, \dots, v_{m}^{'})) \in r (⋀ 1 \leq i \leq n s_{i}^{v_{i}} \land ⋀ 1 \leq i \leq m a_{i}^{u_{i}} \land ⋀ 1 \leq i \leq n {(s_{i}^{'})}^{v_{i}^{'}})

For many boolean functions ( $\oplus$ , $\land$ , etc) this formulation will be quite small.

Auxiliary variables

This formula is a tree, where variables are leaves, and operations are internal nodes (much like an AST). Clearly, the variables are shared by many operations, so the more efficient representations exploit this sharing, and represent the tree as a directed acyclic graph (DAG) instead.

Note that not only leaves of the tree are shared, but that bigger nodes can also be shared. This leads us to introduce the notion of auxiliary variable definitions. An auxiliary variable represents one such shared node.

We can define auxiliary variables directly in the propositional logic by using the $=$ operator (which is alternative notation for $\leftrightarrow$ ).

For instance, for a $n$ -bit ripple-carry adder can be encoded with:

Initial state $s_{1}, \dots, s_{n}$
Input numbers $a_{1}, \dots, a_{n}$
Output $s_{1}^{'}, \dots, s_{n}^{'}$

The formula for the adder with auxiliary variables $c_{1}, \dots, c_{n + 1}$ (serving as the carry) is:

c_{1} = 0 \land n ⋀ i = 1 (s_{i}^{'} = s_{i} \oplus a_{i} \oplus c_{i}) \land (c_{i + 1} = (s_{i} \land a_{i}) \lor (s_{i} \land c_{i}) \lor (a_{i} \land c_{i}))

The initial carry is $c_{1} = 0$ . Every individual adder gets 3 bits of input to add: two bits, and the previous carry. It outputs a carry of 1 iff two or more input bits are 1. It outputs a single bit as the result of the addition, which is the XOR of all inputs.

Propositional logic

Definition

Propositional logic is a language for representing Boolean functions $f : {0, 1}^{n} \to 0, 1$ as formulas. The grammar of this language is:

P ::= x ∣ 0 ∣ 1 ∣ P \land P ∣ P \lor P ∣ P \oplus P ∣ P \to P ∣ P \leftrightarrow P \neg P

Where $x$ denotes variable identifiers.

QBF

Having looked at boolean formulas let’s now look at a small generalization, QBFs:

Definition: Quantified Boolean Formulas

Quantified Boolean Formulas (QBFs) is built from:

Propositional variables
Constants $0$ and $1$
Operators $\land, \lor, \neg, \to, \leftrightarrow, \exists, \forall$

We will use $=$ as alternative notation for $\leftrightarrow$ . A boolean formula is QBF without quantifiers ( $\forall$ and $\exists$ ).

Free variables

Definition: Free variables

The free variables of a formula is the set of variables that are not bound by a quantifier:

\begin{matrix} F V (v) & = {v} if v is a propositional variable F V (F_{1} \land F_{2}) & = F V (F_{1}) \cup F V (F_{2}) F V (F_{1} \lor F_{2}) & = F V (F_{1}) \cup F V (F_{2}) F V (F_{1} \to F_{2}) & = F V (F_{1}) \cup F V (F_{2}) F V (\neg F_{1}) & = F V (F_{1}) F V (\exists v . F_{1}) & = F V (F_{1}) ∖ {v} F V (\forall v . F_{1}) & = F V (F_{1}) ∖ {v} \end{matrix}

Environment

Definition: Environment

An environment $e$ is a partial map from propositional variables to ${0, 1}$ (“false” or “true”).

Consider two vectors $v = (v_{1}, \dots, v_{n})$ and $p = (p_{1}, \dots, p_{n})$ of $n$ propositional variables. We denote the environment as a mapping $[p \mapsto v]$ given by $e (p_{i}) = v_{i}$ , $\forall 1 \leq i \leq n$

We denote the result of evaluating a boolean expression $F$ with the environment as $⟦ F ⟧_{e}$ . This can evaluate to $0$ (“false”) or $1$ (“true”).

\begin{matrix} ⟦ x ⟧_{e} & = e (x) ⟦ 0 ⟧_{e} & = 0 ⟦ 1 ⟧_{e} & = 1 ⟦ F_{1} \land F_{2} ⟧_{e} & = ⟦ F_{1} ⟧_{e} \land ⟦ F_{2} ⟧_{e} ⟦ F_{1} \lor F_{2} ⟧_{e} & = ⟦ F_{1} ⟧_{e} \lor ⟦ F_{2} ⟧_{e} \end{matrix}

While the formula $⟦ F_{1} \land F_{2} ⟧_{e} = ⟦ F_{1} ⟧_{e} \land ⟦ F_{2} ⟧_{e}$ might seem weird at first (we defined $\land$ in terms of another $\land$ , it makes more sense if we think about the first $\land$ as an AST node and the second as a logical and in the host language:


1
2
3
4
5
6
7

def eval(expr: Expr)(implicit env: Var => Boolean): Boolean = expr match {
    case x: Var => env(x)
    case Literal(0) => false
    case Literal(1) => true
    case And(a, b) => eval(a) && eval(b)
    case Or(a, b) => eval(a) || eval(b)
}

With this notation in hand, we can introduce the following shorthand:

Definition: Models

We write $e ⊨ F$ to denote that $F$ is true in environment $e$ , i.e. that $⟦ F ⟧_{e} = 1$ .

Substitution

Definition: Substitution

Let $F$ and $G$ be propositional formulas, and let $c$ be a variable. Let $F [c := G]$ denote the result of replacing each occurrence of $c$ in $F$ by $G$ :

\begin{matrix} c [c := G] & = G (F_{1} \land F_{2}) [c := G] & = F_{1} [c := G] \land F_{2} [c := G] (F_{1} \lor F_{2}) [c := G] & = F_{1} [c := G] \lor F_{2} [c := G] (\neg F_{1}) [c := G] & = \neg (F_{1} [c := G]) \end{matrix}

We’ll also introduce a general notation to simultaneously replace many variables: $F [c := G]$ denotes the substitution of a vector $c$ of variables with a vector of expressions $G$ .

Validity, Satisfiability and Equivalence

Definition: Satisfiability

A formula $F$ is satisfiable $⟺ \exists e . e ⊨ F$

Note that if $F$ is not satisfiable, it is unsatisfiable, which means $\forall e, ⟦ F ⟧_{e} = 0$ .

Definition: Validity

A formula $F$ is valid $⟺ \forall e . e ⊨ F$

Theorem: Validity and unsatisfiability

$F$ is valid $⟺ \neg F$ is unsatisfiable.

The proof should follow quite trivially from the definitions.

Definition: Equivalence

Formulas $F$ and $G$ are equivalent $⟺$ $\forall$ environment $e$ defined for all free variables in $F V (F) \cup F V (G)$ , we have:

e ⊨ F ⟺ e ⊨ G

This means that two formulas are equivalent if and only if they always return the same values for the same environment (assuming it’s defined for all their free variables).

Theorem: Equivalence and validity

$F$ and $G$ are equivalent $⟺$ the formula $F \leftrightarrow G$ is valid.

Bounded model checking

Formula representation of sequential circuits

Definition: Sequential circuit

We represent a sequential circuit as a 5-tuple $C = (s, Init, R, x, a)$ where:

$s = (s_{1}, \dots, s_{n})$ is the vector of state variables
$Init$ is a boolean formula describing the initial state
$R$ is a boolean formula called the transition formula
$x = (x_{1}, \dots, x_{k})$ is the vector of auxiliary variables
$a = (a_{1}, \dots, a_{m})$ is the vector of input variables

The boolean formula $Init$ tells us which states we can start in, so it can only contain state variables:

F V (Init) \subseteq {s_{1}, \dots, s_{n}}

The transition formula $R$ can only contain state ( $s$ ), next-state ( $s^{'}$ ), auxiliary ( $x$ ) or input ( $a$ ) variables:

F V (R) \subseteq {s_{1}, \dots, s_{n}, a_{1}, \dots, a_{m}, x_{1}, \dots, x_{k}, s_{1}^{'}, \dots, s_{n}^{'}}

The sequential circuit is a representation of a transition system $C = (S, I, r, A)$ , where:

$I = {v \in {0, 1}^{n} ∣ [s \mapsto v] ⊨ Init}$ , meaning that the initial states of a transition system is given by an assignment of state variables that verifies the $Init$ formula
$r = {(v, u, v^{'}) \in {0, 1}^{m + n + m} ∣ [(s, a, s^{'}) \mapsto (v, u, v^{'})] ⊨ \exists x . R}$ , meaning that the transition relation is given by a mapping of states $s$ and inputs $a$ to next-states $s^{'}$ , such that the mapping satisfies the transition formula. Here, the auxiliary variables are existentially quantified so that we can express the criterion without them.

Inductive invariant checking

Given a sequential circuit representation $C = (s, Init, R, x, a)$ of a transition system $M = (S, I, r, A)$ , and a formula $Inv$ , how can we check that $Inv$ is an inductive invariant? According to the definition, we require:

$I \subseteq Inv$
$Inv ∙ r \subseteq Inv$

We’ll ask the SAT solver to check if it’s possible to break either of the two conditions by asking it if it can satisfy either of the following two formulas:

$Init \land \neg Inv$ to check if there is an initial state not included in the invariant.
$Inv \land R \land \neg Inv [s := s^{'}]$ to check if, starting from the invariant and take a step, we can end up outside of the invariant.

To understand this condition, it’s useful to think of $Inv$ as determining the assignment of $s$ . Then, seeing that $S$ contains variables $s, a, x$ and $s^{'}$ , it will fix the assignment for the next states $s^{'}$ . We can then see if the invariant is still true at the next state.

If the SAT solver returns UNSAT to both, we have proven that $Inv$ is an inductive invariant. Note that this resembles a proof by induction (because it is!).

Bounded model checking for reachability

How do we check whether a given state is reachable? Often, we’re interested in knowing if we can reach an error state or not; being able to do so would be bad. To simplify the question a little, we can ask whether we can reach this error state in $j$ steps.

Let $E$ be the error formula corresponding to the error state, so $F V (E) \subseteq {s_{1}, \dots, s_{n}}$ . When we talked about circuits, we said that the state and inputs change at each step, so let us denote the state at step $i$ as $s^{i}$ , and the inputs at step $i$ as $a^{i}$ .

We’ll construct an error formula $T_{j}$ that is satisfiable if and only if there exists a trace of length $j$ starting from the initial state $Init$ that satisfies $E$ :

T_{j} \equiv Init [s := s^{0}] \land (j - 1 ⋀ i = 0 R [(s, a, x, s^{'}) := (s^{i}, a^{i}, x^{i}, s^{i + 1})]) \land E [s := s^{j}]

This formula starts at the initial state, then computes all states $s^{i}$ , and plugs in the final state $s^{j}$ in the error formula to see if it can be satisfied.

If the SAT solver returns UNSAT, the error state is not reachable. If it returns SAT, the

Satisfiability checking

SAT problem

The SAT problem is to determine whether a given formula $F$ is satisfiable. The problem is NP-complete, but useful heuristics exist.

A SAT solver is a program that given a boolean formula $F$ either:

Returns SAT and optionally an environment $e$ such that $e ⊨ F$
Returns UNSAT and optionally a proof that no satisfying assignment exists

Formal proof system

Let’s consider a set of logical formulas $F$ (e.g. propositional logic).

Definition: Proof system

A proof system is a pair $(F, Infer)$ where $Infer \subseteq F^{*} \times F$ is a decidable set of inference steps, where:

A set is decidable $⟺$ there is a program to check if an element belongs to it
Given a set $S$ , $S^{*}$ denotes all finite sequences with elements from $S$

Definition: Inference step

An inference step $S$ is a 2-tuple $S = ((P_{1}, \dots, P_{n}), C) \in Infer$ , which we can denote as:

\frac{P_{1} \dots P_{n}}{C}

We say that from the premises $P_{1} \dots P_{n}$ , we derive the conclusion $C$ .

Definition: Axiom

We say that an inference step is called an axiom when $n = 0$ , i.e. that it has no premises:

\frac{}{C}

Definition: Proof

Given a proof system $(F, Infer)$ , a proof is a finite sequence of inference steps $S_{0}, \dots, S_{m} \in Infer$ such that, for every inference step $S_{i}$ , each premise $P_{j}$ is a conclusion of a previous step.

A minimal propositional logic proof system

We’ll look into a simple logic called the Hilbert system. We’ll define the grammar of our logic as follows. This grammar defines a set of formulas $F$ .

F ::= x ∣ 0 ∣ F \to F

This may seem very minimal, but we can actually express many things by combining these. For instance, we can introduce negation (“for free”) as a shorthand:

\neg F \equiv F \to 0

The inference rules are $Infer = {P_{2}, P_{3}, M P}$ , where:

\begin{matrix} P_{2} & = \frac{}{F \to (G \to F)} \forall F, G \in F P_{3} & = \frac{}{(F \to (G \to H)) \to ((F \to G) \to (F \to H))} \forall F, G, H \in F M P & = \frac{F \to G, F}{G} \forall F, G \in F \end{matrix}

The first two rules are axioms, telling us that an implication is true if the right-hand side is true ( $P_{2}$ ), and that implication is distributive ( $P_{3}$ ). We might recognize modus ponens in the last rule.

We can use these rules to construct a proof of $a \to a$ . We’ll draw this proof as a DAG: we can always view a proof as a DAG because of the requirement that the premises of an inference step be a conclusion of a previous step.

Provability

A formula is provable if we can derive it from a set of initial assumptions. We’ll start by formally defining what an assumption even is:

Definition: Assumptions

Given $(F, Infer)$ where $Infer \subseteq F^{*} \times F$ , and given a set of assumptions $A \subseteq F$ , a derivation from $A$ in $(F, Infer)$ is a proof in $(F, {Infer}^{'})$ where:

{Infer}^{'} = Infer \cup {\frac{}{F} ∣ F \in A}

In other words, assumptions from $A$ are just treated as axioms (i.e. they are rules that have no prerequisites, hence $((), F)$ ). A derivation is a proof that starts from assumptions.

Definition: Provable

We say that “a formula $F \in F$ is provable from a set of assumptions $A$ ”, denoted $A ⊢_{Infer} F$ , $⟺$ there exists a derivation from $A$ in $Infer$ that contains an inference step whose conclusion is $F$ .

We write $\emptyset ⊢_{Infer} F$ (or simply $⊢_{Infer} F$ ) to denote that there exists a proof in $Infer$ containing $F$ as a conclusion.

Consequence and soundness in propositional logic

Definition: Semantic consequence

Given a set of assumptions $A \subseteq F$ , where $F$ is in propositional logic, and given $C \in F$ , we say that $C$ is a semantic consequence of $A$ , denoted $A ⊨ C$ , $⟺$ for every environment $e$ that defines all variables in $FV (C) \cup ⋃_{P \in A} FV (P)$ , we have:

⟦ P ⟧_{e} = 1 \forall P \in A ⟹ ⟦ C ⟧_{e} = 1

In other words, iff an environment makes all assumptions true, and $C$ is true in an environment $e$ when the set of assumptions $A$ are all true in that environment, then we call $C$ a semantic consequence.

Definition: Soundness

A step $((P_{1}, \dots, P_{n}), C) \in Infer$ is sound $⟺ {P_{1}, \dots, P_{n}} ⊨ C$

A proof system $Infer$ is sound if every inference step is sound.

In other words, a conclusion of step is sound if it is a semantic consequence of the previous steps. A proof is sound if all steps are sound.

If $C$ is an axiom (which has no precondition, meaning that $n = 0$ in the above), this definition of soundness means that $C$ is always a valid formula. We call this a tautology.

Theorem: Semantic consequence and provability in sound proof systems

Let $(F, Infer)$ where $F$ are propositional logic formulas. If every inference rule in $Infer$ is sound, then $A ⊢_{Infer} F$ implies $A ⊨ F$ .

This theorem tells us that that if all the inference rules are sound, then $F$ is a semantic consequence of $A$ if $F$ is provable from $A$ . This may sound somewhat straightforward (if everything is sound, then it seems natural that the semantic consequence follows from provability), but is a nice way to restate the previous definitions.

The proof is immediate by induction on the length of the formal proof. As a consequence $\emptyset ⊢_{Infer} F$ implies that $F$ is a tautology.

Proving unsatisfiability

Let’s take a look at two propositional formulas $F$ and $G$ . These are semantically equivalent if $F ⊨ G$ and $G ⊨ F$ .

We can prove equivalence by repeatedly applying the following “case analysis” rule, which replaces a given variable $x$ by 0 in $F$ and by 1 in $G$ :

Definition: Case analysis rule

\frac{F G}{F [x := 0] \lor G [x := 1]}

This is sound, because if we consider an environment $e$ defining $x \in FV (F) \cup FV (G)$ , and assume $⟦ F ⟧_{e} = 1$ and $⟦ G ⟧_{e} = 1$ , then:

if $e (x) = 0$ then $⟦ F [x := 0] ⟧_{e} = ⟦ F ⟧_{e} = 1$
if $e (x) = 1$ then $⟦ G [x := 1] ⟧_{e} = ⟦ G ⟧_{e} = 1$

In either case $F [x := 0] \lor G [x := 1]$ remains true when $F$ and $G$ are sound.

Strictly speaking, the above rule may not be quite enough, so we’ll also introduce a few simplification rules that preserve the equivalence:

\begin{matrix} 0 \land F & ⇝ 0 1 \land F & ⇝ F 0 \lor F & ⇝ F 1 \lor F & ⇝ F \neg 0 & ⇝ 1 \neg 1 & ⇝ 0 \end{matrix}

Those rules together form the sound system ${Infer}_{D}$ , where:

{Infer}_{D} = {\frac{F}{F^{'}} ∣ F^{'} is simplified from F}

Remember that a set $A$ of formulas is satisfiable if there exists an environment $e$ such that for every formula $F \in A$ , $⟦ F ⟧_{e} = 1$ . We can use ${Infer}_{D}$ to conclude unsatisfiability:

Theorem: Refutation soundness

If $A ⊢_{{Infer}_{D}} 0$ then $A$ is unsatisfiable

Here, $0$ means false. This follows from the soundness of $⊢_{{Infer}_{D}}$ . More interestingly, the converse is also true.

Theorem: Refutation completeness

If a finite set $A$ is unsatisfiable, then $A ⊢_{{Infer}_{D}} 0$

This means that $A$ unsatisfiable $⟺ A ⊢_{{Infer}_{D}} 0$ .

For the proof, we can take the conjunction of formulas in $A$ and existentially quantify it to get $A^{'}$ (i.e. $\exists x . A$ )

Conjunctive Normal Form (CNF)

To define conjunctive normal form, we need to define the three levels of the formula:

CNF is the conjunction of clauses
A clause is a disjunction of literals
A literal is either a variable $x$ or its negation $\neg x$

This is a nice form to work with, because we have the following property: if $C$ is a clause then $⟦ C ⟧_{e} = 1 ⟺$ there exists a literal $x_{i} \in C$ such that $⟦ x_{i} ⟧_{e} = 1$ .

We can represent formulas in CNF as a set of sets. For instance:

A = a \land b \land (\neg a \lor \neg b) \equiv {{a}, {b}, {\neg a, \neg b}}

The false value can be represented as the empty clause $\emptyset$ . Note that seeing an empty clause in CNF means that the whole formula is unsatisfiable.

Clausal resolution

Definition: Clausal resolution rule

Let $C_{1}$ and $C_{2}$ be two clauses.

\frac{C_{1} \cup {x} C_{2} \cup {\neg x}}{C_{1} \cup C_{2}}

This rule resolves two clauses with respect to $x$ . It says that if clause $C_{1}$ contains $x$ , and clause $C_{2}$ contains $\neg x$ , then we can remove the variable from the clauses and merge them.

Theorem: Soundness of the clausal resolution rule

Clausal resolution is sound for all clauses $C_{1}, C_{2}$ and propositional variables $x$ .

This tells us that clausal resolution is a valid rule. A stronger result is that we can use clausal resolution to determine satisfiability for any CNF formula:

Theorem: Refutational completeness of the clausal resolution rule

A finite set of clauses $A$ is satisfiable $⟺$ there exists a derivation to the empty clause from $A$ using clausal resolution.

Unit resolution

A unit clause is a clause that has precisely one literal: it’s of the form ${L}$ where $L$ is a literal. Note that the literal in a unit clause must be true.

Given a literal $L$ we define the dual $¯ L$ as $¯ \neg x = x$ and $¯ x = \neg x$ .

Unit resolution is a special case of resolution where at least one of the clauses is a unit clause.

Definition: Unit resolution

Let $C$ be a clause, and let $L$ be a literal.

\frac{C {L}}{C ∖ {¯ L}}

This is sound (if $L$ is true then $¯ L$ is false and can thus be removed from another clause $C$ ). When applying this rule we get a clause $C^{'} \subseteq C$ : this gives us progress towards $\emptyset$ , which is good.

Equivalence and equisatisfiability

Let’s recall that two formulas $F_{1}$ and $F_{2}$ are satisfiable iff $F_{1} ⊨ F_{2}$ and $F_{2} ⊨ F_{1}$ . TODO is this a typo? Should it be “equivalent”?

Definition: Equisatisfiability

Two formulas $F_{1}$ and $F_{2}$ are equisatisfiable $⟺ F_{1}$ is satisfiable whenever $F_{2}$ is satisfiable.

Equivalent formulas are always equisatisfiable, but equisatisfiable formulas are not necessarily equivalent.

Tseytin’s Transformation

Tseytin’s transformation is based on the following insight: if $F$ and $G$ are two formulas, and we let $x \notin FV (F)$ be a fresh variable, then $F$ is equisatisfiable with:

(x \leftrightarrow G) \land F [G := x]

Tseytin’s transformation applies this recursively in order to transform an expression to CNF. To show this, let’s consider a formula using $\neg, \land, \lor, \oplus, \to, \leftrightarrow$ :

F = ((p \lor q) \land r) \to (\neg s)

The transformation works by introducing a fresh variable for each operation (we can think of it as being for each AST node):

\begin{matrix} x_{1} & \leftrightarrow \neg s x_{2} & \leftrightarrow p \lor q x_{3} & \leftrightarrow x_{2} \land r x_{4} & \leftrightarrow x_{3} \to x_{1} \end{matrix}

Note that these formulas refer to subterms by their newly introduced equivalent variable. This prevents us from having an explosion of terms in this transformation.

Each of these equivalences can be converted to CNF by using De Morgan’s law, and switching between $\oplus$ and $\leftrightarrow$ . The resulting conversions are:

Operation	CNF
$x = \neg a$	$(\neg a \lor \neg x) \land (a \lor x)$
$x = a \land b$	$(\neg a \lor \neg b \lor x) \land (a \lor \neg x) \land (b \lor \neg x)$
$x = a \lor b$	$(a \lor b \lor \neg x) \land (\neg a \lor x) \land (\neg b \lor x)$
$x = a \to b$	$(\neg a \lor b \lor \neg x) \land (a \lor x) \land (\neg b \lor x)$
$x = a \leftrightarrow b$	$(\neg a \lor \neg b \lor x) \land (a \lor b \lor x) \land (a \lor \neg b \lor \neg x) \land (\neg a \lor b \lor \neg x)$
$x = a \oplus b$	$(\neg a \lor \neg b \lor \neg x) \land (a \lor b \lor \neg x) \land (a \lor \neg b \lor x) \land (\neg a \lor b \lor x)$

Note that the Tseytin transformations can be read as implications. For instance, the $x = a \lor b$ transformation can be read as:

If $a$ and $b$ are true, then $x$ is true
If $a$ is false, then $x$ is false
If $b$ is false, then $x$ is false

It then takes the conjunction of all these equivalences:

x_{4} \land (x_{4} \leftrightarrow x_{3} \to x_{1}) \land (x_{3} \leftrightarrow x_{2} \land r) \land (x_{2} \leftrightarrow p \lor q) \land (x_{1} \leftrightarrow \neg s)

SAT Algorithms for CNF

Now that we know how to transform to CNF, let’s look into algorithms that solve SAT for CNF formulas.

DPLL

The basic algorithm that we’ll use is DPLL, which applies clausal resolution recursively until an empty clause appears, or all clauses are unit clauses. This works thanks to the theorem on refutational completeness of the clausal resolution rule.


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

def DPLL(S: Set[Clause]): Bool = {
    val S' = subsumption(UnitProp(S))
    if (∅ ∈ S') false // an empty clause means the whole thing is unsat
    else if (S' has only unit clauses) true // the unit clauses give e
    else {
        val L = a literal from a clause of S' where {L} not in S'
        DPLL(S' + Set(L)) || DPLL(S' + Set(complement(L)))
    }
}

// Unit Propagation
def UnitProp(S: Set[Clause]): Set[Clause] =
    if (C ∈ S && unit U ∈ S && resolve(U, C) not in S)
        UnitProp((S - C) + resolve(U, C))
    else S

def subsumption(S: Set[Clause]): Set[Clause] =
    if (C1, C2 ∈ S such that C1 ⊆ C2)
        subsumption(S - C2)
    else S

Backtracking

Perhaps the most intuitive algorithm is to construct a binary decision tree. At each node, we take a random decision. If that leads to a conflict, we go back one step, and take the opposite decision.

This is quite simple, but the complexity is exponential. We’ll therefore see some smarter algorithms.

Non-chronological backtracking

We still construct a binary decision tree. Each decision may also force some other variables into a certain value: we will track these implications in a directed graph.

In this graph, each node represents a value assignment to a variable; let’s say we color a node blue if it has been set directly by a decision, and in green if the value is a consequence of a decision. Edges go from nodes (which may be blue or green) to their consequences.

As we construct the graph, we may create conflicts, meaning that we have two (green) nodes assigning different values to the same variable. In this case, we look at the set of nodes pointing to the conflicting pair of nodes:

In the above example, the variables $x_{3}$ , $x_{7}$ and $x_{8}$ point to the conflicting pair of $x_{9}$ ’s. This means that one of the assignments to these variables was incorrect, because it lead us to the conflict. We can learn from this conflict, and add the following conflict clause to the formula:

(\neg x_{3} \lor \neg x_{7} \lor x_{8})

We can then backtrack to the first decision where we set $x_{3}$ , $x_{7}$ or $x_{8}$ (which may be much earlier than the parent decision in the tree). Every once in a while, it may be useful to completely abandon the search tree (but keep the conflict clauses): this is called a restart.

This approach significantly prunes the search tree; by introducing this conflict clause, we’ve learned something that will be useful forever.

2-literal watching

This algorithm does the standard trick of unit propagation, but avoids expensive book-keeping by only picking 2 literals in each clause to “watch”. We ignore assignments to other variables in the clause.

For each variable, we keep two sets of pointers:

Pointers to clauses in which the variable is watched in its negated form
Pointers to clauses in which the variable is watched in its non-negated form

Then, when a variable is assigned true, we only need to visit clauses where its watched literal is negated. This means we don’t have to backtrack!

Linear Temporal Logic

Definition

With bounded model checking, we’ve seen how to check for a property over a finite trace. However, there are certain properties that we cannot prove by just seeing a finite trace. For instance, program termination or eventual delivery cannot be proven with the semantics of propositional logic. This will prompt us to introduce linear temporal logic, with which we can study events on a trace.

Let $B$ be a boolean formula over state and input variables.

F ::= B ∣ \neg F ∣ F_{1} \lor F_{2} ∣ F_{1} \land F_{2} ∣ next F ∣ prev F ∣ F_{1} until F_{2} ∣ F_{1} since F_{2}

We write $t, i ⊨ F$ to say that a trace $t$ satisfies formula $F$ at time $i$ . The rules for the above constructs are:

\begin{matrix} t, i ⊨ B & ⟺ ⟦ B ⟧_{e} = 1 where e is the state of t at step i t, i ⊨ \neg F & ⟺ \neg (t, i ⊨ F) t, i ⊨ F_{1} \lor F_{2} & ⟺ (t, i ⊨ F_{1}) \lor (t, i ⊨ F_{2}) t, i ⊨ F_{1} \land F_{2} & ⟺ (t, i ⊨ F_{1}) \land (t, i ⊨ F_{2}) t, i ⊨ next F & ⟺ (t, (i + 1) ⊨ F) t, i ⊨ prev F & ⟺ i > 0 \land (t, (i - 1) ⊨ F) t, i ⊨ F_{1} until F_{2} & ⟺ \exists k, k \geq i . \forall j, i \leq j < k . (t, k ⊨ F_{2}) \land (t, j ⊨ F_{1}) t, i ⊨ F_{1} since F_{2} & ⟺ \exists k, 0 \leq k \leq i . \forall j, k < j \leq i . (t, k ⊨ F_{2}) \land (t, j ⊨ F_{1}) \end{matrix}

We can interpret until to mean that $F_{1}$ is true until $F_{2}$ becomes true. For instance, we can guarantee something until an overflow bit is on, at which point all bets are off. Note that this does not impose any constraints on $F_{1}$ once $F_{2}$ is true.

Note that next and prev, and since and until are duals of each other³.

We can add some derived operations from these:

\begin{matrix} eventually F & \equiv 1 until F & ⟺ \exists k \geq i . (t, k ⊨ F) globally F & \equiv \neg (eventually (\neg F)) & ⟺ \forall k \geq i . (t, k ⊨ F) \end{matrix}

The operation globally can be thought of as meaning “forever, from now on” (where “now” is step $i$ ). For instance, $globally (p \to eventually q)$ means that from now on, every point in the trace satisfying $p$ is followed by a point in the trace satisfying $q$ at some point.

Binary Decision Diagrams

Definition

Binary Decision Diagrams (BDDs) are a representation of Boolean functions: we can represent a Boolean function $f : {0, 1}^{n} \to {0, 1}$ as a directed acyclic graph (DAG). We distinguish terminal from non-terminal nodes. Each edge is labeled with a decision: a solid edge (“high edge”) means the variable is 1, and a dashed edge (“low edge”) means that it is 0. The leaf nodes are labeled with the outcome.

For instance, the BDD for $x \lor y$ is:

We can also think of this DAG as a finite automaton, or as a (loop-free) branching program.

Canonicity

The key idea of BDDs is that specific forms of BDDs are canonical, and that BDDs can be transformed into their canonical form. For instance, the previous example can be rewritten as:

Let’s define this transformation more formally.

We first assign an arbitrary total ordering to variables: variables must appear in that order along all paths. Here, we picked $x < y$ as our ordering. Note that in general, selecting a good ordering is an intractable problem, but decent application-specific heuristics exist.

Then, the reduced ordered BDD (RO-BDD) is obtained by:

Merging equivalent leaf nodes (which is what we did above)
Merging isomorphic nodes (same variables and same children)
Eliminating redundant tests (where both outgoing edges go to the same child)

Doing this brings us to the following property:

Theorem: Unicity of RO-BDD

With a fixed variable order, the RO-BDD for a Boolean function $f$ is unique

In the following, we’ll always refer to RO-BDDs, and just call them BDDs.

Data structures for BDDs

To encode a BDD, we’ll map number all nodes as 0, 1, 2, …, where 0 and 1 are terminals. The variables are also numbered as $x_{1}, x_{2}, \dots, x_{n}$ . We also number the levels in the diagram, according to the total ordering that we selected: level 1 is the root node, and level $n + 1$ contains terminal nodes.

A data structure for BDDs is the node table $T : u \to (i, l, h)$ , mapping a node $u$ to its low child $l$ and high child $h$ . The node table also contains an entry $i$ describing the level in the ordering as well as the name of the variable.

For instance, for the example we used above, the table would be:

Node number $u$	Level and name $i$	Low edge $l$	High edge $h$
0	3
1	3
2	2 $y$	0	1
3	1 $x$	2	1

We’ll assume we have some methods for querying this table:

init(T): initialize $T$ with 0 and 1 terminal nodes
u = add(T, i, l, h): add node $u$ with $(i, l, h)$ to $T$
var(u): get $i$ of node $u$
low(u): get $l$ of node $u$
high(u): get $h$ of node $u$

We can also define the inverse $H : (i, l, h) \to u$ of a node table, allowing us to find a node if we have all the information about it. We’ll assume that we have some methods to query and update this structure:

init(H): initialize $H$ with 0 and 1 terminal nodes
u = lookup(H, i, l, h): get node $u$ from $(i, l, h)$
insert(H, i, l, h, u): add an entry from $(i, l, h)$ to $u$

Basic operations on BDDs

Somewhat surprisingly, given a BDD for a formula $f$ , we can check whether it is a tautology, satisfiable or inconsistent in constant time:

$f$ is a tautology $⟺$ the BDD is $1$
$f$ is satisfiable $⟺$ the BDD is not $0$
$f \equiv g ⟺$ their BDDs are equal⁴

To insert a node into $T$ , we ensure that we’re keeping a RO-BDD by eliminating redundant tests, and preventing isomorphic nodes. If that is not the case, we can update the tabée $T$ and the reverse mapping $H$ .


1
2
3
4
5
6
7
8
9
10
11
12
13
14

type NodeId = Int
type Level = Int

def mk(i: Level, l: NodeId, h: NodeId): NodeId = {
  // eliminate redundant tests:
  if (l == h) l
  // prevent isomorphic nodes:
  else if (lookup(H, i, l, h) != null) lookup(H, i, l, h) 
  else {
    u = add(T, i, l, h) // insert node
    insert(H, i, l, h, u) // update reverse mapping
    u
  }
}

With this method in hand, we can see how to build a BDD from a formula $f$ . The key idea is to use Shannon’s expansion:

f = (\neg x \land f ∣_{x = 0}) \lor (x \land f ∣_{x = 1})

Here, $f ∣_{x = 1}$ means that we replace all $x$ nodes by their high-edge subtree. In the formula, we can think of it as a substitution of $x$ by 1. We call this basic operation Restrict.

This breaks the problem into two subproblems, which we can solve recursively:


1
2
3
4
5
6
7
8
9
10

def build(f: Formula): NodeId = build2(f, 1)
private def build2(f: Formula, level: Level): NodeId =
  if (level > n)
    if (f == False) 0 else 1
  else {
    xi = f.variables.head
    f0 = build2(f.subst(xi, 0), level + 1)
    f1 = build2(f.subst(xi, 1), level + 1)
    mk(level, f0, f1)
  }

Interpolation-based model checking

Interpolation

Definition: Interpolant

Let $F$ and $G$ be propositional formulas. An interpolant for $F$ and $G$ is a formula $H$ such that:

$F ⊨ H$
$H ⊨ G$
$FV (H) \subseteq FV (F) \cap FV (G)$

Note that if these conditions hold, we have $F ⊨ G$ . The goal of $H$ is to serve as an explanation of why $F$ implies $G$ , using variables that the two have in common.

Theorem: Existence and Lattice of Interpolants

Let $F$ and $G$ be propositional formulas such that $F ⊨ G$ and let $S$ be the set of interpolants of $(F, G)$ . Then:

If $H_{1}, H_{2} \in S$ then $H_{1} \land H_{2} \in S$ and $H_{1} \lor H_{2} \in S$
$S \neq \emptyset$
$\exists H_{min} . \forall H \in S . H_{min} ⊨ H$
$\exists H_{max} . \forall H \in S . H ⊨ H_{max}$

For instance, let’s consider two formulas $F (x, y)$ and $G (y, z)$ . The variables they have in common are $y$ so we’re looking for an interpolant $I (y)$ .

Reverse interpolants

We know that $F \to G \equiv \neg F \lor G$ . The negation of this is $F \land \neg G$ . Let $A = F$ and $B = \neg G$ . Instead of looking at the validity of $F \to G$ , we can look at unsatisfiability of $A \land B$ . To aid us in this, we’ll define $H$ as an interpolant for $A \land B$ , meaning that we have:

$A ⊨ H$
$H ⊨ B$ , meaning that $B ⊨ \neg H$
$FV (H) \subseteq FV (A) \cap FV (B)$

As previously seen, we can determine whether $A \land B$ is unsatisfiable by using the theorem on completeness of clause resolution: it is unsatisfiable iff we can derive the empty clause using resolution. A key insight here is that we can use the resolution proof to construct an interpolant $H$ for $A \land B$ .

Let’s define $I (C)$ as the interpolant for $A \land (\neg C ∣_{A})$ and $B \land (\neg C ∣_{B})$ , where $C ∣_{A}$ denotes the clause $C$ , but only with literals belong in $FV (A)$ . The idea here is that we can construct it recursively, and that $I (\emptyset)$ is the interpolant for $A$ and $B$ .

There are multiple ways of constructing this $I (C)$ , like the Symmetric System or McMillan’s System (which uses a SAT solver). There are many interpolants that exist, and it’s unclear which is best. Small formulas are good, but we do not currently know any efficient algorithms to find them.

Tseytin’s transformation and interpolants

Remember that Tseytin’s transformation transforms an expression into CNF by introducing fresh variables. Suppose we have converted $A$ and $B$ to $cnf (A)$ and $cnf (B)$ , and that the newly introduced variables are $p_{A}$ and $p_{B}$ , respectively. The results of the Tseytin transformations are:

\emptyset ⊨ A \leftrightarrow \exists p_{A} . cnf (A) and \emptyset ⊨ B \leftrightarrow \exists p_{B} . cnf (B)

Lemma: Interpolant for CNF

The interpolant $H$ for $cnf (A)$ and $cnf (B)$ is also an interpolant for $A$ and $B$

We’ll prove this by showing that all three properties of interpolants are preserved:

todo
todo
By assumption of $H$ being an interpolant for $cnf (A)$ and $cnf (B)$ , we have:
$\begin{matrix} FV (H) & \subseteq FV (cnf (A)) \cap FV (cnf (B)) \subseteq (FV (A) \cup p_{A}) \cap (FV (B) \cup p_{B}) = FV (A) \cap FV (B) \end{matrix}$
The second step is by the above definition of the transformation’s results. The last step is because $p_{A}$ and $p_{B}$ are disjoint.

$\begin{matrix} ■ \end{matrix}$

Reachability checking using interpolants

We can use interpolants to improve upon bounded model checking, in order to prove properties without having to unfold up to the maximum length. To do this, we’ll need to recall two concepts that we’ve seen previously:

Remember that bounded model checking constructs a formula $T_{k}$ that is satisfiable iff there exists a trace of length $\leq k$ starting from the initial state, satisfying an error formula $E$ .
Also, recall the $post$ function.

Reachability checking

To check for reachability, we can keep adding ${post}^{i}$ to the set of reachable states until one of the following two situations arises:

We reach a fixpoint: ${post}^{i + 1} (Init) = {post}^{i} (Init)$ )
We find that an error state is reachable: ${post}^{i} (Init) \cap E \neq \emptyset$ .

The algorithm would look something like this:


1
2
3
4
5
6
7
8
9
10
11
12
13

val errorStates: Set[State] = ???

def reachable(currentStates: Set[State]): Boolean = {
  val nextStates = currentStates union post(currentStates)
  if (nextStates intersect errorStates != emptyset)
    true
  else if (nextStates == currentStates)
    false
  else
    reachable(nextStates)
}

reachable(Init)

The problem with this approach is that computing $post$ may result in a complex image (a large formula or BDD), and it may take many steps to compute all reachable states. To fix this problem, we can do the same trick we always do in formal verification: simplifying the model.

Approximated reachability checking

The insight to simplify is that we can drop complex and uninteresting parts of the $post$ formula: instead of $F_{interesting} \land F_{complex}$ , we’ll only look at $F_{interesting}$ . This allows us to be faster: indeed, a formula that says nothing about certain boolean variables describes a larger set of states (meaning that we grow faster), and has a smaller formula (meaning that the result of $post$ is less complex).

So how does one approximate the post? There are many possible approximations of it, so we’ll use a subscript to denote the (potentially) different approximations. We’ll use a superscript $#$ to denote an approximation of something. Note that a superscript number $n$ still denotes $n$ recursive applications of the function.

Let ${post}_{j}^{#} (X)$ denote any over-approximation of $post$ :

post (X) \subseteq {post}_{j}^{#} (X)

We’ll consider a monotonic $post$ ⁵, meaning that:

X \subseteq Y ⟹ post (X) \subseteq post (Y)

Now, consider the following sequence:

$Init$	$Init$
$post (Init)$	${post}_{1}^{#} (Init)$
${post}^{2} (Init)$	${post}_{2}^{#} ({post}_{1}^{#} (Init))$
…	…
${post}^{n} (Init)$	${post}_{n}^{#} (\dots {post}_{2}^{#} ({post}_{1}^{#} (Init)) \dots)$

The relationship here is that:

post ({post}^{i} (Init)) \subseteq post ({post}_{i}^{#} (\dots {post}_{1}^{#} (Init) \dots)) \subseteq {post}_{i + 1}^{#} ({post}_{i}^{#} (\dots))

This means that we can replace ${post}^{n}$ with recursive applications of different ${post}_{j}^{#}$ approximations. This leads us to the following algorithm:


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

val errorStates: Set[State] = ???
val post#: Array[Set[State] => Set[State]] = ???

def maybeReachable(
  currentStates: Set[State], 
  postAcc: Set[State], // accumulator of post#[i-1](post#[i-2](...))
  i: Int
): Boolean = {
  // compute post#[i](...post#[1](Init)...)
  val nextPostAcc = post#[i](postAcc)

  val nextStates = currentStates union nextPostAcc
  if (nextStates intersect errorStates != emptySet)
    true
  else if (nextStates == currentStates)
    false
  else
    maybeReachable(nextStates, nextPostAcc, i + 1)
}

maybeReachable(Init, Init, 1)

If maybeReachable returns false, then we know for sure that the system is safe, that the error states are not reachable. However, crucially, if maybeReachable returns true, then we cannot really conclude anything. Maybe the error states are reachable, and maybe we just need to try again with better approximations ${post}^{#}$ .

Constructing approximations from interpolants

We have discussed how to use an approximation, but not how to choose one. We’ll start out by showing how to find one from $k = 0$ , and how to continue from there. Let’s look at the formula for bounded model checking again:

T_{j} \equiv Init [s := s^{0}] \land (j - 1 ⋀ i = 0 R [(s, a, x, s^{'}) := (s^{i}, a^{i}, x^{i}, s^{i + 1})]) \land E [s := s^{j}]

To simplify the formula a little, we’ll define:

R_{i} = R [(s, a, x, s^{'}) := (s^{i}, a^{i}, x^{i}, s^{i + 1})]

This allows us to rewrite the formula as:

T_{j} \equiv Init [s := s^{0}] \land R_{0}      A \land (j - 1 ⋀ i = 1 R_{i}) \land E [s := s^{j}]      B

We define $A$ and $B$ as above, and are now interested in finding an interpolant $H$ between the two. The first thing we can look at is which variables $A$ and $B$ have in common; by the third property of interpolants:

FV (H) \subseteq FV (A) \cap FV (B) = s^{1}

We also need the two first properties of interpolants:

$A ⊨ H$ , which is equivalent to $Init [s := s^{0}] \land R_{0} ⊨ H$ . Intuitively, this is like $Init ∙ ¯ r \subseteq H$ , so we can define ${post}_{1}^{#} (Init) = H$ . This is a valid approximation, as $post (Init) \subseteq {post}_{1}^{#} (Init)$ .
$H ⊨ B$ , which is equivalent to $B ⊨ \neg H$ . We can just impose the constraint of $unsat (H \land B)$ to prevent $H$ from being too general.

Once we have an approximation for ${post}_{1}^{#}$ , we can find the ${post}_{2}^{#}$ by treating $H [s^{1} := s^{0}]$ as the new $Init$ and repeating the process, and so on for all the other approximations.

LCF Approach to Formal Proofs

Logic for Computable Functions (LCF) is a logic for reasoning about computable partial functions based on domain theory.

In “A metalanguage for Interactive Proof in LCF”, the idea is:

A Theorem is an abstract data type that stores a formula
We cannot create a theorem out of an arbitrary formula (the constructor is private)
We can create formulas by:
- Creating axiom instances given some parameters (static methods)
- Use inference rules to get theorems from other theorems (instance methods)

The idea is that this allows us to maintain invariants about the theorems. For instance:


1
2
3
4
5
6

final class Theorem private(val formula: Formula) {
  def modusPonens(pq: Theorem, p: Theorem): Theorem = pq.formula match {
    case Implies(pf, qf) if p.formula == pf => Theorem(qf)
    case _ => throw new Exception("illegal use of modus ponens")
  }
}

First order logic

Grammar

We have formulas $F$ and terms $t$ :

\begin{matrix} F ::= & p (t_{1}, \dots, t_{n}) ∣ t_{1} = t_{2} ∣ ⊤ ∣ ⊥ ∣ \neg F ∣ F_{1} \land F_{2} ∣ F_{1} \lor F_{2} ∣ F_{1} \to F_{2} ∣ F_{1} \leftrightarrow F_{2} ∣ \forall x . F ∣ \exists x . F t ::= & x ∣ c ∣ f (t_{1}, \dots, t_{n}) \end{matrix}

Where:

$x$ denotes a variable
$p$ denotes a predicate symbol
$f$ denotes a function symbol
$c$ denotes a constant. We can think of it as a function symbol of arity 0.

To denote how many arguments a function or predicate symbol takes, we define a function $ar$ . For instance, if $ar (f) = 2$ then $f$ takes two arguments.

We’ll also define granularity levels of a formula:

We call $p (t_{1}, \dots, t_{n})$ an atomic formula if it contains no logical connectives or formulas.
A literal is an atomic formula or its negation.
A clause is a disjunction of literals

Interpretation

Definition: First-order logic interpretation

A first-order interpretation is denoted $I = (D, e)$ , where:

$D \neq \emptyset$ is the set of constants
$e$ maps constants, functions and predicate functions as follows:
- Each constant $c$ into an element of $D$ , i.e. $e (c) \in D$
- Each function symbol $f$ with $ar (f) = n$ into a total function of $n$ arguments, i.e. $e (f) : D^{n} \to D$
- Each predicate symbol $p$ with $ar (p) = n$ into an $n$ -ary relation, i.e. $e (p) \subseteq D^{n}$

One thing that’s important to understand about first-order logic is that it is not defined over a fixed set of constants. It can be interpreted with an arbitrary set of constants $D$ , which is not necessarily just booleans (which would be $D = {true, false}$ ). Much like with SAT solvers which can return a boolean assignment $e$ , in an interpretation of a first-order formula, the choice of $e$ maps constants, function symbols and predicate symbols into actual values.

We can evaluate a given formula $F$ with a given interpretation $I$ . We denote this as $⟦ F ⟧_{I}$ .

If the result of the evaluation is true, we write $I ⊨ F$ or $⟦ F ⟧_{I} = 1$ .
If the result of the evaluation is is false, we write $I ⊭ F$ or $⟦ F ⟧_{I} = 0$ .

Since the constants in $D$ aren’t necessarily booleans, how does the result of the evaluation return a boolean? Well, we can “push down” evaluation and compute logical operations on those results⁶:

\begin{matrix} ⟦ \neg F ⟧_{I} & = \neg ⟦ F ⟧_{I} ⟦ F_{1} \land F_{2} ⟧_{I} & = ⟦ F_{1} ⟧_{I} \land ⟦ F_{2} ⟧_{I} ⟦ F_{1} \lor F_{2} ⟧_{I} & = ⟦ F_{1} ⟧_{I} \lor ⟦ F_{2} ⟧_{I} ⟦ \forall x . F ⟧_{I} & = \forall d \in D . ⟦ F ⟧_{(D, e [x := d])} ⟦ \exists x . F ⟧_{I} & = \exists d \in D . ⟦ F ⟧_{(D, e [x := d])} \end{matrix}

We say that:

Definition: Validity and satisfiability in first-order logic

$F$ is valid if $\forall I . ⟦ F ⟧_{I} = 1$
$F$ is satisfiable if $\exists I . ⟦ F ⟧_{I} = 1$

As an example, let’s take a formula $F$ with function symbols $p$ and $q$ :

F = \forall x . \exists y . (p (x, y) \land q (y, x))

Validity: $\forall D \neq \emptyset . \exists p, q \subseteq D^{2} . \forall x \in D . \exists y \in D . ((x, y) \in p \land (y, x) \in q)$
Satisfiability: $\exists D \neq \emptyset . \exists p, q \subseteq D^{2} . \forall x \in D . \exists y \in D . ((x, y) \in p \land (y, x) \in q)$

This leads us to the following observation:

Lemma

$F$ is valid $⟺ \neg F$ is not satisfiable

This means that to check validity, we can instead check satisfiability of the negation. Looking into negations will lead us to defining a normal form for negation.

Negational normal form

In negational normal form, negation only applies to atomic formulas, and the only other connectives are $\land$ and $\lor$ (we’ve translated $\to$ and $\leftrightarrow$ away). It essentially “pushes down” negation. We can transform formulas to negational normal form as follows:

\begin{matrix} F_{1} \leftrightarrow F_{2} & ⇝ (F_{1} \to F_{2}) \land (F_{2} \to F_{1}) F_{1} \to F_{2} & ⇝ \neg F_{1} \lor F_{2} \neg \neg F & ⇝ F \neg (F_{1} \land F_{2}) & ⇝ \neg F_{1} \lor \neg F_{2} \neg (F_{1} \lor F_{2}) & ⇝ \neg F_{1} \land \neg F_{2} \neg \forall x . F & ⇝ \exists x . \neg F \neg \exists x . F & ⇝ \forall x . \neg F \neg ⊥ & ⇝ ⊤ \neg ⊤ & ⇝ ⊥ \end{matrix}

Prenex normal form

Prenex normal form is a form where are all quantifiers appear first, and then we have a formula without quantifiers. Once we are in negational normal form, we can pull quantifiers to the top by the following:

\begin{matrix} (\forall x . F) \lor G & ⇝ \forall x . (F \lor G) (\forall x . F) \land G & ⇝ \forall x . (F \land G) (\exists x . F) \lor G & ⇝ \exists x . (F \lor G) (\exists x . F) \land G & ⇝ \exists x . (F \land G) \end{matrix}

Skolem functions

Observe that the following formula is valid:

(\forall x . p (x, f (x)))) \to (\forall x . \exists y . p (x, y))

Indeed, if we assume the left-hand side of the implication to be true, we need to prove that the right-hand side also holds. To do this, we can simply pick $y$ to be the value of $f (x)$ . This seems obvious.

What’s less obvious is a sort of converse: if we assume that the right-hand side holds, we can prove that there exists an $f$ satisfying the whole formula. Note that we can’t write $\exists f$ because $f$ is a symbol and the FOL grammar doesn’t allow this, but what we can do instead is to extend the signature with a new function symbol $f$ that does not appear in the formula. We call this a Skolem function.

Definition: Skolemization

We can skolemize a formula in prenex normal form by replacing:

\forall x_{1}, \dots, x_{n} . \exists y . F (x_{1}, \dots, x_{n}, y)

with

\forall x_{1}, \dots, x_{n} . F (x_{1}, \dots, x_{n}, g (x_{1}, \dots, x_{n}))

Where $g$ is a fresh function symbol (called a Skolem function) of arity $n$ .

Converting imperative programs to formulas

Motivating example

An imperative program can be thought of as a relation between initial state and final state. For instance, let’s consider the following instructions:


1
2

x = x + 2
y = x + 10

We can think of this as the relation:

{((x, y), (x^{'}, y^{'})) ∣ x^{'} = x + 2 \land y = x + 12}

We can ensure postconditions on this. In Stainless, we could check the following condition:


1
2
3
4
5
6
7
8
9

import stainless.lang._
import stainless.lang.StaticChecks._

case class FirstExample(var x: BigInt, var y: BigInt) {
  def increase: Unit = {
    x = x + 2
    y = x + 10
  }.ensuring(_ => old(this).x > 0 ==> (x > 0 && y > 0))
}

This is equivalent to the following condition, which says that the relation of the program should be a subset of the relation of the pre- and postconditions.

\begin{matrix} {((x, y), (x^{'}, y^{'})) ∣ x^{'} = x + 2 \land y = x + 12} \subseteq & {((x, y), (x^{'}, y^{'})) ∣ x > 0 \to (x^{'} > 0 \land y^{'} > 0)} \end{matrix}

This is equivalent to checking the validity of the following formula:

(x^{'} = x + 2 \land y = x + 12) \to (x > 0 \to (x^{'} > 0 \land y^{'} > 0))

Translating commands

We’ll first define a general formulation of the translation, and then look into commands on a case-by-case basis.

Suppose we want to translate a program containing $n$ mutable variables $V = {x_{1}, \dots, x_{n}}$ . Let $c$ be an arbitrary command. Let $R (c)$ be the formula describing the relation between initial state $V$ and final state $V^{'}$ . We define the relation as $ρ (c)$ :

ρ (c) = {(x, x^{'}) ∣ R (c)}

Assignment

We formulate assignment (x = t) as follows:

x^{'} = t \land ⋀ v \in v ∖ {x} v^{'} = v

The formula says that $x$ now has value $t$ , but also fixes everything that hasn’t changed. We need to constrain the other variables so that they cannot take arbitrary values.

Conditions

We formulate conditions (if (b) c1 else c2) as follows:

(b \land R (c_{1})) \lor (\neg b \land R (c_{2}))

This is a fairly straightforward transformation that corresponds to the boolean formulation of a condition.

Non-deterministic choice

What if we have a condition where we do not know what happens in the condition (e.g. if (*) c1 else c2)? We can simply translate that into a disjunction:

R (c_{1}) \lor R (c_{2})

Sequences

We formulate sequences (c1; c2) as composition of the relations $r_{1}$ and $r_{2}$ corresponding to $c_{1}$ and $c_{2}$ :

ρ (c_{1}; c_{2}) = ρ (c_{1}) \circ ρ (c_{2}) = {(x, x^{'}) ∣ \exists z . (x, z) \in r_{1} \land (z, x^{'}) \in r_{2})}

This simply tells us that there must exist an intermediary state $z$ that binds initial and final state together. The formula is thus:

R (c_{1}; c_{2}) = \exists z . R (c_{1}) [x^{'} := z] \land R (c_{2}) [x := z]

Where $z$ are freshly picked. This relation places the constraint that the output variables of $c_{1}$ should be the input variables of $c_{2}$ . This is a little reminiscent of the formula for bounded model checking.

As a useful convention when converting larger programs, we can name $z$ after the position in the program.

Non-deterministic commands

Let’s introduce a potentially dangerous command, which we’ll call havoc (a word meaning destruction and confusion). How can we formulate havoc(x)? A conservative approach would be to let $x$ be arbitrary henceforth, but keep all other variables as they are:

R (havoc (x)) = ⋀ v \in v ∖ {x} v^{'} = v

Assumption

An assumption (which we’ll call assume(F)) limits the space of possibilities. We can use assume to recover from havoc (e.g. havoc(x); assume(x == e) is equivalent to x = e if x isn’t in the free variables of e). The command doesn’t change anything, but if the condition doesn’t hold, execution should be stopped.

R (assume (F)) = F \land ⋀ v \in v v^{'} = v

The relation created by this translation is the identity relation over the set $A = {x ∣ F}$ of variables satisfying $F$ . To justify the name “assume”, we can look at the following example.

$R (assume (F); c) = F \land R (c)$
$R (c; assume (F)) = R (c) \land F [x := x^{'}]$ , where $x^{'}$ are the final values that we get from executing $c$ .

Note that if (b) c1 else c2 is equivalent to if (*) { assume(b); c1 } else { assume(!b); c2 }; the generated formulas will be equivalent.

Full example

Consider the following code:


1
2
3

(if (b) { x = x + 1 } else { y = x + 2});
x = x + 5;
(if (*) { y = y + 1} else {x = y})

Notice the line numbers; we’ll use those to name our intermediary variables. The translation becomes:

\begin{matrix} \exists x_{2}, y_{2}, x_{3}, y_{3} . & ((b \land x_{1} = x + 1 \land y_{1} = y) \lor (\neg b \land x_{1} = x \land y_{1} = x + 2)) (x_{2} = x_{1} + 5 \land y_{2} = y_{1}) ((x^{'} = x_{2} \land y^{'} = y_{2} + 1) \lor (x^{'} = y_{2} \land y^{'} = y_{2})) \end{matrix}

Here, $x$ and $y$ denote the variables’ initial state (before execution), and $x^{'}$ and $y^{'}$ denote their final state.

Hoare Logic

Hoare logic (named after Sir Tony Hoare) is a logic that was introduced to reason about programs. We can think of it as a way of inserting annotations into code, in order to make proofs about (imperative) program behavior simpler.

As an example, annotations have been added in the program below:


1
2
3
4
5
6
7
8
9
10
11
12
13
14

// {0 <= y}
i = y;
// {0 <= y && i = y}
r = 0;
// {0 <= y && i = y && r = 0}
while // {r = (y-i)*x && 0 <= i}
  (i > 0) {
    // {r = (y-i)*x && 0 < i}
    r = r + x;
    // {r = (y-i+1)*x && 0 < i}
    i = i - 1
    // {r = (y-i)*x && 0 <= i}
}
// {r = x * y}

Let’s look at the first three lines:


1
2
3

// {0 <= y}
i = y;
// {0 <= y && i = y}

This constitutes a Hoare triple, which we’ll study in more detail now.

Hoare triples

Central to Hoare logic are Hoare triples.

Definition: Hoare Triple

Let $S$ be the set of possible states. Let $P, Q \subseteq S$ . Let $r \subset S \times S$ be a relation over the states $S$ . A Hoare triple is defined as:

{P} r {Q} ⟺ \forall s, s^{'} \in S . (s \in P \land (s, s^{'}) \in r \to s^{'} \in Q)

We call $P$ the precondition and $Q$ the postcondition.

Note that ${P}$ does not mean “singleton set of $P$ ”, but is notation for an “assertion” around a command. A Hoare triple may or may not hold; after all it is simply a shorthand for a logical formula, as the definition shows. Let’s look at examples of triples that do and do not hold:

{j = a} j = j + 1 {a = j + 1}

This triple does not hold: if $j$ is equal to $a$ initially, and we then increment $j$ by 1, then $a \neq j + 1$ .
{i != j} if (i > j) then m=i-j else m=j-i {m > 0}

This triple does hold. If $i > j$ then $m > 0$ , and if $j < i$ then it is also positive.

Preconditions and postconditions

Here are a few cues as to how to think of stronger vs. weaker conditions:

A stronger condition is a smaller set than the weaker condition.
A stronger condition is a subset of a weaker condition.
A stronger condition implies a weaker condition.

In other words, putting conditions on a set makes it smaller.

The strongest possible condition is “false”, which is the set $\emptyset$ . The weakest condition is “true”, which is the biggest set (all tuples).

Definitions

Definition: Strongest postcondition

sp (P, r) = {s^{'} ∣ \exists s . s \in P \land (s, s^{'}) \in r}

To visualize this, let’s look at a diagram of the relation $r$ :

Strongest postcondition of a relation — Image from lara.epfl.ch

If we let $P$ be the red set, then $sp (P, r)$ is the blue set: it’s the smallest set of values that all are pointed to from $P$ by $r$ . In other words, it’s the image of $P$ ( $post (P)$ or $P ∙ r$ ), which we can notice has the same definition.

Definition: Weakest precondition

wp (r, Q) = {s ∣ \forall s^{'} . (s, s^{'}) \in r \to s^{'} \in Q}

Weakest precondition of a relation — Image from lara.epfl.ch

Dually, if we let $Q$ be the blue set, then $wp (r, Q)$ is the red set: it’s the largest set of values that only point to $Q$ . Notice that there are points that point to $S$ and $Q$ (since $r$ doesn’t need to be injective), but those are not included in $wp (r, Q)$ . The weakest precondition is the largest possible set from which we will definitely end up in $Q$ from.

Equivalence

Lemma: Three forms of Hoare Triple

The following three conditions are equivalent.

${P} r {Q}$
$P \subseteq wp (r, Q)$
$sp (P, r) \subseteq Q$

These conditions expand into the following formulas, respectively:

$\forall s, s^{'} . [(s \in P \land (s, s^{'}) \in R) \to s^{'} \in Q]$ by definition of a Hoare triple
$\forall s . [s \in P \to (\forall s^{'} . (s, s^{'}) \in r \to s^{'} \in Q)]$ , by definition of the weakest postcondition and definition of subset.
$\forall s^{'} . [(\exists s . s \in P \land (s, s^{'}) \in r) \to s^{'} \in Q)]$ by definition of the strongest postcondition and definition of subset.

From here on, we can prove equivalence using first-order logic properties:

$(P \land Q \to R) ⟺ (P \to (Q \to R))$
$(\forall u . (A \to B)) ⟺ (A \to \forall u . B)$ when $u \notin FV (A)$
$(\forall u . (A \to B)) ⟺ ((\exists u . A) \to B)$ when $u \notin FV (B)$

$\begin{matrix} ■ \end{matrix}$

Characterization

The above lemma also gives us a good intuitive grip of what wp and sp are: they’re the best possible values for $P$ and $Q$ , respectively. For the triple to hold, any other $P$ must be a subset of wp (i.e. stronger), and any other $Q$ must be a supserset of $Q$ (i.e. weaker). This leads us to the following characterization lemmas.

Lemma: Characterization of sp

$sp (P, r)$ is the smallest set $Q$ such that ${P} r {Q}$ , that is, the two following hold:

${P} r {sp (P, r)}$
$\forall Q \subseteq S . {P} r {Q} \to sp (P, r) \subseteq Q$

The first condition immediately follows from the equivalence in the above lemma: it is equivalent to $sp (P, r) \subseteq sp (P, r)$ . The second condition ensures that the strongest precondition is the smallest one (as it’s a subset of all $Q \subseteq S$ ).

Lemma: Characterization of wp

$wp (r, Q)$ is the largest set $P$ such that ${P} r {Q}$ , that is, the two following hold:

${wp (r, Q)} r {Q}$
$\forall P \subseteq S . {P} r {Q} \to P \subseteq wp (P, r)$

The reasoning is the same as above.

Duality

When defining wp, we could see from the diagram that $wp (r, Q)$ almost corresponded to going backwards from $Q$ . And it is almost, because we must deal with the cases where values outside of $wp (r, Q)$ point to $Q$ (which is possible when the relation is not injective). To deal with this, we don’t look at $Q ∙ r^{- 1}$ , but at the complement set of “error states” $S ∖ Q$ (in brown in the diagram).

Lemma: Duality of postcondition-of-inverse and wp

$S ∖ wp (r, Q) = sp (S ∖ Q, r^{- 1})$

Note that $r^{- 1} = {(y, x) ∣ (x, y) \in r}$ and is always defined.

To prove this lemma, we can expand both sides and apply basic first-order logic properties. We first prove it from the left-hand side:

\begin{matrix} x \in S ∖ wp (r, Q) & = x \notin wp (r, Q) = \neg (\forall x^{'} . (x, x^{'}) \in r \to x^{'} \in Q) = \exists x^{'} . (x, x^{'}) \in r \land x^{'} \notin Q \end{matrix}

Now on the right-hand side:

\begin{matrix} x \in sp (S ∖ Q, r^{- 1}) & = \exists x^{'} . x^{'} \notin Q \land (x^{'}, x) \in r^{- 1} = \exists x^{'} . x^{'} \notin Q \land (x, x^{'}) \in r \end{matrix}

As these are equal, we have proven equality. $\begin{matrix} ■ \end{matrix}$

More laws

First, we’ll state a lemma telling us that sp can be applied to each point of a set, or the the whole set, and we get the same results:

Lemma: Pointwise sp

sp (P, r) = ⋃ s \in P sp ({s}, r)

From this, it should be clear what the sp of unions is:

Lemma: Disjunctivity of sp

\begin{matrix} sp (P_{1} \cup P_{2}, r) & = sp (P_{1}, r) \cup sp (P_{2}, r) sp (P, r_{1} \cup r_{2}) & = sp (P, r_{1}) \cup sp (P, r_{2}) \end{matrix}

For wp, the wp can be obtained by selecting each point for which the sp is in $Q$ . To understand this, remember that the sp is like the image, so we can select all points that only point to $Q$ , which is the intuitive explanation we had for wp.

Lemma: Pointwise wp

wp (r, Q) = {s ∣ s \in S \land sp ({s}, r) \subseteq Q}

Likewise, this should give us an idea of how to deal with intersections of sets:

Lemma: Conjunctivity of wp

\begin{matrix} wp (r, Q_{1} \cap Q_{2}) & = wp (r, Q_{1}) \cap wp (r, Q_{2}) wp (r_{1} \cup r_{2}, Q) & = wp (r_{1}, Q) \cap wp (r_{2}, Q) \end{matrix}

All of these can be proven by expanding to formulas and using basic first-order logic.

Hoare Logic for loop-free programs

By now, we’ve seen how to annotate a single relation, and how to reason about preconditions and postconditions. How do we scale this up to a whole program? Specifically, we’ll need to reason over unions and compositions of relations. To do that, we’ll introduce two theorems telling us how to do that.

Suppose the possible paths of a program are $J$ , a set of relations.

Theorem: Expanding paths

The condition:

{P} ⋃ i \in J r_{i} {Q}

is equivalent to:

\forall i . i \in J \to {P} r_{i} {Q}

This simply says that to a triple is valid over a set of relations when it is valid over all relations in the set: it serves as a generalization when we’re considering multiple possible paths.

To prove this, we can use the definitions to expand into formulas. Alternatively, we can use the previous lemmas:

\begin{matrix} {P} ⋃ i \in J r_{i} {Q} & = sp (P, ⋃ i \in J r_{i}) \subseteq Q = (⋃ i \in J sp (P, r_{i})) \subseteq Q = \forall i . i \in J . \to sp (P, r_{i}) \subseteq Q = \forall i . i \in J \to {P} r_{i} {Q} \end{matrix}

The first step translates into the third equivalent form, and the second step uses disjunctivity of sp. The third step translates the union to a quantified formula, and the last step translates back the the first equivalent form. $\begin{matrix} ■ \end{matrix}$

Theorem: Transitivity of Hoare triples

If ${P} r_{1} {Q}$ and ${Q} r_{2} {R}$ then ${P} r_{1} \circ r_{2} {R}$ . We can write this as the following inference rule:

\frac{{P} r_{1} {Q} {Q} r_{2} {R}}{{P} r_{1} \circ r_{2} {R}}

We won’t go into too much detail for this theorem. The two theorems above tell us that if we can annotate Hoare triples for individual statements, we can annotate the whole program.

Hoare logic for loops

For general loops, the simplest rule that we can have is the following. It says that if a single iteration of the loop doesn’t change the precondition, then the whole loop doesn’t change the precondition.

Lemma: Rule for non-deterministic loops

\frac{{P} r {P}}{{P} r^{*} {P}}

This is obviously going to be true by transitivity, but let’s prove it formally nonetheless. We can generalize the previous results to programs with loops. A special case of the transitivity theorem of Hoare triples is when $r_{1} = r_{2}$ and $P = Q = R$ . In that case, we have:

\frac{{P} r {P} {P} r {P}}{{P} r^{2} {P}}

We can keep applying the transitivity rule to achieve a more general form:

\frac{{P} r {P} n \geq 0}{{P} r^{n} {P}}

By the Expanding Paths condition, we then have:

\frac{{P} r {P}}{{P} ⋃_{n \geq 0} r^{n} {P}}

Note that we have the transitive closure in the denominator, $r^{*} = ⋃_{n \geq 0} r^{n}$ . $\begin{matrix} ■ \end{matrix}$

Hoare logic for loops with conditions

Also known as while loops. We did not previously define the relation for while loops like while (b) { c }, so let’s do it now.

Let $b_{s}$ be the set corresponding to the command b, and $(\neg b)_{s}$ be the set corresponding to the command !b. Recall the definition of identity relation. Let $r = ρ (c)$ be the relation of the loop body. The relation of the while loop is:

ρ (while (b) c) = (Δ_{b_{s}} \circ r)^{*} \circ Δ_{(\neg b)_{s}}

The relation follows the $r$ relation an arbitrary number of times while the $b$ condition is true, and then finally the $b$ condition is false. This translates almost directly into the following rule:

Lemma: Rule for loop with condition

For a while (b) { c } loop, we have:

\frac{{P \cap b_{s}} r {P}}{{P} (Δ_{b_{s}} \circ r)^{*} \circ Δ_{(\neg b)_{s}} {P \cap (\neg b)_{s}}}

Restated with commands and conditions instead of relations and sets:

\frac{{P \land b} c {P}}{{P} while (b) c {P \land \neg b}}

We trivially have:

{P} Δ_{b_{s}} {P \cap b_{s}} {P} Δ_{(\neg b)_{s}} {P \cap (\neg b)_{s}}

So by transitivity:

\frac{{P \cap b_{s}} r {P}}{{P} Δ_{b_{s}} {P \cap b_{s}} r {P}} \equiv \frac{{P \cap b_{s}} r {P}}{{P} Δ_{b_{s}} \circ r {P}}

From the rule for non-deterministic loops, we have:

\frac{{P} Δ_{b_{s}} \circ r {P}}{{P} (Δ_{b_{s}} \circ r)^{*} {P}}

Applying these rules, we get the lemma. $\begin{matrix} ■ \end{matrix}$

Properties of program contexts

Properties of relations

Lemma: Monotonicity over composition

\begin{matrix} (r_{1} \subseteq r_{2}) & ⟹ (r_{1} \circ s) \subseteq (r_{2} \circ s) (r_{1} \subseteq r_{2}) & ⟹ (s \circ r_{1}) \subseteq (s \circ r_{2}) \end{matrix}

Lemma: Monotonicity over union

(r_{1} \subseteq r_{2}) \land (s_{1} \subseteq s_{2}) ⟹ (r_{1} \cup s_{1}) \subseteq (r_{2} \cup s_{2})

Lemma: Union distributivity

(r_{1} \cup r_{2}) \circ s = (r_{1} \circ s) \cup (r_{2} \circ s)

Properties of expressions

Expressions are functions that take relations, and construct a more complex relation from them. We’ll only consider expressions that use union ( $\cup$ ) and composition ( $\circ$ ). An example of such an expression would be:

E (r) = (b_{1} \circ r) \cup (r \circ b_{2})

We’ll see two theorems stating that expressions are monotonic, and that they “sort of distribute” over union (meaning sometimes with equality, but always at least with $\subseteq$ ).

Theorem: Monotonicity of expressions using union and composition

Let $S$ be the universe, and let $C = {r ∣ r \subseteq S^{2}}$ be the set of all possible relations in $S$ . Let $E : C \to C$ be any function building one relation from another, where $E (r)$ is built from:

$r$ ,
some additional constant expressions $b_{1}, \dots, b_{n}$ ,
using $\cup$ and $\circ$ .

Such expressions $E$ are monotonic on $C$ :

r_{1} \subseteq r_{2} ⟹ E (r_{1}) \subseteq E (r_{2})

This theorem can be proven by induction on the expression tree defining $E$ , using the monotonicity properties of $\cup$ and $\circ$ that we have seen above.

Theorem: Union “distributivity” of expressions in one direction

Let $r_{i}$ with $i \in I$ be a family of relations. Then:

E (⋃ i \in I r_{i}) \supseteq ⋃ i \in I E (r_{i})

Let $s = ⋃_{i \in I} r_{i}$ . Note that $\forall i . r_{i} \subseteq s$ . Since $E$ is monotonic, $\forall i . E (r_{i}) \subseteq E (s)$ . Since all the $E (r_{i})$ are included in $E (s)$ , so is their union, so $⋃_{i \in I} E (r_{i}) \subseteq E (s)$ .

$\begin{matrix} ■ \end{matrix}$

Note that we do not have equality and we therefore don’t really have a real union distributivity! To see this, take $E (r) = r \circ r$ , and consider the family of relations $I = {1, 2}$ where $r_{1} = {(1, 2)}$ and $r_{2} = {(2, 3)}$ . In this case:

\begin{matrix} E (⋃ i \in I r_{i}) & = E (r_{1} \cup r_{2}) = {(1, 3)} ⋃ i \in I E (r_{i}) & = E (r_{1}) \cup E (r_{2}) = \emptyset \end{matrix}

However, under some special assumptions on $E$ , we actually have full, normal distributivity with equality:

Theorem: Refined union distributivity of expressions

If $E$ satisfies one of the conditions below:

$E (r)$ contains $r$ at most once
$E (r)$ contains $r$ any number of times, but $I$ is a set of natural numbers and $r_{i}$ is an increasing sequence $r_{1} \subseteq r_{2} \subseteq \dots$
$E (r)$ contains $r$ any number of times, but $r_{i}, i \in I$ is a directed family of relations, meaning that for each $i, j$ there exists a $k$ such that $r_{i} \cup r_{j} \subseteq r_{k}$ (and $I$ is possibly uncountably infinite)

Then $E$ distributes over union:

E (⋃ i \in I r_{i}) = ⋃ i \in I E (r_{i})

The third case is actually a generalization of the second. With the increasing sequence, the $r_{k}$ can just be the bigger relation between $r_{i}$ and $r_{j}$ . In this second case, $I$ can be finite or countably infinite, which is also less general than the third case.

All the proofs are done by induction, but we will not go into much detail on them.

More on mapping programs to formulas

We’ve seen how to translate really basic constructs like conditions, while loops and assignment, but will now see some more advanced constructs that many real programming languages.

Mutable local variables

When translating code into formulas, each statement is a relation between variables in scope. What happens if we introduce a variable in local scope? Suppose x and z are global variables, and we have a block introducing a local variable y:


1
2
3
4
5
6
7

x = x + 1;
{
  var y;
  y = x + 3;
  z = x + y + z
};
x = x + z

The final formula should not depend on y. Therefore, we need to do some kind of local variable translation, which we can do with existential quantification.

Let’s call the whole expression in brackets $P$ . Inside $P$ , we have variables $V = {x, y, z}$ . Let $R_{V} (P)$ be the formula for $P$ , containing variables $V$ in the scope. This is a refinement of the previous definition of $R$ , which only used the top-level scope $V$ ; here, we can give it a local scope.

The variable initialization in the bracket block can be translated into a formula by:

R_{V} ({var y; P}) = \exists y, y^{'} . R_{V \cup {y}} (P)

This lets $y$ and $y^{'}$ be unconstrained, and translates the rest of the block with $y$ now added into the scope $V$ . This lets $y$ take any value in $P$ . Note that the translation of this is quite similar to what havoc does. In fact, we can express havoc using these semantics:

R_{V} (havoc (x)) ⟺ R_{V} ({var y; x = y})

This equivalence will serve as a handy shorthand: when we initialize multiple variables, we can write it as:

havoc (y_{1}, \dots, y_{m}) \equiv havoc (y_{1}); \dots; havoc (y_{m})

Note that the order of havocs does not matter.

Specifications

A specification (a.k.a. spec) is a formula that expresses some pre- and postconditions that the program should respect. Note that the spec is often more general than the strongest postcondition, but it could very well be the actual sp.

There are three ways in which we can think of a spec; we give a translation of the same example for each:

Formula: $(z^{'} = z) \land (x^{'} > 0) \land (y^{'} > 0)$
Relation: ${(x, y, z, x^{'}, y^{'}, z^{'}) ∣ (z^{'} = z) \land (x^{'} > 0) \land (y^{'} > 0)}$
Program: havoc(x, y); assume(x > 0 && y > 0)

A program adheres to the spec if its relation is a subset of the spec’s relation.

Note that the above program representation lets $x$ and $y$ be unconstrained by the havoc, and constrains $x^{'}$ and $y^{'}$ through the assume. We get $z = z^{'}$ by default, by not writing anything about $z$ .

We can define the operator in the other direction in the obvious manner:

P_{2} ⊒ P_{1} ⟺ P_{1} ⊑ P_{2}

Note that this is nothing more than a new notation for relation subset, since:

P_{1} ⊑ P_{2} ⟺ ρ (P_{1}) \subseteq ρ (P_{2})

Definition: Equivalence

We define equivalence of two programs $P_{1}$ and $P_{2}$ as:

P_{1} \equiv P_{2} ⟺ P_{1} ⊑ P_{2} \land P_{2} ⊑ P_{1}

From the above comment, we can see that this is just new notation for relation equality, since:

P_{1} \equiv P_{2} ⟺ ρ (P_{1}) = ρ (P_{2})

This follows directly from our lemmas of monotonicity of relations over composition and monotonicity over union. $\begin{matrix} ■ \end{matrix}$

Why is this notion of refinement useful? It allows us to model one possible execution of very general, possibly non-deterministic program. We can do this by refining the program in steps, until it becomes deterministic, simple, efficiently executable:

P_{0} ⊒ P_{1} ⊒ \dots ⊒ P_{n}

Loops, revisited

Let’s examine the following program $L$ , which has variables $V = {x, y}$ :


1
2
3

while (x > 0) {
  x = x - y
}

We’re interested in finding the smallest relation $ρ (L)$ between initial state $(x, y)$ and final state $(x^{'}, y^{'})$ . Let $k$ be the number of time the loop executes. We can see that there are two different cases here:

When $k = 0$ , we never enter the loop because the initial $x$ did not satisfy the loop condition; therefore, all variables are kept the same
When $k > 0$ , we enter the loop, and decrement $x$ by $y$ $k$ times, and finally the loop condition no longer holds.

This leads us to the following formulas:

\begin{matrix} k = 0 & ⟹ R (L) = (x \leq 0) \land (x^{'} = x) \land (y^{'} = y) k = 1 & ⟹ R (L) = (x > 0) \land (x^{'} = x - y) \land (y^{'} = y) \land (x^{'} \leq 0) ⋮ k > 0 & ⟹ R (L) = (x > 0) \land (x^{'} = x - k y) \land (y^{'} = y) \land (x^{'} \leq 0) \end{matrix}

To find a formula that fits both the $k = 0$ and $k > 0$ cases, we can take the disjunction of the two. For $k > 0$ , there will be a single value of $k$ at runtime, so we existentially quantify to express that:

\begin{matrix} R (L) = & [(x \leq 0) \land (x^{'} = x) \land (y^{'} = y)] \lor [\exists k . (k > 0) \land (x > 0) \land (x^{'} = x - k y) \land (y^{'} = y) \land (x^{'} \leq 0)] \end{matrix}

This existential quantifier is annoying, and we will see later how to apply to one-point rule to eliminate it. (TODO, note that the bar in the slides is notation for “y divides …”)

Fixpoints

Before we see how to translate recursive functions, we need a bit of theory on fixpoints:

Definition: Fixpoint

$s \in C$ is a fixpoint of $E : C \to C$ if $E (s) = s$

This is analogous to what exists on real function: the fixpoints of $f (x) = x^{2} - x - 3$ are $x_{1} = - 1$ and $x_{2} = 3$ .

We are often interested in the fixpoint that is smaller than all others, which we call the least fixpoint. In the example on the polynomial, it would be $x_{1} = - 1$ . For relations, we’re looking for the fixpoint that is $\subseteq$ of all other fixpoints.

Recursion

A recursive function will result in a recursive relation; say that we’re translating the following function f into a relation:


1
2
3
4
5

def f() = if (x > 0) {
    x = x -1;
    f();
    y = y + 2
} else { }

We know how to translate most of these constructs, but what postconditions can we assume on the recursive call? We’re not done inferring postconditions on the body, so we don’t know what the final result should be. The solution to find a relation $s$ for $f$ such that $E (s) = s$ .

For now, let’s suppose $s$ has this property, and leave it as a variable. Translating the above function f, we get:

E (s) = [Δ_{(x > 0)_{s}} \circ (ρ (x = x - 1) \circ s \circ ρ (y = y + 2))] \cup Δ_{(x \leq 0)_{s}}

Here, the subscript s means “the set corresponding to this formula”. We’ll how to find this relation $s$ :

Theorem: Relation for recursion

Let $E (s)$ be the expression translating the body of a recursive function, where $s$ is the relation of the recursive call. Let $s$ be defined as follows:

s = ⋃ k \geq 0 E^{k} (\emptyset)

where $E^{0} (\emptyset) = \emptyset$ . The relation $s$ is the least fixpoint of $E$ , and $E (s)$ is the relation corresponding to the recursive function.

We’ll prove that $s$ is indeed a fixpoint of $E$ . Note that, according to the theorem of monotonicity of expressions using union and composition, $E$ is monotonic. This fact means that we actually satisfy the second condition of union-distributivity of $E$ . To see this, pick $r_{0}, r_{1}, \dots, r_{k}$ as follows:

$r_{0} = \emptyset$
$r_{1} = E (r_{0}) = E (\emptyset)$
…
$r_{k} = E^{k} (\emptyset)$

We indeed have $r_{0} \subseteq r_{1} \subseteq \dots \subseteq r_{k}$ by monotonicity of $E$ . Therefore, $E$ distributes over union. Having union-distributivity will be crucial in finding a relation $s$ such that $E (s) = s$ . Indeed, we can pick $s$ as follows:

s = ⋃ k \geq 0 r_{k}

With union-distributivity, we can show that this choice of $s$ satisfies $E (s) = s$ :

E (s) = E (⋃ k \geq 0 r_{k}) (1) = ⋃ k \geq 0 E (r_{k}) = ⋃ k \geq 0 r_{k + 1} = ⋃ k \geq 1 r_{k} = \emptyset \cup ⋃ k \geq 1 r_{k} = s

The step $(1)$ is the one that needs the union-distributivity property.

$\begin{matrix} ■ \end{matrix}$

Let’s follow this up with a proof that $s$ is the least fixpoint. We obtained $s$ by solving $E (s) = s$ ; now, suppose $r$ is an arbitrary relation such that $E (r) \subseteq r$ . Note that $s$ does satisfies this condition. We now claim that $s \subseteq r$ , i.e. that it is the smallest. If we expand $s$ to its definition, we’ll see that we need to prove:

⋃ k \geq 0 E^{k} (\emptyset) \subseteq r

If we can show $E^{k} (\emptyset) \subseteq r$ for every $k$ , we’ll have proven this. This can be done by induction: the base case is $\emptyset \subseteq r$ , which is trivially true. The induction step is by monotonicity of $E$ :

E^{k} (\emptyset) \subseteq r (1) ⟹ E (E^{k} (\emptyset)) \subseteq E (r) (2) ⟹ E (E^{k} (\emptyset)) \subseteq r

Step $(1)$ is by monotonicity of $E$ , and step $(2)$ is by the original assumption of $E (r) \subseteq r$ .

$\begin{matrix} ■ \end{matrix}$

Note that this second proof is actually stronger than we strictly need it to be: not only did we prove that $s$ is the least fixpoint (smaller than any $r$ such that $E (r) = r$ ), we proved that $s$ is also smaller than any other $r$ such that $E (r) \subseteq r$ . We’ll see some vocabulary for this later (todo link), with which we can say that $s$ is the least postfix point.

This model has the advantage of being simple, but also has limitations; for one, it translates programs that never terminate in the same way as programs that do. Therefore, the correct semantics of the translation is that it only applies to terminating executions. The alternative would be error states for non-termination, but we won’t look into that.

Specification of recursive functions

In the previous section, we had $E (r) \subseteq r$ . Let’s think about what that means, from a more intuitive perspective. It means that when we plug $r$ into $E$ , we get something that conforms to the $r$ spec. This is exactly what we wanted in the first place: finding a translation of a recursive call that also satisfies the spec for the function itself.

Now, suppose that we want to check a user-defined specification $q$ :

q = {((x, y), (x^{'}, y^{'})) ∣ y^{'} \geq y}

As for any spec, we need to check that the relation of the program is a subset of the spec, $s \subseteq q$ . This is actually equivalent to proving $E (q) \subseteq q$ .

Mutual recursion

Suppose we have two mutually recursive procedures $r_{1} = E_{1} (r_{1}, r_{2})$ and $r_{2} = E_{2} (r_{1}, r_{2})$ . We can extend the previous approach to work on pairs. We define $E (r_{1}, r_{2}) = (E_{1} (r_{1}, r_{2}), E_{2} (r_{1}, r_{2}))$ and $r = (r_{1}, r_{2})$ . We want to find a pair of relations $r$ such that:

E (r) = r

In order to do this, we introduce the a partial ordering (more on this later, todo link), where $(r_{1}, r_{2}) ⊑ (r_{1}^{'}, r_{2}^{'})$ means $r_{1} \subseteq r_{1}^{'}$ and $r_{2} \subseteq r_{2}^{'}$ . This will allow us to express refinements.

Pairs aren’t sets, but we can define set-like operations on them by applying the operation to both members of the pair. We denote these operations using the square variant of the set operation in question. For instance:

(r_{1}, r_{2}) ⊔ (r_{1}^{'}, r_{2}^{'}) = (r_{1} \cup r_{1}^{'}, r_{2} \cup r_{2}^{'})

The entire theory is preserved as long as we have a partial order $⊑$ with some “good properties” (i.e. lattice elements are a generalization of sets), so this extension can be done without too much extra work.

To find the least fixpoint, the semantics are now:

(s_{1}, s_{2}) = ⨆ i \geq 0 E^{i} (\emptyset, \emptyset)

As before, we can prove that if we consider any relations $c_{1}, c_{2}$ such that $E_{1} (c_{1}, c_{2}) \subseteq c_{1}$ and $E_{2} (c_{1}, c_{2}) \subseteq c_{2}$ then $s$ is the least fixpoint, meaning $s_{1} \subseteq c_{1}$ and $s_{2} \subseteq c_{2}$ .

Quantifier elimination in Presburger arithmetic

Quantifier elimination

Definition: Quantifier elimination

Given a formula $F (y)$ , the goal of quantifier elimination (QE) is to find a formula $G (y)$ that:

is equivalent to $F (y)$
has no quantifiers
has $FV (G) \subseteq FV (F)$

Generally, given an assignment $y$ , it’s easier to check the truth value of $G (y)$ because it has no quantifiers.

The third above condition may prompt an interesting question; what if $F$ has no free variables, for instance because they’re all bound by quantifiers? The condition still holds, so $G$ would have no variables at all, it would simply be a constant expression, which we can immediately verify the truth of it.

This also means that we can check satisfiability and validity of $H (y)$ by:

Satisfiability: do QE on $\exists y . H (y)$ and evaluate
Validity: do QE on $\forall y . H (y)$ and evaluate

Presburger arithmetic

Let’s talk about how to use what we’ve discussed in order to verify programs. We can do this in three steps:

Compile programs to logical formulas
Express properties in logic or code
Use an automated theorem prover for generated conditions (SAT, SMT, rewrite, interactive provers)

Which logic should we use? We’ll look into integer linear arithmetic, also known as Presburger arithmetic.

This is integer arithmetic with logical operations ( $\land, \lor, \neg$ ), quantifiers ( $\forall, \exists$ ), addition ( $+$ ), and comparison ( $<, =$ ). This is one of the earliest theories that was shown to be decidable⁷.

We’ll see that we can extend Presburger arithmetic to admit quantifier elimination (QE): this is not a trivial result, as not all theories admit QE. The reason for which we want to do QE in the first place is that formulas are hard to decide when they have formulas. A Presburger arithmetic formula of size $n$ with $m$ quantifiers is decidable by a single-tape alternating Turing machine in time $2^{n^{O (m)}}$ . This is very sensitive to the value of $m$ .

Another reason to do QE is to remove quantifiers from interpolants, which is useful in generalizing counterexamples to invariants. Note that if a logic has QE, it also has quantifier-free interpolants.

One-point rule

The one-point rule is one of the many steps used in quantifier elimination procedures. Note that it is not enough on its own, because it only handles equalities, and not inequalities .

Theorem: One-point rule

If $y$ is a tuple of variables not containing $x$ , then:

\exists x . (x = t (y) \land F (x, y)) ⟺ F (t (y), y)

This rule should make intuitive sense; it’s somewhat akin to inlining (in the $\Rightarrow$ direction) or extracting to a variable (in the $\Leftarrow$ direction). In the $\Rightarrow$ direction, we say that we apply the one-point rule, and in the $\Leftarrow$ direction we call it flattening.

We can also state the dual of this rule, which is the negated version of this statement

Theorem: Dual one-point rule

\forall x . (x = t (y) \to F (x, y)) ⟺ F (t (y), y)

The proof for this is easy; we negate both sides and see that it reduces to the rule for $\exists$ :

\begin{matrix} \exists x . (x = t (y) \land \neg F (x, y)) ⟺ \neg F (t (y), y) \\ ■ \end{matrix}

Making Presburger arithmetic admit QE

As is, Presburger arithmetic (PA) does not admit QE. If we lack some operations that can be expressed with quantifiers, there may be no equivalent without quantifiers. For instance, we can state divisibility by 3 in PA as follows:

\exists y . x = y + y + y

This indicates to us that we need a divisibility operator (e.g. $3 ∣ x$ ), because in order to do QE we must have a quantifier-free equisatisfiable variant of the above formula. We will therefore extend PA with the following, where we always have $K \in Z$ .

Comparison $x < y$
Subtraction $x - y$
Divisibility $K ∣ y$
Multiplication by a constant factor $K \cdot x$ (this is just shorthand for very long additions)

The resulting language has operators ${+, -, =, <, ∣, \cdot}$ on numbers and variables, and ${\land, \lor, \neg, \to, \exists, \forall}$ on atomic formulas.

Normalized Presburger arithmetic

To normalize terms in PA, we can rearrange each term to be of the form:

K_{0} + n \sum i = 1 K_{i} x_{i}

A term in this form is called a linear term. To normalize literals in PA, we do the following translation:

\begin{matrix} \neg (t_{1} < t_{2}) & ⇝ t_{2} < t_{1} + 1 \neg (t_{1} = t_{2}) & ⇝ (t_{1} < t_{2}) \lor (t_{2} < t_{1}) t_{1} = t_{2} & ⇝ (t_{1} < t_{2} + 1) \land (t_{2} < t_{1} + 1) \neg (K ∣ t) & ⇝ K - 1 ⋁ i = 1 K ∣ t + i t_{1} < t_{2} & ⇝ 0 < t_{2} - t_{1} \end{matrix}

This generates some disjunctions and conjunctions, but we can convert back to DNF again.

Eliminating existential quantifiers

Let’s see how to eliminate $\exists$ from the following, where $F$ is quantifier-free:

\exists x . F (x, y)

To do that, we can convert $F$ to disjunctive normal form, a disjunction of clauses $C_{i}$ , each of which is a conjunction of literals.

F ⟺ m ⋁ i = 1 C_{i}

The elimination is then done by:

\exists x . F ⟺ (\exists x . m ⋁ i = 1 C_{i}) ⟺ m ⋁ i = 1 \exists x . C_{i}

Eliminating universal quantifiers

Suppose $F_{0} (x, y)$ is quantifier-free, and we want to eliminate $\forall$ from the following formula:

\forall x . F_{0} (x, y)

This is equivalent to:

\forall x . F_{0} (x, y) ⟺ \neg (\exists x . \neg F_{0} (x, y))

We know how to handle this right-hand side: we can eliminate the existential quantifier in $\exists x . \neg F_{0} (x, y)$ to obtain $F_{1} (y)$ . The result of elimination is therefore:

\neg F_{1} (y)

Exposing the variable to eliminate

Sometimes, we want to do QE of a quantified variable $y$ , but $y$ appears in a multiplied in the formula, or with bounds.

Multiplication

For comparison and “divides” terms, we can rely on the following observations, for $c \in N^{+}$ :

$0 < t \equiv 0 < c t$
$K ∣ t \equiv c k ∣ c T$

Let $K_{1}, \dots, K_{n}$ be the coefficients next to $y$ ; we choose $M = lcm (K_{1}, \dots, K_{n})$ . Then, to ensure coefficient 1, we multiply all literals by $M / | K_{i} |$ to obtain multiples $M$ or $- M$ (as in the example above, in which $M = 30$ ). Then, we let $x = M y$ and solve:

\exists x . F (x) \land (M ∣ x)

As an example of this, let’s consider the following formula:

\exists y . (0 < - w + 3 y + 1) \land (0 < - 2 y + z + 6) \land 4 ∣ (5 y + 1)

In this case, the we can take the least common multiple (lcm) of the coefficients of $y$ :

M = lcm (3, 2, 5) = 30

We now make all occurrences of $y$ by have coefficient $M$ (but preserving mathematical equivalence, so we need to update other coefficients too):

\exists y . (0 < - 10 w + 30 y + 10) \land (0 < - 30 y + 15 z + 90) \land (24 ∣ (30 y + 6))

Let $x$ denote $30 y$ . Note that this is not an arbitrary $x$ , it must be divisible by 30, so we add a condition for that at the end. The formula is now:

\exists x . (0 < - 10 w + x + 10) \land (0 < - x + 15 z + 90) \land (24 ∣ (x + 6)) \land (30 ∣ x)

Bounds

Let’s focus on a single variable $x$ . We can reorganize the formula in terms of $x$ to fit the following form, so that there are $L$ lower bounds on $x$ , and $U$ upper bounds, and $D$ divisibility constraints. We call this form $F_{1} (x)$ :

F_{1} (x) = (L ⋀ i = 1 a_{i} < x) \land (U ⋀ j = 1 x < b_{j}) \land (D ⋀ i = 1 K_{i} ∣ (x + t_{i}))

If there are no divisibility constraints ( $D = 0$ ), then the formula can be rewritten as:

F_{1} (x) \equiv (max i a_{i} + 1 \leq min j b_{j} - 1)

The min and the max are not something that we can express directly in PA, but we can convert that into the following equivalent form:

F_{1} (x) \equiv (max i a_{i} + 1 \leq min j b_{j} - 1) \equiv ⋀ i, j a_{i} + 1 < b_{j}

Alternatively, we can express this as follows, where $t_{k}$ does not contain $x$ (after all, our goal is to eliminate $x$ ):

F_{1} (x) \equiv ⋁ k F_{1} (t_{k})

Let’s see a few instances of this, depending on the values of $L$ , $U$ and $D$ :

$D = 0$ and $L > 0$ :
$F_{1} (x) \equiv L ⋁ k = 1 F_{1} (a_{k} + 1)$
At least one of the terms in $⋁$ will evaluate to $max a_{i} + 1$ , so this is valid.
$D > 0$ :
$L ⋁ k = 1 N ⋁ i = 1 F_{1} (a_{k} + i)$
where $N = lcm (K_{1}, \dots, K_{D})$ . This works because if $F_{1} (u)$ holds, then $F_{1} (u - N)$ holds too.
$L = 0$ :
$N ⋁ x = 1 D ⋀ i = 1 K_{i} ∣ (x + t_{i})$

Generalization of Presburger arithmetic

Let’s consider a generalization of Presburger logic: first-order formulas with equality and comparison, interpreted over rationals instead of integers. This is called dense linear order without endpoints. The solution for QE is actually simpler than for PA, because there are no divisibility constraints.

These are of course equivalent, but it sometimes helps to be able to distinguish whether an operator is written in the context of a formula or in the context of a mathematical statement. ↩
The proof of this identity is in exercise session 1, exercise 2.1.1. It is done by decomposing into existential quantifiers. ↩
Or rather, they’re almost duals, because the future is infinite but the past is finite. ↩
This is a consequence of the the theorem of unicity of the RO-BDD ↩
Why do we consider $post$ to be monotonic? Well, that will become clear later in the course: for our application of verifying programs, we will work with monotonic relations. ↩
These rules are not complete, but suffice if we’ve translated the formula to negational normal form. ↩
The story goes that Presburger solved this in his MSc thesis with Tarski in 1929, but that Tarski was not impressed. ↩

View the edit history

« Back