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.
Logistics
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)
Instructor
Rayna Dimitrova (dimitrova@cispa.de)