This is the course website for the course on Software Verification offered in the winter semester of 2025 at RPTU Kaiserslautern, taught by Prof. Rupak Majumdar.

About the Course

Software Verification is an advanced seminar covering the algorithmic foundations for reasoning about code. This year, we will put particular emphasis on computational aspects for large-scale search and the use of LLMs in facilitating search. Along the way, we will also study algorithms and heuristics that reason about code with some support from the user. By taking this course, you will learn the basics of managing large-scale search that appears in automated reasoning about (concurrent and distributed) software systems.

Grading

Grading will be based on an oral final exam. In order to appear for the exam, you are expected to finish all readings and solve and hand in assignments. There are no strict deadlines for the assignments and readings; just send them over by the end of the semester. Students are nonetheless recommended to read them shortly after they are introduced in the course.

You are welcome to collaborate with others on the assignments. However, each student is expected to write down their solution independently, and to mention collaborators. The use of LLMs is permitted and sometimes required for some assignments.

Announcements

See Calendar for readings and announcements.