CSE308 - Tutorial 8 - SAT-Based Unbounded Model Checking

Setup

You should already have installed pysmt and a sat solver on your system and the NuSMV model checker.

You can run in the terminal the command pysmt-install --check and check what you currently have installed. You’ll see something like this:

Installed Solvers:
  msat      True (5.6.1)
  cvc4      False (None)              Not in Python's path!
  z3        True (4.8.7)
  yices     False (None)              Not in Python's path!
  btor      False (None)              Not in Python's path!
  picosat   False (None)              Not in Python's path!
  bdd       True (2.0.3)

Make sure at least a smt solver is on your system (z3 will do).

Download and extract the files of the tutorial CSE308-TD8-1-handin.zip. You’ll have a folder called CSE308-TD8-1-handin.

Evaluation

You will receive a maximum 20 points, subdivided as follows:

• Implementation of k-induction: 5 points
• toy1: 5 points
• toy2_bounded: 5 points
• toy2_unbounded: 5 points

K-Induction

You will first implement the k-induction algorithm in the function:

def kind(ts : SymbolicTS, prop: BoolFormula, max_k : int) -> bool

in the file mc308/td8.py. The function takes as input a transition system and an invariant properties, and returns true if the property holds, false if it does not hold, and None if the induction step did not prove the property up to the maximum bound max_k.

NOTE: the function should check in sequence the induction for 0, 1, 2, … k-s.

You can test your implementation using the td8_script.py file (it loads some models from you from the td8_models folder).

Verifying systems with K-induction

You will apply K-induction to verify some simple transition systems. While K-induction is a complete verification algorithm, you will see that even in simple cases you may need to provide more help to the verification algorithm (i.e., prove some other simple invariants).

Toy

You will verify the transition system modeled in the toy_solve.smv file.

The system:

• has a single variable of type signed word of length 32. This means the variable has 32 bits (32 boolean variables) and all the operations on the variable (e.g., equality, comparisons, sum) works respecting the two’s complement representation. If you need a refresher, look here.

• the counter starts from 0 and counts up to 0sh32_7FFFFFFF.

You have to prove that the counter never reaches the value -0sd32_1 (-1, which is 0xFFFFFFFF in hexadecimal).

Intuitively the property holds: the counter starts from 0 and it always increments until it reaches the greatest positive number 0sh32_7FFFFFFF.

You could try and prove the property using k-induction in your code, you can load the same SMV model using the file toy_solve.smv file.

The commands to use k-induction are:

go_bmc
check_invar_bmc -a een-sorensson -k 10

Here, een-sorensson is a version of the k-induction algorithm (slightly stronger than the one we saw in class) and k is the bound of the search.

You can also use your implementation to try things out, you can load an equivalent model to the smv file using the corresponding vmt file you find in the same folder as follows:

with open("toy_solve.vmt", 'r') as f:
  sts, invars, live = from_vmt(f)

kind(sts, invars[0], 10) # use k-induction on the first invariant property of the model.

K-induction will not be able to prove the property as is with a reasonable bound. Instead, a standard technique is the following (i.e., strengthening the inductive check):

• think about other invariant properties that may hold in the system and may help to prove what are you interested in with k-induction.

• once you have a candidate, you can see if it is really an invariant (i.e., prove it holds using k-induction).

• at this point, you can add the invariant property in your model. You can add an INVAR constraint in the SMV file or, if you are using your implementation of k-induction, you can use the function add_invar in the SymbolicTS class to add an invariant when you have one. Of course, this step is sound if you proved the formula you have to be an invariant.

Adding other invariant properties strengthen the inductive reasoning of k-induction (intuitively, it cuts states that are not reachable from the initial states and are on a path that do not satisfy the inductive step), so you may be able to prove a property with a lower bound k.

To understand better what invariant to add, you may want to print a “counter-example to induction” when the inductive step fails. In that case you have a satisfying assignment that correspond to an uninitialized path that fails the induction step. This path gives you some hint about the invariant you may need to prove.

You will submit the file toy_solve.smv as a solution (add your INVAR or multiple invariants). Note that you get a solution if all the formulas you add are an invariant and all can be proved with the check_invar_bmc command as you saw earlier.

Toy2 (bounded)

You will work on the model defined in the toy2_bounded.smv file. This model:

• Has 2 counters, each one is smilar to the one we saw before. Both counters increment their value synchronously.

• Both counters stop incremementing their value as soon as at least one of them reaches the maximum value (defined in MAX_C, which is 0sh32_7FFFFFFF). The two counters stop together once either one reaches the maximum value MAX_C.

• The initial value of the two counters is not set to 0, but it can start from a different value according to the INIT constraints (and also from a negative number).

• Interestingly, the initial constraints also impose other limitations on the counter value of c0 and c1. Try to understand what these constraint say.

• Your goal is to prove that c1.val != bound, where bound is the value MAX_C - offset.

• Note that MAX_C is our usual constant, while offset is a value between 0 and 5 (note that offset is declared as a FROZENVAR, meaning its value never change in a transition).

Try to prove the property via k-induction. You will need to provide an additional invariant to succeeed (use the same method as above). Add the INVAR constraint you need to the toy2_bounded.smv file.

Toy2 (unbounded)

You will work on the model defined in the toy2_unbounded.smv file. This model is exactly as the previous one, except the value of the offset variable: now the variable is greater or equal than 0, but the upper value is not bounded.

Try to prove the usual property (c1.val != bound) via k-induction (you may already have the right invariant, depending on how you solved the previous exercise).

Submit your work

You’ll have to upload the following files: