LARA

Labs 06: SMT-based verifier for a language with integer state and recursion

In this lab, we have a verifier for a small imperative language with recursive procedures. In Verification.scala, we generate verification conditions for the post-conditions of each procedure, and invoke Z3 to know whether they are unsatisfiable (and the post-condition is valid) or satisfiable (and the post-condition has a counter-example). You must have a z3 binary in your path for this to work.

You task is to complete the relation function. This function takes a statement and generates an expression that represents the meaning of the statement (by using the original variables and their primed version). In the Compose case, we generate a fresh copy of the global variables, to represent the state in between the two statements.

To test your code, you can use sbt “run examples/valid/Fact.scala” (or other examples). Please make sure that your code passes all examples by using sbt test.

A few hints:

  • Except for the Compose case, you should not generate fresh copies of the global variables, and you should not update the fresh variable.
  • The arguments/parameters of procedures are immutable, the arguments of the procedure that we are verifying (and only those) can appear in the formula.
  • Old expressions refer to variables at the beginning of the function. In the ProcedureInvocation case, make sure that you replace the Old expressions with the appropriate variables.
  • You are provided with helper functions such as replace and subst on expressions.