SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Fri 24 Oct 2014 10:52 - 11:15 at Salon E - Specification and Verification Chair(s): Gary Leavens

Many real programs are written in multiple different programming languages, and supporting this pattern creates challenges for formal compiler verification. We describe our Coq verification of a compiler for a high-level language, such that the compiler correctness theorem allows us to derive partial-correctness Hoare-logic theorems for programs built by linking the assembly code output by our compiler and assembly code produced by other means. Our compiler supports such tricky features as storable cross-language function pointers, without giving up the usual benefits of being able to verify different compiler phases (including, in our case, two classic optimizations) independently. The key technical innovation is a mixed operational and axiomatic semantics for the source language, with a built-in notion of abstract data types, such that compiled code interfaces with other languages only through axiomatically specified methods that mutate encapsulated private data, represented in whatever formats are most natural for those languages.

Fri 24 Oct
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:00: Specification and VerificationOOPSLA at Salon E
Chair(s): Gary Leavens University of Central Florida
10:30 - 10:52
Talk
Bounded Exhaustive Test Input Generation from Hybrid Invariants
OOPSLA
Nico RosnerDept. of Computer Science FCEyN, University of Buenos Aires, Valeria BengoleaDept. of Computer Science FCEFQyN, University of Rio Cuarto, Pablo PonzioDept. of Computer Science FCEFQyN, University of Rio Cuarto, Shadi Abdul KhalekGoogle, Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. of Software Engineering Instituto Tecnológico de Buenos Aires, Sarfraz KhurshidUniversity of Texas at Austin
Link to publication
10:52 - 11:15
Talk
Compiler Verification Meets Cross-Language Linking via Data Abstraction
OOPSLA
Link to publication
11:15 - 11:37
Talk
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
OOPSLA
Aaron TuronMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS
Link to publication
11:37 - 12:00
Talk
Natural Proofs for Asynchronous Programs using Almost-Synchronous Invariants
OOPSLA
Ankush DesaiUniversity of California, Berkeley, Pranav GargUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign
Link to publication