CSE308 - Tutorial 8 - SAT-Based Unbounded Model Checking

Setup

You should already have all the dependencies on your system.

In case, run in the terminal the command pysmt-install --check and check you have a SAT (or SMT solver) installed. Your output will be something like:

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)

IMPORTANT: for implementing k-induction you just need a SAT solver. So, all is ok if you just have any of the following installed (True value in the column): msat, cvc4, z3,yices,picosat.

IMPORTANT: for implementing the interpolant-based algorithm, you will need the solver msat installed (the pysmt api does not link the interpolation functions for the others)

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

Troubleshoting msat installation

If you don’t have msat installed, try to install it:

$ pysmt-install --msat

If the instatllation fails with a 500 error https request, then you need to update the pysmt package with pip:

$ pip install --upgrade --pre pysmt

At this point you can try to install msat again (pysmt-install...).

If this does not work, you can try on the lab machines (you need to upgrade with –pre also there).

Evaluation

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

• K-induction: 5 points
• Verifying systems with K-induction: 10 points
• Interpolation: 5 points

Deadline.

The deadline for submitting the exercise to obtain a full grade is Thursday June 5th at 23:59. You can submit your work after that deadline but you will receive only 50% of the total grade.

K-Induction

You will 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 apparently simple transition systems.

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 varible (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 reach 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.

Try to prove the property using k-induction in your code, you can load the same SMV model using the file toy_solve.vmt (this is just a different format than SMV that we can read easily).

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.

The toy_solve.vmt was not in the initial archive. You can download it here. The vmt file is just a translation of the smv file that we can read easily in python.

IMPORTANT: The k-induction algorithm may not be able to prove the property with a “reasonable” bound. A standard technique is the following (i.e., strengthening the inductive check):

• think about other invariant that holds in the system (hint: sign of the counter variable).

• 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 it’s correct to add that invariant in your model (e.g., add the invariant formula to the initial states and transition relation)

  Use the function add_invar in the SymbolicTS class to add an invariant when you have one.

• As additional hint, 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 (you can use code from TD7).

Once you proved the property, add the invariant to the toy_solve.smv file (INVAR constraint). You will submit that file as solution.

Adding other invariant properties strengthen the inductive reasoning of k-induction – so you may be able to prove a property with a lower bound k.

Toy2 (bounded)

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

• Has 2 counters smilar to the one we saw before. However, 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 initial value of the two counters is also not 0, so the counter can start from a negative number.

• Interestingly, the initial constraints also impose other limitations on the counter value (see the INIT constraint). Try to understand what these constraint says.

• 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.

Download toy2_bounded.vmt.

Toy2 (unbounded)

You will work on the model defined in the toy2_bounded.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 property (c1.val != bound) via k-induction. Add the INVAR constraint you need to the toy2_unbounded.smv file.

Download toy2_unbounded.vmt.

Interpolant-based model checking

You will implement the interpolation-based model checking algorithm in the function:

def itp(ts : SymbolicTS, prop: BoolFormula) -> bool

You can use the same test cases you used for testing k-induction.

For computing an interpolant, you can use the function binary_interpolant from PySmt. The function:

• takes as input two formulas (the conjunction of the two formula must be unsatisfiable!).
• returns a Craig interpolant of the two formulas.

Submit your work

You’ll have to upload the following files: