Ph.D. Stanford University, 1991
Dr.h.c. Fourier University, Grenoble, 2012; Masaryk University, Brno, 2015
IST Austria (Institute of Science and Technology Austria)

Biographical sketch
Curriculum vitae

Research group
Coordinates Mail: Am Campus 1, A-3400 Klosterneuburg
Phone: +43 2243 9000 1007
Fax (not private): +43 2243 9000 2000
Research Blast: Model checking of software
Chic: Interface-based design
Computational modeling in biology
Games for verification and control
Giotto: Embedded software design
HyTech: Verification of hybrid automata
Liveness of reactive systems
Mocha: Assume-guarantee model checking
Real Time: Logics and automata
Symbolic algorithms for system analysis
Transactional memories
Open positions If you are interested in pursuing a doctoral degree or postdoc in one of these areas, please contact us.
Lectures Reliable Systems Engineering (Inaugural Lecture, EPFL, December 2006)
Publications By year
By topic
By venue: conferences; journals
Bibtex entries

DBLP database
Google Scholar
Current students Konstantin Kueffner
Mathias Lechner
N. Ege Sarac
Former students Pei-Hsin Ho (Ph.D. Cornell, 1995): Automatic Analysis of Hybrid Systems
Peter W. Kopke (Ph.D. Cornell, 1996): The Theory of Rectangular Hybrid Automata
Sriram K. Rajamani (Ph.D. UC Berkeley, 1999): New Directions in Refinement Checking
Shaz Qadeer (Ph.D. UC Berkeley, 1999): Methodology for Scalable Model Checking
Freddy Y.C. Mang (Ph.D. UC Berkeley, 2002): Games in Open Systems Verification and Synthesis
Benjamin Horowitz (Ph.D. UC Berkeley, 2003): Giotto: A Time-triggered Language for Embedded Programming
Rupak Majumdar (Ph.D. UC Berkeley, 2003): Symbolic Algorithms for Verification and Control
Ranjit Jhala (Ph.D. UC Berkeley, 2004): Program Verification by Lazy Abstraction
Arindam Chakrabarti (Ph.D. UC Berkeley, 2007): A Framework for Compositional Design and Analysis of Systems
Krishnendu Chatterjee (Ph.D. UC Berkeley, 2007): Stochastic Omega-Regular Games
Arkadeb Ghosal (Ph.D. UC Berkeley, 2008): A Hierarchical Coordination Language for Reliable Real-Time Tasks
Slobodan Matic (Ph.D. UC Berkeley, 2008): Compositionality in Deterministic Real-Time Embedded Systems
Vinayak S. Prabhu (Ph.D. UC Berkeley, 2008): Games for the Verification of Timed Systems
Vasu Singh (Ph.D. EPFL, 2009): Formalizing and Verifying Transactional Memories
Gregory Theoduloz (Ph.D. EPFL, 2010): Software Verification by Combining Program Analyses of Adjustable Precision
Maria Mateescu (Ph.D. EPFL, 2011): Propagation Models for Biochemical Reaction Networks
Damien Zufferey (Ph.D. IST Austria, 2013): Analysis of Dynamic Message-Passing Programs
Arjun Radhakrishna (Ph.D. IST Austria, 2014): Quantitative Specifications for Verification and Synthesis
Thorsten Tarrach (Ph.D. IST Austria, 2016): Automatic Synthesis of Synchronization Primitives for Concurrent Programs
Przemek Daca (Ph.D. IST Austria, 2017): Statistical and Logical Methods for Property Checking
Mirco Giacobbe (Ph.D. IST Austria, 2019): Automatic Time-Unbounded Reachability Analysis of Hybrid Systems
Bernhard Kragl (Ph.D. IST Austria, 2020): Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization
Communities ARiSE (Austrian Rigorous Systems Engineering)
ARTIST (European Network of Excellence on Embedded Systems Design)
ViSP (Vienna Security and Privacy Center)
Funding ERC (European Research Council)
FWF (Austrian Science Fund)

Last updated in September 2021.