Stefan Schupp

Stefan Schupp

Formal Verification Engineer

Apple

Professional Summary

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.

Education

PhD Computer Science

RWTH Aachen University

MS Computer Science

RWTH Aachen University

BS Computer Science

RWTH Aachen University

Interests

Formal verification Modeling and analysis of hybrid systems Reachability analysis Flowpipe construction SMT solving
About me

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.

Featured Publications

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.

avatar
Stefan Schupp
Read more