In computer science, a special place in modelling belongs to mathematical logic. Given a yes/no question formulated in a logical language, a decision procedure produces a correct yes/no answer.
This module focuses on decision procedures for first-order logical theories. A common term for describing this field is Satisfiability Modulo Theories (SMT). Satisfiability (SAT) solvers and SMT solvers are software tools that implement decision procedures. They are used in practice to solve difficult combinatorial problems related to chip design, software and hardware verification, planning, and other applications.
Since the ability of these techniques to cope with problems arising in industry depends critically on decision procedures, this is a vibrant and prospering research subject for many researchers around the world, both in academia and in industry.
Intel and AMD, for example, are developing and using theorem provers and decision procedures as part of their efforts to build circuit verification tools with ever-growing capacity. Microsoft is developing and routinely using decision procedures in several code analysis tools. In 2022 Amazon reported running billions of SMT queries daily to offer their cloud service customers configurable and rigorously enforced security policies.
The aim is for the students to become familiar with the modelling, logical, algorithmic and implementation 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.
The theories covered in this module are all used in practice. We illustrate applications of each theory with examples representative of real problems, whether they may be verification of C programs, verification of hardware circuits, or optimizing compilers.
This is an indicative module outline only to give an indication of the sort of topics that may be covered. Actual sessions held may differ.
Decision procedures for propositional 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.
By the end of the module, students should be able to:
Reading lists can be found in Talis
Interpretation of terms and formulas in logical theories.
Automation of reasoning with the use of decision procedures:
Identification of an appropriate logic based on a problem description in natural language.
Translation of problems from natural language into logical formulas (logical modelling).
Application of decision procedures for theories and combinations of theories to logical formulas.
Analysis of decision procedures with respect to computational complexity.
Use and development of software for automated reasoning.
Formalisation of problems. Identification of ambiguities and unknowns in problem description. Identification of constraints in problem description.
Algorithmic thinking. Use and development of software tools to solve problems.
| Type | Required |
|---|---|
| Lectures | 20 sessions of 1 hour (13%) |
| Seminars | 10 sessions of 1 hour (7%) |
| Practical classes | 10 sessions of 1 hour (7%) |
| Private study | 65 hours (43%) |
| Assessment | 45 hours (30%) |
| Total | 150 hours |
Concepts and algorithms covered in the module will be put into practice in module coursework (45 hours private study) as well as the timetabled lab sessions.
Students are also expected to engage in self-study to absorb content and prepare for the examination (65 hours).
No further costs have been identified for this module.
You do not need to pass all assessment components to pass the module.
Students can register for this module without taking any assessment.
| Weighting | Study time | Eligible for self-certification | |
|---|---|---|---|
| Practical assignment | 30% | 45 hours | No |
|
A programming assignment which will target problem solving using decision procedures. |
|||
| CS415 Exam | 70% | No | |
|
In-person examination
|
|||
| Weighting | Study time | Eligible for self-certification | |
|---|---|---|---|
| CS415 Resit Exam | 100% | No | |
|
|||
This module is Optional for:
This module is Option list A for:
This module is Option list B for: