Accession Number:

AD1043395

Title:

Verified compilation of Concurrent Managed Languages

Descriptive Note:

Technical Report,01 Jul 2013,31 Jul 2017

Corporate Author:

Purdue University West Lafayette United States

Personal Author(s):

Report Date:

2017-11-01

Pagination or Media Count:

36.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE