LFU:online

Participants recognize problems that can be tackled with SAT/SMT solvers, learn the theoretical foundations of such logic engines, and can successfully apply these tools in small projects of their own

How can the correctness of security-critical software and hardware be ensured? How should an airline assign flight crew to flights to minimise costs, at the same time meeting
regulations and ensuring the schedule is robust? How can a fixed number of software tests cover a maximal number of test situations? For such verification and optimization tasks SAT and SMT solvers turned out to be a catalyzer which render problems practically solvable that have long been considered infeasible. What lies behind this success?

Automatic analysis of computer hardware and software requires engines capable of reasoning efficiently about large and complex systems. Thus powerful boolean satisfiability solvers have become tools of choice for industrial verification applications already in the early 2000s. However, practical systems are usually modeled at a higher level, and translation to the Boolean setting can be expensive.
Satisfiability Modulo theories takes SAT to a more expressive level, where one can reason
natively in a rich logic supporting linear arithmetic, bitvectors, etc. Indeed SMT has been called the most promising contribution to the fields of software and hardware verification and test in the last years (by the IBM's HVC award).

Theoretical contents are covered in lectures, theoretical and programming exercises provide opportunity for application

regular exercises plus written tests

This course can be used as "Wahlmodul", see https://www.uibk.ac.at/informatik/studium/anerkennung (Zuordnungsbestätigung)