Verified compilation of Concurrent Managed Languages
Technical Report,01 Jul 2013,31 Jul 2017
Purdue University West Lafayette United States
Pagination or Media Count:
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.
- Computer Programming and Software