I am an Assistant Professor at the group of Prof. Dr. Kim G Larsen at the DEIS unit at the Department of Computer Science at Aalborg University. I received my doctorate in Computer Science from the University of Freiburg. My supervisors were Prof. Dr. Andreas Podelski together with Dr. Bernd Westphal.
My research focuses on formal verification and strategy synthesis for stochastic hybrid games. Previously I have worked on software verification via model checking and automated theorem proving.
- Urgent Partial Order Reduction for Extended Timed Automata. In ATVA'20. [.pdf] [.bib]
- On-the-Fly Synthesis for Strictly Alternating GamesPartial Order Reduction for Reachability Games. In PetriNets'20. [.pdf] [.bib]
- Partial Order Reduction for Reachability Games. In CONCUR'19. [.pdf] [.bib]
- Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In CAV'18. [.pdf]
- Analyzing spreadsheets for parallel execution via model checking. In Essays on the Occasion of Bernhard Steffen's 60th Birthday. [.pdf] [.bib]
- A Delay-Robust Touristic Plan Recommendation Using Real-World Public Transportation Information. In RecTour 2017. [.pdf]
- Uppaal Stratego for Intelligent Traffic Lights. In ITS Europe 2017. [.pdf] [.bib]
- Toolchain for user-centered intelligent floor heating control. In IECON16. [.pdf]
- Online and Compositional Learning of Controllers with Application to Floor Heating. In TACAS16 [.pdf]
- Quasi-Dependent Variables in Hybrid Automata. In HSCC14 [.pdf]
- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification. In FM2014 [.pdf]
- Detecting Quasi-equal Clocks in Timed Automata. In FORMATS 2013 [.pdf]
- Timed Automata with Disjoint Activity. In FORMATS 2012 [.pdf]
- Reducing Quasi-Equal Clocks in Networks of Timed Automata. In FORMATS 2012 [.pdf]
- Deciding Functional Lists with Sublists Sets. In VSTTE 2012 [.pdf]
- An Efficient Decision Procedure for Imperative Tree Data Structures. In CADE 2011 [.pdf]
- Ready for testing: ensuring conformance to industrial standards through formal verification. In Formal Aspects of Computing [.pdf]
- Near Optimal Task Graph Scheduling with Priced Timed Automata and Priced Timed Markov Decision Processes. [.pdf] [.bib]
- Model Checking for Time Division Multiple Access Systems [.pdf]
- Decision Procedures for List Manipulating Programs[.pdf]
Current and Past Projects
- BEO-COVID project from Poul Due Jensen Foundation. Beo-Covid
- Energy Consumption Optimization in Radio Access Networks ECO-RAN
- Danish Center for Data-Intensive Cyber-Physical Systems DiCyPS
- Danish project, Popular Parallel Programming P3
- European reaserach project CASSTING
- German trans-regional research project for Automatic Verification And Analysis of Complex Systems AVACS
- German project ZIM for ensuring conformance to industrial standards through formal verification
- Numerous PBL group supervisions at Aalborg University
- Master thesis supervisions San Pablo University in Peru.
- Lecturing Model Checking SS14 at the San Pablo University in Peru.
- Lecturing Computer Science Theory I SS12. Uni Freiburg.
- Co-organizing the Model Checking SS11 lecture together with Sergiy Bogomolov. Uni Freiburg.
- Organizing the Algorithms Theory WS10-11 lecture. Uni-Freiburg.
- Organizing the Theory I SS10 lecture. Uni Freiburg
- Co-organizing the Algorithms Theory WS09-10 lecture together with Phillip Heidegger. Uni Freiburg
- Tutorial for the lecture Software Design, Modelling and Analysis in UML. Uni Freiburg
Tools Working in/with
- Verification of Petri Nets and extensions with TAPAAL
- Modelling with: UPPAAL, UPPAAL TIGA, and UPPAAL STRATEGO.
- Simulations with Matlab and Simulink.
- Designing and implementing the hybrid model checker SASET.
- Java program verification with the Jahob System, for reasoning about reachability in trees and lists.
MiscI am also
- Microsoft Certified Solution Developer
- Systems Engineer