TDDE34 Software Verification

Lab work for TDDE34

The lab work of the course consists in solving, demonstrating, and submiting solutions to the following four assignments.

• You are encouraged/expected to work in pairs. Register in pairs to webreg before april 5th.

• Different pairs can only discuss at high level. Solutions to the assignments are individual to the pairs. We follow the IDA general policy for computer lab assignments. In particular concerning the concesquences of any kind of academic dishonesty.

• Demonstrate your work in a lab session for each one of the following assignements before you send your report/code.

Explicit Model Checking

The assignment description can be obtained by downloading the "homework1.pdf" file. The assignment involves modeling and verification using the spin model checker. Spin is installed on the campus machines. You can the gui interface via "/courses/TDDE34/Spin/bin/ispin.tcl". It is a good idea to copy the examples from "/courses/TDDE34/Spin/examples" to your own directory to experiment with the model checker.

Symbolic verification

The assignment description can be obtained by downloading the "homework2.pdf" file. The assignment involves modeling and verification using the NuSMV model checker. On the campus machines, you can access it after "module add courses/TDDE34", then just type NuSMV. It is a good idea to copy the examples from "/courses/TDDE34/NuSMV/share/nusmv/examples" to your own directory to experiment with the model checker. Those described in the tutorial are under "/courses/TDDE34/NuSMV/share/nusmv/examples/smv-dist".

Axiomatic reasoning

The assignment description can be obtained by downloading the "homework3.pdf" file. The assignment involves writing and verifying programs using the Dafny programming language and verification framework. Checkout-out this turorial. Dafny can be easily installed on your machine and can be combined with emacs or visual code.

On the campus machines, you can use dafny directly via the command line (just type dafny and the name of the dafny-file, e.g. dafny abs.dfy) or via emacs by setting up melpa and installing the boogie-friends package (see the setup section here). You can use the following paths to a dafny installation on the campus machines:

  (setq flycheck-dafny-executable "/courses/TDDE34/Dafny/dafny")
  (setq flycheck-z3-smt2-executable "/courses/TDDE34/Dafny/z3/bin/z3")
  (setq flycheck-inferior-dafny-executable "/courses/TDDE34/Dafny/DafnyLanguageServer")
  

Abstraction and over-approximations

The assignment description can be obtained by downloading the "homework4.pdf" file. You can create a folder for this lab under your home directory and create the following symbolic links (after you "module add courses/TDDE34"):

  ln -s /opt/liu/cpachecker/3.0/0/scripts
  ln -s /opt/liu/cpachecker/3.0/0/doc
  ln -s /opt/liu/cpachecker/3.0/0/config

You can then launch an analyis from within the folder with:

  /scripts/cpa.sh -predicateAnalysis doc/examples/example.c

Page responsible: Ahmed Rezine
Last updated: 2025-04-02