/Formal-Methods-2022

Repository containing the exercises solved during the Lab lectures for the course of Formal Methods (a.k.a. "Module 1: Automated Reasoning" and "Module 2: Model Checking") for the academic year 2021/2022

Primary LanguageSMT

Formal-Methods-2022

Surveys and tutorial about SAT/SMT

http://satassociation.org/tutorials.html

Introduction Python

For people that asked me some links to easily learn the basics of Python, please check the material from the following UniTN course: https://disi.unitn.it/~passerini/teaching/2021-2022/sci-pro/index.html. In particular, the material about "Complex statements"are really useful for our course (List Comprehension and the various loops).

Lab 1

  • Getting started with SAT solving
  • Dimacs and SMT-LIB format
  • Encoding circuits and checking equivalence
  • From real tasks to SAT models: sorting people, cracking codes

Lab 2

  • Getting started with pysmt
  • Solving logic puzzles
  • Solving Sudoku
  • Solving Nonogram
  • Functionalities: Incrementality and UNSAT cores

Lab 3

  • Using SMT-LIB: different data types
  • Solving logic puzzles using SMT
  • Solving geometric tasks
  • SAT/SMT functionalities: AllSAT/ALLSMT

Lab 4

  • Using BitVectors and Arrays
  • Uninterpreted vs interpreted functions

Lab 5

  • OptiMathSAT: defining cost functions and different types of optimizations
  • Optimization of graph shortest paths
  • MaxSAT/MaxSMT
  • The importance of PseudoBoolean for SMT

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