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. On the campus machines, you can access it via "/courses/TDDE34/Spin/bin/spin" (or "/courses/TDDE34/Spin/bin/ispin.tcl" for the gui interface).

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 via "/courses/TDDE34/NuSMV/bin/NuSMV". It is a good idea to copy the examples (at /courses/TDDE34/NuSMV/share/nusmv/examples) to your own directory to experiment with the model checker. Those described in the tutorial are under 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 to create the following symbolic links:

  ln -s /courses/TDDE34/CPAchecker/scripts
  ln -s /courses/TDDE34/CPAchecker/doc
  ln -s /courses/TDDE34/CPAchecker/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: 2024-03-27