TDDE34 Software Verification

Lab work for TDDE34

Rules

Before you read the information on this Web page and before you register for the labs, please spend some time to read the rules that we apply to conduct the laboratory work in this course.

• It is prohibited to use AI tools, including those included into text editors or IDEs, to generate (parts of) the code or the reports. This is the case even if modifications are introduced.
• Submitted code and reports MUST BE YOURS. If we suspect generative AI tools were used against the rule above, we will report to the disciplinary board.
• You may (this is not a recommendation) use such tools for general conceptual questions. Be however always very critical due to hallucinations and errors. Always cross-check with other sources
• You cannot use AI tools to answer any of the questions during the demonstration.

In addition to the above,

• A lab group consists of 1 or 2 students. We (strongly) recommend working in pairs, both for qualitative and for quantitative reasons.
• Demonstrations are individual examinations, even if they are typically conducted in pairs. Each member of the pair should be able to answer any question about any part of the submission. Failure to do so will be considered as a misleading attempt.

If you have any questions, or if you are not sure about the exact meaning of any of the rules, you must consult the course leader or the lab assistant before you start working with the labs.

The lab work

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 8th.

• 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 "spin-lab.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.

Axiomatic reasoning

The assignment description can be obtained by downloading the "dafny-lab.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")
  

Symbolic verification

The assignment description can be obtained by downloading the "nusmv-lab.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".

Abstraction and over-approximations

The assignment description can be obtained by downloading the "ai.pdf" file. (Being updated, coming soon).

Page responsible: Ahmed Rezine
Last updated: 2026-03-23