Verification of Programs and Systems
Vienna University of Technology, 2013S-now, 184.741
with Helmut Veith(†) and Josef Widder
This undergraduate course provides an introduction to verification techniques such as assertions, testing, test-case generation, model checking, and Hoare Logic. There is a strong focus on the application of verification tools.
Computer Aided Verification
Vienna University of Technology, 2016S, 181.145
with Igor Konnov
This graduate course provides an introduction to model checking, temporal logic, abstraction techniques and interpolation-based verification.
Formal Methods in Computer Science
Vienna University of Technology, 2016S, 185.291
with Gernot Salzer, Uwe Egly, Stefan Woltran, Igor Konnov, Florian Lonsing, Thomas Pani, Mantas Simkus, and Florian Zuleger
This graduate course provides an introduction formal methods in computer science, including specifications and temporal logic.
Seminar on Formal Methods
Vienna University of Technology, 2012W-now, 184.221
Research seminar for graduate students, covering seminal papers on automated verification and recent advances in the field.
Semantics of Programming Languages
Vienna University of Technology, 2013S-now, 184.749.
with Florian Zuleger and Agata Ciabattoni
An advanced course on the semantics of programming languages, including operational, denotational, and axiomatic semantics.
Automated Software Verification: Software Model Checking
Vienna University of Technology, 2013S-now, 184.747
Princeton University, Spring 2011, ELE/COS 580 (course website)
This course covers contemporary automated verification techniques for software. The focus is on the underlying techniques and algorithms rather than on using verification tools. The course is divided into two main parts: One covering model checking for finite state models (e.g., manual abstractions or UML state-charts), and a second part that shows how these techniques can be applied to infinite state programs by means of abstraction.