CS415 Decision Procedures
Academic Aims
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.
Learning Outcomes
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.
Content
- 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.