formal-methods-lab

Exercises and homeworks for the Formal Methods lab (2022) at the University of Trento.

Lab1

• Introduction to SAT solving
• Dimacs
• Mathsat (introduction)
• SMT-LIB

Lab2

• Pysmt
• Incremental SAT
• UNSAT cores

Lab3

• Mathsat (Bool, Int, Real)
• Interpreted functions
• AllSAT

Lab4

• BitVectors
• Arrays
• Uninterpreted functions

Lab5

• OptiMathSat

Lab 6

• Multi-objective optimization
• Minmax/maxmin
• Simulation of exam exercise: pseudo-Booleans and linear combinations

Lab7

• Introduction to nuXmv
• nuXmv: the adder circuit

Lab8

• Encode programs using nuXmv
• Checking mutual exclusion using nuXmv
• Chemical reactions using nuXmv

Lab9

• nuXmv for planning

Lab10

• Bounded Model Checking
• K-Invariant
• Exercises done:
  • Cleaning Robot
  • Number Paranoia
  • Cannibals