Accepted Papers

Lukas Bulwahn. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing Under One Roof
Andrea Asperti and Wilmer Ricciotti. Rating Disambiguation Errors
Hing-Lun Chan and Michael Norrish. A String of Pearls: Proofs of Fermat's Little Theorem
Pierre Neron. A Formal Proof of Square Root and Division Elimination in Embedded Programs
Andrei Popescu, Johannes Hölzl and Tobias Nipkow. Proving concurrent noninterference
Jianzhou Zhao and Steve Zdancewic. Mechanized Verification of Computing Dominators for Formalizing Compilers
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein. Noninterference for Operating System Kernels
Keisuke Nakano. Shall We Juggle, Coinductively?
Dominic Mulligan and Claudio Sacerdoti Coen. On the correctness of an optimising assembler for the MCS-51 microcontroller
Valentin Robert and Xavier Leroy. A formally-verified alias analysis
Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
Brian Campbell. An Executable Semantics for CompCert C
Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic
Christian Doczkal and Gert Smolka. Constructive Completeness for Modal Logic with Transitive Closure
Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property
Pierre-Nicolas Tollitte, David Delahaye and Catherine Dubois. Producing Certified Functional Code from Inductive Specifications
Alexander Vaynberg and Zhong Shao. Compositional Verification of a Baby Virtual Memory Manager
Anders Mörtberg, Thierry Coquand and Vincent Siles. Coherent and Strongly Discrete Rings in Type Theory
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