CS415 15 CATS (7.5 ECTS) Term 1
Option - MEng CS and DM
The aim of this course is for the students to become familiar with the modelling, logical, algorithmic and implementational aspects of decision procedures for first-order theories that are useful in the context of automated verification and reasoning, theorem proving, compiler optimization, synthesis and so forth.
At the end of the module the student should be able to:
- Select and apply techniques from mathematical logic, linear algebra, algorithmic graph theory and other areas to construct decision procedures for a wide range of useful first-order theories.
- Recognise and compare theories with respect to their utility in modelling real decision problems, and their amenability to efficient solvability in practice.
- Implement cutting-edge decision procedures on top of an extensible template, in an industry-standard language such as C++
- Evaluate decision procedures using international repositories of relevant benchmarks.
- Decision procedures for propositonal logic, equality logic and uninterpreted functions. SAT solvers, binary decision diagrams, small-domain instantiations.
- Decision procedures for linear arithmetic, bit vectors, arrays and pointers. Simplex, branch and bound, bit-vector arithmetic, software verification.
- Theories with quantifiers, combining theories, propositional encodings.
- Implementation in C++, benchmarks, SMT solvers.
- Daniel Kroening and Ofer Strichman. Decision Procedures, An Algorithmic Point of View, Springer, 2008
- Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Model checking, edited by Ed Clarke, Thomas Henzinger and Helmut Veith, 2014
- SAT/SMT/AR Summer Schools, online lecture materials. 2011 (MIT, USA), 2012 (Trento, Italy), 2013 (Espoo, Finland), 2014 (Semmering, Austria), 2015 (Stanford, USA), 2016 (Lisbon, Portugal).
Two hour examination (70%), practical assignment (30%)
20 one-hour lectures, 10 one-hour seminars plus 10 hours of practical classes/workshops