CS550 Formal Verification
Throughout these notes, vectors are denoted in bold and lowercase (e.g. ). Booleans are denoted interchangeably by and , or and . Generally, I try to use and for formulas, and and for mathematical notation^{1}.
 Transition systems
 Propositional logic
 Bounded model checking

Satisfiability checking
 SAT problem
 Formal proof system
 A minimal propositional logic proof system
 Provability
 Consequence and soundness in propositional logic
 Proving unsatisfiability
 Conjunctive Normal Form (CNF)
 Clausal resolution
 Unit resolution
 Equivalence and equisatisfiability
 Tseytin’s Transformation
 SAT Algorithms for CNF
 Linear Temporal Logic
 Binary Decision Diagrams
 Interpolationbased model checking
 LCF Approach to Formal Proofs
 First order logic
 Converting imperative programs to formulas
 Hoare Logic
 Properties of program contexts
 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.
A transition system is a 4tuple where:
 is the set of states
 is the set of starting states
 is the transition relation
 is the alphabet
For and , means that ther is a transition from to on input .
A few special cases of this general form exist:
 If is finite, we have a finite state machine
 If and , then the system is deterministic.
Traces and reachability
A trace is a finite or infinite sequence, describing steps taken by a transition system:
where we require, :
A trace may or may not be finite. If they are finite, we can assume that the trace ends with a state . We’ll introduce some notation for traces:
is the set of all traces of a transition system , starting from .
The reachable states are states for which there exists a trace that ends in :
To check for reachability, for a finite , 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 .
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 :
Generally, we’ll use a bar for relations that disregard input. Note that even when is deterministic, can become nondeterministic.
Composition
Relations can be composed:
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 be the routes operated by United Airlines, and be the routes operated by Delta. Then is the set of routes possible by taking a United flight followed by a Delta flight.
Iteration
An iteration describes paths of length in a relation . It is defined recursively by:
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:
The identity relation (also called “diagonal relation” or “triangular relation”) is the relation mapping every item in the universe to itself:
This relation can be conditioned, so as to only include elements in a set (or satisfying a condition ):
Transitive closure
Applying iteration an arbitrary number of times leads us to the transitive closure:
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: , so every item is mapped back onto itself (among others, potentially)
 Transitivity:
 Distributivity (under certain conditions): if is reflexive and transitive and , then
 Monotonicity:
A few bonus facts:
 is the smallest reflexive transitive relation containing .

An edge is in the transitive closure if and only if there is a path in the graph . In mathematical notation, this is:
Image
Finally, we’ll introduce one more definition:
The image of a state set under a relation is the set of states reachable in one step from :
We also introduce an alternative notation:
The alternative notation may make it simpler to read images; can be read as “ following then following ”.
Reach
The above definitions lead us to a first definition of reach:
Post
We’ll introduce another definition in order to give an alternative definition of reach. We’re still considering a state system .
This definition of post leads us to another formulation of reach:
The proof is done by expanding the post:
Where:
 Step (1) is by the definition of .
 Step (2) is by the definition of iteration, and using the identity ^{2}.
 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 steps is equal to the states reachable in the union of steps.
 Step (4) is by the definition of transitive closure.
 Step (5) is by the first definition of reach.
Invariants
A way to think of invariants is that all the reachable states must “satisfy the invariant”, i.e. be included in .
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 , if then we must also grow to include all states reachable from in order to satisfy the second property. Therefore, and is an invariant.
For an invariant , is an inductive strengthening of if:
 is an inductive invariant
In this case, we have:
Encoding and storage
Motivating example
Transition systems very quickly get out of hand. Suppose a snack dispenser has different items, and has 10 of each. It can take 500 coins. It then has:
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 finitestate transition system . We will let be such that , and , or in other words, and .
To encode the transition system in bits, we can think of it as 4tuple of boolean functions:
 We can represent the states on bits:
 We can represent the alphabet on bits:
 We can represent the set of initial states by the boolean function , which maps each state to a boolean (“initial” or “not initial”).
 We can represent the transition relation as a function , which is
We can think of these functions as a circuit receiving an input , which alters the state , which in turn alters the relation .
Formula encoding of boolean functions
Both the initial states and the transition relation are boolean functions. We will often define them mathematically (e.g. or ), but how do we encode them in bits?
We can use a truth table. For instance, the truth table encoding of is a table mapping inputs and to outputs . 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 . We can consider an inputoutput pair as the following condition:
We can write this as a propositional formula with variables . This formula should be true exactly when the tuple belongs to .
Let , and let be a propositional variable. We can then define:
With this notation in hand, we can state the following:
We can always represent a transition relation as a propositional formula in disjunctive normal form, where:
For many boolean functions (, , 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 ).
For instance, for a bit ripplecarry adder can be encoded with:
 Initial state
 Input numbers
 Output
The formula for the adder with auxiliary variables (serving as the carry) is:
The initial carry is . 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 as formulas. The grammar of this language is:
Where denotes variable identifiers.
QBF
Having looked at boolean formulas let’s now look at a small generalization, QBFs:
Quantified Boolean Formulas (QBFs) is built from:
 Propositional variables
 Constants and
 Operators
We will use as alternative notation for . A boolean formula is QBF without quantifiers ( and ).
Free variables
The free variables of a formula is the set of variables that are not bound by a quantifier:
Environment
An environment is a partial map from propositional variables to (“false” or “true”).
Consider two vectors and of propositional variables. We denote the environment as a mapping given by ,
We denote the result of evaluating a boolean expression with the environment as . This can evaluate to (“false”) or (“true”).
While the formula might seem weird at first (we defined in terms of another , it makes more sense if we think about the first 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:
We write to denote that is true in environment , i.e. that .
Substitution
Let and be propositional formulas, and let be a variable. Let denote the result of replacing each occurrence of in by :
We’ll also introduce a general notation to simultaneously replace many variables: denotes the substitution of a vector of variables with a vector of expressions .
Validity, Satisfiability and Equivalence
A formula is satisfiable
Note that if is not satisfiable, it is unsatisfiable, which means .
A formula is valid
is valid is unsatisfiable.
The proof should follow quite trivially from the definitions.
Formulas and are equivalent environment defined for all free variables in , we have:
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).
and are equivalent the formula is valid.
Bounded model checking
Formula representation of sequential circuits
We represent a sequential circuit as a 5tuple where:
 is the vector of state variables
 is a boolean formula describing the initial state
 is a boolean formula called the transition formula
 is the vector of auxiliary variables
 is the vector of input variables
The boolean formula tells us which states we can start in, so it can only contain state variables:
The transition formula can only contain state (), nextstate (), auxiliary () or input () variables:
The sequential circuit is a representation of a transition system , where:
 , meaning that the initial states of a transition system is given by an assignment of state variables that verifies the formula
 , meaning that the transition relation is given by a mapping of states and inputs to nextstates , 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 of a transition system , and a formula , how can we check that is an inductive invariant? According to the definition, we require:
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:
 to check if there is an initial state not included in the invariant.

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 as determining the assignment of . Then, seeing that contains variables and , it will fix the assignment for the next states . 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 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 steps.
Let be the error formula corresponding to the error state, so . When we talked about circuits, we said that the state and inputs change at each step, so let us denote the state at step as , and the inputs at step as .
We’ll construct an error formula that is satisfiable if and only if there exists a trace of length starting from the initial state that satisfies :
This formula starts at the initial state, then computes all states , and plugs in the final state 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 is satisfiable. The problem is NPcomplete, but useful heuristics exist.
A SAT solver is a program that given a boolean formula either:
 Returns
SAT
and optionally an environment such that  Returns
UNSAT
and optionally a proof that no satisfying assignment exists
Formal proof system
Let’s consider a set of logical formulas (e.g. propositional logic).
A proof system is a pair where 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 , denotes all finite sequences with elements from
An inference step is a 2tuple , which we can denote as:
We say that from the premises , we derive the conclusion .
We say that an inference step is called an axiom when , i.e. that it has no premises:
Given a proof system , a proof is a finite sequence of inference steps such that, for every inference step , each premise 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 .
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:
The inference rules are , where:
The first two rules are axioms, telling us that an implication is true if the righthand side is true (), and that implication is distributive (). We might recognize modus ponens in the last rule.
We can use these rules to construct a proof of . 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:
Given where , and given a set of assumptions , a derivation from in is a proof in where:
In other words, assumptions from are just treated as axioms (i.e. they are rules that have no prerequisites, hence ). A derivation is a proof that starts from assumptions.
We say that “a formula is provable from a set of assumptions ”, denoted , there exists a derivation from in that contains an inference step whose conclusion is .
We write (or simply ) to denote that there exists a proof in containing as a conclusion.
Consequence and soundness in propositional logic
Given a set of assumptions , where is in propositional logic, and given , we say that is a semantic consequence of , denoted , for every environment that defines all variables in , we have:
In other words, iff an environment makes all assumptions true, and is true in an environment when the set of assumptions are all true in that environment, then we call a semantic consequence.
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 is an axiom (which has no precondition, meaning that in the above), this definition of soundness means that is always a valid formula. We call this a tautology.
Let where are propositional logic formulas. If every inference rule in is sound, then implies .
This theorem tells us that that if all the inference rules are sound, then is a semantic consequence of if is provable from . 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 implies that is a tautology.
Proving unsatisfiability
Let’s take a look at two propositional formulas and . These are semantically equivalent if and .
We can prove equivalence by repeatedly applying the following “case analysis” rule, which replaces a given variable by 0 in and by 1 in :
This is sound, because if we consider an environment defining , and assume and , then:
 if then
 if then
In either case remains true when and 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:
Those rules together form the sound system , where:
Remember that a set of formulas is satisfiable if there exists an environment such that for every formula , . We can use to conclude unsatisfiability:
If then is unsatisfiable
Here, means false. This follows from the soundness of . More interestingly, the converse is also true.
If a finite set is unsatisfiable, then
This means that unsatisfiable .
For the proof, we can take the conjunction of formulas in and existentially quantify it to get (i.e. )
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 or its negation
This is a nice form to work with, because we have the following property: if is a clause then there exists a literal such that .
We can represent formulas in CNF as a set of sets. For instance:
The false value can be represented as the empty clause . Note that seeing an empty clause in CNF means that the whole formula is unsatisfiable.
Clausal resolution
This rule resolves two clauses with respect to . It says that if clause contains , and clause contains , then we can remove the variable from the clauses and merge them.
Clausal resolution is sound for all clauses and propositional variables .
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:
A finite set of clauses is satisfiable there exists a derivation to the empty clause from using clausal resolution.
Unit resolution
A unit clause is a clause that has precisely one literal: it’s of the form where is a literal. Note that the literal in a unit clause must be true.
Given a literal we define the dual as and .
Unit resolution is a special case of resolution where at least one of the clauses is a unit clause.
This is sound (if is true then is false and can thus be removed from another clause ). When applying this rule we get a clause : this gives us progress towards , which is good.
Equivalence and equisatisfiability
Let’s recall that two formulas and are satisfiable iff and . TODO is this a typo? Should it be “equivalent”?
Two formulas and are equisatisfiable is satisfiable whenever 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 and are two formulas, and we let be a fresh variable, then is equisatisfiable with:
Tseytin’s transformation applies this recursively in order to transform an expression to CNF. To show this, let’s consider a formula using :
The transformation works by introducing a fresh variable for each operation (we can think of it as being for each AST node):
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 and . The resulting conversions are:
Operation  CNF 

Note that the Tseytin transformations can be read as implications. For instance, the transformation can be read as:
 If and are true, then is true
 If is false, then is false
 If is false, then is false
It then takes the conjunction of all these equivalences:
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.
Nonchronological 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 , and point to the conflicting pair of ’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:
We can then backtrack to the first decision where we set , or (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.
2literal watching
This algorithm does the standard trick of unit propagation, but avoids expensive bookkeeping 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 nonnegated 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 be a boolean formula over state and input variables.
We write to say that a trace satisfies formula at time . The rules for the above constructs are:
We can interpret until to mean that is true until 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 once is true.
Note that next and prev, and since and until are duals of each other^{3}.
We can add some derived operations from these:
The operation globally can be thought of as meaning “forever, from now on” (where “now” is step ). For instance, means that from now on, every point in the trace satisfying is followed by a point in the trace satisfying at some point.
Binary Decision Diagrams
Definition
Binary Decision Diagrams (BDDs) are a representation of Boolean functions: we can represent a Boolean function as a directed acyclic graph (DAG). We distinguish terminal from nonterminal 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 is:
We can also think of this DAG as a finite automaton, or as a (loopfree) 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 as our ordering. Note that in general, selecting a good ordering is an intractable problem, but decent applicationspecific heuristics exist.
Then, the reduced ordered BDD (ROBDD) 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:
With a fixed variable order, the ROBDD for a Boolean function is unique
In the following, we’ll always refer to ROBDDs, 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 . We also number the levels in the diagram, according to the total ordering that we selected: level 1 is the root node, and level contains terminal nodes.
A data structure for BDDs is the node table , mapping a node to its low child and high child . The node table also contains an entry 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  Level and name  Low edge  High edge 

0  3  
1  3  
2  2  0  1 
3  1  2  1 
We’ll assume we have some methods for querying this table:

init(T)
: initialize with 0 and 1 terminal nodes 
u = add(T, i, l, h)
: add node with to 
var(u)
: get of node 
low(u)
: get of node 
high(u)
: get of node
We can also define the inverse 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 with 0 and 1 terminal nodes 
u = lookup(H, i, l, h)
: get node from 
insert(H, i, l, h, u)
: add an entry from to
Basic operations on BDDs
Somewhat surprisingly, given a BDD for a formula , we can check whether it is a tautology, satisfiable or inconsistent in constant time:
 is a tautology the BDD is
 is satisfiable the BDD is not
 their BDDs are equal^{4}
To insert a node into , we ensure that we’re keeping a ROBDD by eliminating redundant tests, and preventing isomorphic nodes. If that is not the case, we can update the tabée and the reverse mapping .
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 . The key idea is to use Shannon’s expansion:
Here, means that we replace all nodes by their highedge subtree. In the formula, we can think of it as a substitution of 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)
}
Interpolationbased model checking
Interpolation
Let and be propositional formulas. An interpolant for and is a formula such that:
Note that if these conditions hold, we have . The goal of is to serve as an explanation of why implies , using variables that the two have in common.
Let and be propositional formulas such that and let be the set of interpolants of . Then:
 If then and
For instance, let’s consider two formulas and . The variables they have in common are so we’re looking for an interpolant .
Reverse interpolants
We know that . The negation of this is . Let and . Instead of looking at the validity of , we can look at unsatisfiability of . To aid us in this, we’ll define as an interpolant for , meaning that we have:
 , meaning that
As previously seen, we can determine whether 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 for .
Let’s define as the interpolant for and , where denotes the clause , but only with literals belong in . The idea here is that we can construct it recursively, and that is the interpolant for and .
There are multiple ways of constructing this , 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 and to and , and that the newly introduced variables are and , respectively. The results of the Tseytin transformations are:
The interpolant for and is also an interpolant for and
We’ll prove this by showing that all three properties of interpolants are preserved:
 todo
 todo

By assumption of being an interpolant for and , we have:
The second step is by the above definition of the transformation’s results. The last step is because and are disjoint.
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 that is satisfiable iff there exists a trace of length starting from the initial state, satisfying an error formula .
 Also, recall the function.
Reachability checking
To check for reachability, we can keep adding to the set of reachable states until one of the following two situations arises:
 We reach a fixpoint: )
 We find that an error state is reachable: .
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 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 formula: instead of , we’ll only look at . 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 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 still denotes recursive applications of the function.
Let denote any overapproximation of :
We’ll consider a monotonic ^{5}, meaning that:
Now, consider the following sequence:
…  … 
The relationship here is that:
This means that we can replace with recursive applications of different 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#[i1](post#[i2](...))
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 .
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 , and how to continue from there. Let’s look at the formula for bounded model checking again:
To simplify the formula a little, we’ll define:
This allows us to rewrite the formula as:
We define and as above, and are now interested in finding an interpolant between the two. The first thing we can look at is which variables and have in common; by the third property of interpolants:
We also need the two first properties of interpolants:

, which is equivalent to . Intuitively, this is like , so we can define . This is a valid approximation, as .

, which is equivalent to . We can just impose the constraint of to prevent from being too general.
Once we have an approximation for , we can find the by treating as the new 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 and terms :
Where:
 denotes a variable
 denotes a predicate symbol
 denotes a function symbol
 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 . For instance, if