Accession Number:



Verified compilation of Concurrent Managed Languages

Personal Author(s):

Corporate Author:

Purdue University West Lafayette United States

Report Date:



The goal of the Havoc project was to explore new proof techniques and methodologies that would enable scalable and modular verification of modern concurrent programming languages like Java or C . The efforts undertaken during the lifetime of this effort focused on a new proof techniques, specifically the use of refinement methods and tactics to simplify reasoning about interferences in proving invariants about concurrent code b incorporating precise notions of memory models, both at the processor and language level, to enable compilation to exploit and be faithful to language definitions and processor features c new designs for compiler intermediate representations that facilitate mechanized proofs and verification and d a realistic case study that combines these ideas to prove the correctness of a state-of-the-art concurrent garbage collector.

Descriptive Note:

Technical Report,01 Jul 2013,31 Jul 2017



Subject Categories:

Communities Of Interest:

Modernization Areas:

Distribution Statement:

Approved For Public Release;

Contract Number:


File Size: