PDF version

Tuesday (11 December 2012): APLAS Day 1

Wednesday (12 December 2012): APLAS Day 2

Thursday (13 December 2012)

9:10-10:10APLAS/CPP Invited Talk: Greg Morrisett. Scalable Formal Machine Models (Chair: Zhong Shao)
10:10-14:00APLAS Day 3
14:00-15:00APLAS/CPP Invited Talk: Xavier Leroy. Mechanized Semantics for Compiler Verification (Chair: Jacques Garrigue)
15:30-17:00CPP Session 1: Certified Compilation (Chair: Chris Hawblitzel)
Valentin Robert and Xavier Leroy. A formally-verified alias analysis
Jianzhou Zhao and Steve Zdancewic. Mechanized Verification of Computing Dominators for Formalizing Compilers
Dominic Mulligan and Claudio Sacerdoti Coen. On the correctness of an optimising assembler for the MCS-51 microcontroller
19:00APLAS/CPP Banquet

Friday (14 December 2012)

9:10-10:10CPP Invited Talk: Gilles Barthe. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs (Chair: Gerwin Klein)
10:40-12:10CPP Session 2: Execution and Testing (Chair: Gerwin Klein)
Brian Campbell. An Executable Semantics for CompCert C
Pierre-Nicolas Tollitte, David Delahaye and Catherine Dubois. Producing Certified Functional Code from Inductive Specifications
Lukas Bulwahn. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing Under One Roof
14:00-15:30CPP Session 3: Operating Systems and Security (Chair: Chris Hawblitzel)
Andrei Popescu, Johannes Hölzl and Tobias Nipkow. Proving concurrent noninterference
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein. Noninterference for Operating System Kernels
Alexander Vaynberg and Zhong Shao. Compositional Verification of a Baby Virtual Memory Manager
16:00-17:30CPP Session 4: Elegant Proofs (Chair: Zhong Shao)
Keisuke Nakano. Shall We Juggle, Coinductively?
Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property
Hing-Lun Chan and Michael Norrish. A String of Pearls: Proofs of Fermat's Little Theorem

Saturday (15 December 2012)

9:10-10:10CPP Invited Talk: Naoki Kobayashi. Program Certification by Higher-Order Model Checking (Chair: Georges Gonthier)
10:40-12:10CPP Session 5: Logic and Types (Chair: Dale Miller)
Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic
Christian Doczkal and Gert Smolka. Constructive Completeness for Modal Logic with Transitive Closure
Andrea Asperti and Wilmer Ricciotti. Rating Disambiguation Errors
14:00-15:30CPP Session 6: Mathematics (Chair: Georges Gonthier)
Pierre Neron. A Formal Proof of Square Root and Division Elimination in Embedded Programs
Anders Mörtberg, Thierry Coquand and Vincent Siles. Coherent and Strongly Discrete Rings in Type Theory
Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
CPP 2012
The Second International Conference on Certified Programs and Proofs
Home Call For Papers Organizers Important Dates Invited Speakers Submit Paper Accepted Papers Program Local Information