CS550 Formal Verification
Throughout these notes, vectors are denoted in bold and lowercase (e.g. ).
 Transition systems

Satisfiability checking
 Propositional boolean logic
 SAT problem
 Formal proof system
 A minimal propositional logic proof system
 Provability
 Consequence and soundness in propositional logic
 Proving unsatisfiability
 Conjunctive normal form
 Clausal resolution
 Unit resolution
 Equivalence and equisatisfiability
 Tseytin’s Transformation
 SAT Algorithms for CNF
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.
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.
An iteration describes paths of length in a relation . It is defined recursively by:
Here, describes the identity relation, i.e. a relation mapping every node to itself.
In our airport analogy, the transitive closure is the set of all airports reachable from our starting airports.
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 ”.
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 ^{1}.
 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.
Definitions and operations on formulas
To continue the discussion of encoding, we’ll have to introduce some concepts related to formulas.
QBF
We’ve looked at boolean formulas, but 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.
Formula representation
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
Propositional boolean logic
Propositional logic is a language for representing Boolean functions as formulas. The grammar of this language is:
Where denotes variable identifiers.
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
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.
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 .
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.
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!

The proof of this identity is in exercise session 1, exercise 2.1.1. It is done by decomposing into existential quantifiers. ↩