Decision procedures for logical theories (these are algorithms that for a certain type of logical formulas provide an answer to the question whether a given formula can be satisfied or not) are the backbone of state-of-the-art methods and tools for software and hardware verification, program synthesis, automatic bug finding, and compiler optimization. In this proseminar we will study decision procedures for different logical theories that are commonly used in the context of program verification and synthesis, and how they are applied to the design, analysis, and construction of software.



Time: TBA

Venue: TBA

Attendance: Participation in all meetings is mandatory (exceptions require an official document, i.e., doctor's certificate).


Important dates

TBA Kick-off meeting (participation is strictly required)



Rayna Dimitrova (




Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.