Proof Engineering (HCSS'15)

file

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

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.

file

Visible to the public Qualification of Formal Methods Tools

Abstract:

Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems such as avionics systems. The recent release of DO-178C and the accompanying Formal Methods supplement DO-333 will make it easier for developers of software for commercial aircraft to obtain certification credit for the use of formal methods.

file

Visible to the public CodeHawk: Sound Static Analysis for Proving the Absence of Memory Related Software Vulnerabilities

Abstract:

Most software vulnerabilities are due to coding errors. Testing is commonly the main means for detecting vulnerabilities, but testing alone only explores a small fraction of the possible behaviors of software. Sound static analysis is a technology that can examine source code and reason about all of its behaviors in order to detect coding errors that lead to vulnerabilities.