Roland Meyer

(TU Braunschweig)
hosted by seminar series Certified Verification with Applications

"BMC with Memory Models as Input"

Dartagnan is a bounded model checker for concurrent programs under weak memory models that we develop in collaboration with Thomas Haas and Hernan Ponce de León. Its distinguishing feature is that the memory model is not hardcoded inside the tool but taken as part of the input. The input format is CAT, the by now standard language for memory models, which has been used to formalize x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives.

Bio: BMC with memory models as input is challenging, because one has to encode into SMT not only the program but also its semantics as defined by the memory model. The talk will focus on the tricks we developed to keep this encoding compact.Roland Meyer is a professor at TU Braunschweig and head of the Institute of Theoretical Computer Science. From 2010 to 2016, he was an assistant and associate professor at TU Kaiserslautern. Roland is interested in verification and synthesis problems for concurrent programs and tends to approach these problems from a theoretical angle, using techniques from automata theory, complexity, and semantics.

Time:	Thursday, 03.02.2022, 13:00
Place:	https://uni-kl-de.zoom.us/j/92435504190?pwd=REpNVnQ2SUs3NkFmemZRZ1BrYVV2QT09

Termin als Datei downloaden und in den Kalender importieren.