Decision Procedures for Verification and Synthesis

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.

 

Presentations: A key objective of the proseminar is for students to learn how to give a scientific presentation. Each student will give two presentations on the topic that they have been assigned (based on provided references that will be research papers or book chapters). 
* The first presentation is for practice (and is not graded), and after it the fellow students and the instructor will provide feedback on the quality of the presentation and suggestions about what can be improved. 
* The second presentation (which will be graded) will be on the same or a closely related topic but based on a different reference. 

Feedback: All students are expected to participate actively in the discussions, and will be required to provide feedback for each of the practice presentations.

Summary: At the end of the semester each student will submit a short summary of the topic that they have presented.

 

Logistics

Time: Tuesday, 8:15-9:45

Venue: All meetings will be virtual, via Zoom (Disclaimer).

             The link to the recurring meeting will be communicated by email.

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

 

Important dates

20 April, 8:15 Kick-off meeting (participation is strictly required)

 

Instructor

Rayna Dimitrova (dimitrova@cispa.de)