CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Tue 19 Jan 2016 16:30 - 17:00 at Room St Petersburg II - Session 8: Compiler Verification

Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic low-level language with linear sequential composition and lexically scoped gotos defined with a small-step semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
Formal Verification of Control-flow Graph Flattening
Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
Axiomatic Semantics for Compiler Verification
Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University