About

I am an Associate 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.

Research Interests

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.

Publications

Conferences

• Stubborn Set Reduction for Timed Reachability and Safety Games. In FORMATS 2021. [.bib]
• An Integer Static Analysis for Better Extrapolation in Uppaal. In FORMATS 2021. [.bib]
• Fluid Model-Checking in UPPAAL for Covid-19. In ISoLA 2020. [.bib]
• 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]

Journals

• An investigation of safe and near-optimal strategies for prevention of Covid-19 exposure using stochastic hybrid models and machine learning. At Decision Analytics Journal [.bib]
• Online and Proactive Vehicle Rerouting with Uppaal Stratego. At Transportation Research Record [.pdf]
• Stubborn set reduction for two-player reachability games. Logical Methods in Computer Science
• Ready for testing: ensuring conformance to industrial standards through formal verification. In Formal Aspects of Computing [.pdf]

Technical Reports

• Energy Consumption Optimization in Radio Access Networks (ECO-RAN) [.pdf] [.bib]
• Near Optimal Task Graph Scheduling with Priced Timed Automata and Priced Timed Markov Decision Processes. [.pdf] [.bib]

Thesis

• Model Checking for Time Division Multiple Access Systems [.pdf]
• Decision Procedures for List Manipulating Programs[.pdf]

Current and Past Projects

• Member of the expert modeling group for COVID-19 at Statens Serum Institut SSI
• 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

Teaching

• Lecturing Models and Tools for Cyber-Physical Systems, Aalborg University.
• 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.

Misc

• Microsoft Certified Solution Developer
• Systems Engineer