Auditorium (Building IMAG)
25 June 2019 - 14h00
BMC with Weak Memory Models
by Hernan Ponce de Leon from Fortiss, Munich, Germany
Abstract: In this talk I'll report progress in verification tool engineering for
weak memory models. I will present Dartagnan, a bounded model checking
tools for concurrent programs. Its distinguishing feature is the memory
model as part of the input. Dartagnan reads CAT, the standard language
for memory models which allows to define x86/TSO, ARMv7, ARMv8, Power,
C/C++, and Linux kernel concurrency primitives. A BMC with memory models
as input presents a challenge. One has to encode not only the program
but also its semantics as defined by the memory model. I'll present some
of the challenges and solutions that make Dartagnan scale. We have
performed experiments to compare our tools against other memory model-
aware verifiers and find them very competitive, despite the modularity
offered by our approach.
