CPP 2012: Program

Program

9:10-10:10	APLAS/CPP Invited Talk: Greg Morrisett. Scalable Formal Machine Models (Chair: Zhong Shao)
10:10-14:00	APLAS Day 3
14:00-15:00	APLAS/CPP Invited Talk: Xavier Leroy. Mechanized Semantics for Compiler Verification (Chair: Jacques Garrigue)
15:00-15:30	Break
15:30-17:00	CPP 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:00	APLAS/CPP Banquet

9:10-10:10	CPP Invited Talk: Gilles Barthe. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs (Chair: Gerwin Klein)
10:10-10:40	Break
10:40-12:10	CPP 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
12:10-14:00	Lunch
14:00-15:30	CPP 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
15:30-16:00	Break
16:00-17:30	CPP 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

9:10-10:10	CPP Invited Talk: Naoki Kobayashi. Program Certiﬁcation by Higher-Order Model Checking (Chair: Georges Gonthier)
10:10-10:40	Break
10:40-12:10	CPP 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
12:10-14:00	Lunch
14:00-15:30	CPP 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