Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Verified LLVM Infrastructure

PIs: Martin (Penn) and Zdancewic (Penn)

We have developed Vellvm (verified LLVM), a framework for reasoning about programs expressed in the open-source LLVM intermediate compiler representation and program transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves simulation relations among them to facilitate different reasoning styles and proof techniques.

Vellvm supports the activities of the ExCAPE project in two ways. First, it provides a foundational way of connecting the semantics of programs synthesized by high-level tools to their low-level implementations. As such, it offers the possibility of verifying the correctness of synthesized software with respect to a realistic low- level computation model Vellvm can serve as a bridge between formal methods and main-stream compiler technology. Second, the Vellvm project itself draws on traditional correctness by construction techniques: verified Vellvm program transformations can be extracted directly from their proofs of correctness as expressed in Coq. This is itself a form of program synthesis, which is complementary to other approaches being explored in the ExCAPE research [ZNMZ13].



Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996