Photo of Georg
About me
Georg Weissenbacher
DPhil (Oxon)
associate professor

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.