Repository logo

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C

Published version

Change log


Lau, S 
Gomes, VBF 
Pichon-Pharabod, J 


C remains central to our infrastructure, making verification of C code an essential and much-researched topic, but the semantics of C is remarkably complex, and important aspects of it are still unsettled, leaving programmers and verification tool builders on shaky ground.

This paper describes a tool, Cerberus-BMC, that for the first time provides a principled reference semantics that simultaneously supports (1) a choice of concurrency memory model (including substantial fragments of the C11, RC11, and Linux kernel memory models), (2) a modern memory object model, and (3) a well-validated thread-local semantics for a large fragment of the language. The tool should be useful for C programmers, compiler writers, verification tool builders, and members of the C/C++ standards committees.



4613 Theory Of Computation, 46 Information and Computing Sciences, 4612 Software Engineering

Journal Title

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Conference Name

CAV 2019: Proc. 31st International Conference on Computer-Aided Verification

Journal ISSN


Volume Title

11561 LNCS


Springer International Publishing
Engineering and Physical Sciences Research Council (EP/K008528/1)
European Research Council (789108)