Decision Procedures and SMT

Overview

The increasing complexity of modern computer systems makes the development of correct software and hardware very challenging. A successful approach to master this challenge is formal verification which proves that the implementation of a system fulfills its specification or which shows that the implementation is buggy. Many verification approaches use automatic reasoning techniques and decision procedures of various logical formalisms as backends.

In this course, we will cover state-of-the-art topics on automated reasoning and decision procedures in the context of formal verification and their applications.

Organization

• This course will be blocked.
• Appointments will be fixed in accordance with the participants.
• There will be a lecture part providing the necessary background.
• Each participant has to select a topic on which a presentation has to be given at the end of the semester.
• The topic can either be based on the contents presented in the lectures of this course or on the course Advanced Model Checking.
• Meetings:
  • One day of lectures by Armin Biere and Martina Seidl on the background.
  • One or two meetings at the end of the semester in which each participant presents a selected topic.
  • Optional individual meetings for the preparation of the presentations.

The dates for presentations will still need to be fixed.

A list of preliminary topics can be found here.

Course Material

The slides set of the first blocked lecture day is available as dklogicskv.pdf.

Contact

For questions, contact Martina Seidl or Armin Biere.