Directed Studies: Decision Procedures for Software Verification
Schedule:
- Course (Prof. Dr. Stefan Leue)
Wednesday 10:00 - 11:30 Room PZ 901 Start: 12 April 2023 - Tutorial (David Boetius)
Wednesday 17:00 - 18:30 Room PZ 901 Start: 19 April 2023 rescheduled
Description:
Prerequisites
Undergraduate standing in Algorithms, Programming, Discrete Structures (in particular formal logic), Theory of Computing.
Contents
Software is logic at work, and hence formal mathematical logic is the calculus of software engineering. In the verification of properties of software systems special decidable fragments of first order logic have received special interest and lots of tools have been developed under the label "Satisfiability Modulo Theories" (SMT). Companies like Google and Microsoft, for instance, use this technology to analyze their software eco systems for security vulnerabilities.
In this directed studies course we will provide a brief introduction into propositional and first order logic. We will then discuss more SMT specific logics and decision procedures, including DPLL(T) for SAT solving, the Nelson-Oppen combination procedure, uninterpreted functions, linear real and integer arithmetic, and quantifier elimination. In addition, we will consider logics and procedures relevant to software verification problems, including the treatment of arrays and pointers, and provide application examples.
Teaching methods
Further details on the course will be provided in ILIAS.
Please register in ZEuS for the course, which will register you automatically in ILIAS as well.
Directed Studies Course - weekly reading assignments that will be presented by participants and discussed during the lectures.
Workload
180 hours, of which 56 hours are spent in class and 124 hours of self study.
Learning objectives
Participants will learn the foundations of SMT technologies. This will enable them to assess SMT technology in its usefulness for solving various problems in academia and industrial practice, and to use this technology in own related projects.
Course literature
Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, second edition, Springer 2016.
Further literature may be announced during the course.
Target group
BA-Students 4. Semester
MA-Students
Remark
Final examination - oral 30 min. A grade bonus can be earned during the tutorials.
Expected course achievement
At least one weekly assignment summary presentation.
Offering Suitable for Participants from Other Programs and Subject Areas
All
Credits
ECTS-points: 6
Weekly teaching hours
SWS: 2 (+ Tutorial: 2)