University of Freiburg
building 052, room 00-020
Decision Procedures, Model Checking
I am working on Verification of Software and Real-Time Systems via model-checking and Automated theorem proving. My current work include: Teaching, abstraction techniques and the design of the Hybrid Model Checker SASET.
- Quasi-Dependent Variables in Hybrid Automata in
- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification in
- Detecting Quasi-equal Clocks in Timed Automata in , together with Bernd Westphal and Andreas Podelski.
- Timed Automata with Disjoint Activity in , together with Bernd Westphal and Andreas Podelski.
- Reducing Quasi-Equal Clocks in Networks of Timed Automata in , together with Christian Herrera, Sergio Feo, Bernd Westphal and Andreas Podelski.
- Deciding Functional Lists with Sublists Sets in , together with Thomas Wies and Viktor Kuncak.
- An efficient decision procedure for imperative tree data structures in , together with Thomas Wies and Viktor Kuncak.
- Decision Procedures for List Manipulating Programs, Master thesis, University of Freiburg, 2009
- Designing and implementing in Ocaml the hybrid model checker SASET.
- Modeling using the UPPAAL model checker.
- Working with the Jahob Verification System for reasoning about reachability in Trees and Lists.
- Lecturing Model Checking at the San Pablo University in Peru.
- Lecturing Theory I SS12.
- Co-organizing the Model Checking SS11 lecture together with Sergiy Bogomolov.
- Organizing the
Algorithms Theory WS10-11 lecture.
- Organizing the
Theory I SS10 lecture.
- Co-organizing the
Algorithms Theory WS09-10 lecture
- Tutorial for the lecture Software Design, Modelling and Analysis in UML.
I am also
- Microsoft Certified Solution Developer
- Systems Engineer