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

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)