Directed Studies: Satisfiability Modulo Theories

Schedule

  • Directed Studies (Prof. Dr. Stefan Leue)
    Wednesday 10:00 - 11:30  Room: PZ 901 (instead of PZ 1001 as announced in LSF)
  • Tutorial (Georgiana Caltais)
    Tuesday 10:00 - 11:30  Room: PZ 901
  • The preliminary talk will take place at 10:00 on Thursday, 
    t.b.A

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 Amazon Web Services and Microsoft, for instance, use this technology to analyze their operating and cloud 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. 

Participants

Bachelor degree in Computer Science level knowledge of Software Engineering, Discrete Mathematics, Programming and Theory of Computation.

Subject Area

Informatik der Systeme / Angewandte Informatik 

Contents / Syllabus

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 taught entirely in English.

Final examination - oral. A grade bonus can be earned during the tutorials.

Literature

Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, second edition, Springer 2016. http://www.decision-procedures.org
Further literature references may be suggested during the lectures.

Credits

SWS: 4
ECTS-points: 6

All the materials are available on the ilias webpage of the course.