![]() |
Ph.D. Stanford University, 1991
Dr.h.c. Fourier University, Grenoble, 2012; Masaryk University, Brno, 2015 |
President IST Austria (Institute of Science and Technology Austria) Biographical sketch Curriculum vitae Research group |
|
Coordinates |
Mail: Am Campus 1, A-3400 Klosterneuburg Email: my_three_initials@ist.ac.at Assistant: Magdalena.Lueger-Kaltenecker@ist.ac.at Phone: +43 2243 9000 1033 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 Guide2Research |
Current students |
Bernhard Kragl
Mathias Lechner |
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 |
Communities |
ARiSE
(Austrian Rigorous Systems Engineering)
ARTIST (European Network of Excellence on Embedded Systems Design) |
Funding |
ERC
(European Research Council)
FWF (Austrian Science Fund) |
Last updated in November 2019.