State Set Representations and Their Usage in the Reachability Analysis of Hybrid Systems
This work presents results obtained in the field of safety verification for linear hybrid systems via flow pipe construction-based reachability analysis.
Strong interest in formal verification across the board, be it pushing boundaries for hybrid or stochastic hybrid systems, investigating & applying techniques for hardware verification or discussing and learning about further directions, techniques and fields were formal verification shines.
PhD Computer Science
RWTH Aachen University
MS Computer Science
RWTH Aachen University
BS Computer Science
RWTH Aachen University
My main interest is centered around formal methods, formal verification, and applications thereof. Early contact with SMT solvers and interval constraint propagation as a theory-solver during my master’s degree has pushed me toward theoretical computer science. The development of HyPro and the work on reachability analysis for linear hybrid systems during my Ph.D. equipped me with experience in both, tool/library design (c/c++/cmake/git/ci …) as well as the realization of theoretical concepts ready to be used by practitioners. Bringing formal methods to students as part of my teaching duties was another insightful experience that I enjoyed very much.
Later working together with the group at WWU opened up a perspective on uncertainty in hybrid systems that raises further requirements on analysis methods. During that time I also started to help organize the ARCH competition subgroup on stochastic hybrid models.
My work at TU Vienna opened up various new opportunities to learn and explore new fields such as IoT and GPU programming (during teaching) as well as simplex architectures (together with TU Graz) and statistical model checking of hyperproperties (together with University of Michigan, ongoing work).
I enjoy new challenges and the discourse and discussion on how to solve the induced problems. The time during my Ph.D. made me sensible of the beauty of algorithms and structured approaches in formal methods. My view for details allowed me to fine-tune those approaches and identify sub-classes of problems and specialize dedicated methods aiming at those sub-classes
While working at Apple I strive to extend my toolbox to further applications and approaches in formal verification to broaden my view and to open up for appplications of learnt techniques across fields.
This work presents results obtained in the field of safety verification for linear hybrid systems via flow pipe construction-based reachability analysis.