Marvin Brieger

Overview of my Research (Poster [pdf])

Problem Statement: Concurrency is an ubiquitous phenomenon in real-world cyber-physical systems (CPSs). Still logical methods for the analysis of CPSs lack support for modeling and verifying parallelism. This misalignment leaves only the error-prone rephrasing of natural parallelism into monolithic/sequential models. Moreover, it obstructs compositional verification along the parallel subcomponents, which is the key to the large-scale verification of concurrent CPSs.

Mission: To overcome the shortcomings described above, I study extensions of differential dynamic logic (dL) to concurrency. The dynamic logic of communicating hybrid programs (dL_CHP) enables modeling and verification of distributed CPSs. This system class captures wide-ranging applications, e.g. in autonomous driving and robot collision avoidance.

Increase the Trust: Although formal verification is considered the royal approach to safety (especially for CPSs), the correctness of many formal methods itself is based on a shaky foundation. Therefore, dL_CHP has a proof calculus based on uniform substitution. The uniform substitution approach enables a close alignment of theorem prover implementations and their logic, as well as, the implementation by means of a microkernel. This increases the trust one can put into the verification results significantly compared to results obtained from tools based on tens of thousands of lines of soundness-critical implementation.