Marvin Brieger

Overview of my Research (Poster [pdf])

Problem Statement: Parallelism is an ubiquitous phenomenon in real-world cyber-physical systems (CPSs), e.g. multiple aircrafts, trains, or cars sharing the same space. 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.