Software Verification
2023-2024
TP3: Bounded Model Checking

Vincent Penelle

Content



The goal of this lab is to make you program two modules: DepthFirstBMC.ml and GlobalBMC.ml of our tool, Simple Program Analyser. These modules will each implement an algorithm for Bounded Model-Checking exploring the execution tree, the first in depth, the second level by level thanks to the unfolding of the step formula.

Rappel:

A control-flow automaton is a tuple (Q,qi,qbad,Δ) where Q is a finite set of states, qiQ is the initial state, qbad is the final state (or "bad"), and Δ ⊆ Q × Op × Q is the set of transitions, where Op is the set of possible operation of the automaton. This set is defined hereafter. Said otherwise, it is an automaton labelled with operations (over variables)

We consider a set of variables X. An expression is an arithmetical expression over ℤ containing or not variables from X:

exp ::= n ∈ ℤ | x ∈ X | exp + exp | exp − exp | exp × exp | exp / exp

A guard is a comparison between two expressions:

guard ::= exp = exp | exp < exp | exp ≤ exp | exp > exp | exp ≥ exp

An operation is either skip, or a guard, or an affectation of the form x := exp, for xX and exp an arithmetical expression:

op ::= skip | guard | x := exp

(cf TP précédent pour plus de détails sur les opérations et leur sémantique)

Point technique:

A configuration of a control-flow automaton A is a pair (q,σ), where q is a state, and σ a function from X to ℤ called valuation.

The semantic of a operation op is a relation containing valuations (σ12) such that σ2 can be obtained by applying op to σ1. Formally, we have [| skip |] = id, [| guard |] is the set containing all (σ,σ) such that σ satisfies the guard, and [| x := exp |] = {(σ,σ[x:=exp])}. Cf last lab session for more details on the implementation of the semantics in an FO formula.

The semantic of a transition t = (q,op,q′) is the binary relation →t on configurations defined by ct c′ if c = (q,σ), c′ = (q′,σ′) and (σ,σ′) ∈ [| op |].

The step relationA is the union of semantics of all transitions of A .

Am execution is a sequence c0, t1, c1, …, tn, cn alternating configurations ci and transitions ti such that ci−1ti ci for all 0 < in. Such a execution is also written c0t1 c1 ⋯ →tn cn for improved readability, and n is its length.

A path q0, op1, q1, …, opn, qn is said to be executable if there exist valuations ρ0, …, ρn ∈ ℤX such that (q0, ρ0) →t1 (q1, ρ1) ⋯ →tn (qn, ρn) is an execution, with ti = (qi−1, opi, qi).

Point technique:

The bounded model-checking problem asks, given a control-flow automaton A and a bound k ∈ ℕ, whether there exist two configurations (q,ρ) and (q′,ρ′) such that:

The problem can be equivalently expressed as: Does there exist an executable path of lenght at most k from qi to qbad.

The algorithm of bounded model-checking can simply be summarised as follows: enumerate every paths of lenght at most k, and as soon as we find an executable one from initial to target state, return that path.

Of course, there exist several possible exploration order of these paths, and some simple but efficient optimisations (namely, it is useless to consider a path whose one of the prefixes is not executable). We can also ask to the program to determine if it did an exhaustive exploration or not (whether longer executions exist).

For now, we will implement a depth-first exploration order: given an (arbitrary) order on transitions, look first all paths starting by the first, then the second, etc. As soon as either the bound is reached or a non-executable path is found, we backtrack one level and continue to explore from there. As soon that a faulty execution is reached, we stop exploration and return it.

More precisely, the (recursive) algorithm receives as argument a CFA A, a path τ, a current state q, the current depth ℓ, and the bound k, and can be summarised as follows:

The algorithm is called on (A,(qi),qi,0,k) to perform bounded model-checking with bound k on the automaton A.

Exercice 1: Depth-first search bounded model-checking

Download the sources of the lab session. In DepthFirstBMC.ml, you have to implement dfs which performs the depth-first exploration of the tree described above. The commentary above the prototype contains all elements needed to help you implementing it, especially by adapting the arguments to facilitate the computation (e.g. by retaining a formula to describe the path up to the current state, instead of the path itself). There will be some subtlety left to you to return correctly the faulty execution.

You can also test your program over the given examples and compare with the given working executable bmc.solution.d.byte.

Point technique:

The global algorithm consist in determining, length by length up to the bound, whether there exists a faulty run of that length. It is equivalent to ask if, for a length k, there exist states q1,⋯,qk−1 and valuations X0,⋯,Xk, such that (qin,X0A (q1,X1) →A ⋯ →A (qk−1,Xk−1) →A (qbad,Xk).

To this end, we start by computing the formula φstep of the automaton, relating two configuration if and only if the automaton allows to go from one to the other. With it, for each length i up to the bound, we check whether the following formula is satisfiable:

  ψi(q0,X0,⋯,qi,Xi)  
def
=
 
    q0 = qin ∧ 
i
j = 1
 ϕstep(qj−1, Xj−1, qj, Xj) ∧ qi = qbad

If so, we have the existence of a faulty execution (and we must reconstruct it from the model of the formula, knowing that some information are missing in the formula given here). If not, there is no faulty execution of length i. If we treated length one by one, we can thus follow through to the next.

Note that it is useless to test ψi if no execution of length i exist. To determine it, it is sufficient to ask the solver to satisfy ψi without ensure that the last state is qbad (i.e., without the red part). If so, we have to continue to explore, but if it is unsatisfiable, there is no execution of length i, and we can certify the program to be correct (exhaustive exploration).

Exercice 2: Global bounded model-checking

In GlobalBMC.ml, implement the function asked for. Indications are given there. Do not hesitate to implement auxiliary functions. In Z3Helper.mli, you have functions to help you manipulate states and transitions of the automaton in the formula.

Start with implementing a version without caring about sending back the counter-example, then, when it works as indented, modify it to send the counter-example.


This document was translated from LATEX by HEVEA.