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