Abstract

file

Visible to the public Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11

Presented as part of the 2015 HCSS conference.

Abstract:

C remains central to our computing infrastructure but still lacks a clear and complete semantics. Programmers lack tools to explore the range of behaviours they should expect; compiler development lacks test oracles; and formal verification and analysis must make (explicitly or implicitly) many choices about the specific C they target.