Proof Engineering (HCSS'15)

file

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

Submitted by Katie Dey on Thu, 04/23/2015 - 6:36pm. Contributors:

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.