CPP 2012

22 papers

1. A Formal Proof of Square Root and Division Elimination in Embedded Programs · Pierre Neron
2. A Formally-Verified Alias Analysis · Valentin Robert, Xavier Leroy
3. A String of Pearls: Proofs of Fermat's Little Theorem · Hing-Lun Chan, Michael Norrish
4. An Executable Semantics for CompCert C · Brian Campbell
5. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs · Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
6. Coherent and Strongly Discrete Rings in Type Theory · Thierry Coquand, Anders Mörtberg, Vincent Siles
7. Compact Proof Certificates for Linear Logic · Kaustuv Chaudhuri
8. Compositional Verification of a Baby Virtual Memory Manager · Alexander Vaynberg, Zhong Shao
9. Constructive Completeness for Modal Logic with Transitive Closure · Christian Doczkal, Gert Smolka
10. Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives · Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
11. Mechanized Semantics for Compiler Verification · Xavier Leroy
12. Mechanized Verification of Computing Dominators for Formalizing Compilers · Jianzhou Zhao, Steve Zdancewic
13. Noninterference for Operating System Kernels · Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
14. On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor · Dominic P. Mulligan, Claudio Sacerdoti Coen
15. Producing Certified Functional Code from Inductive Specifications · Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois
16. Program Certification by Higher-Order Model Checking · Naoki Kobayashi
17. Proof Pearl: Abella Formalization of λ-Calculus Cube Property · Beniamino Accattoli
18. Proving Concurrent Noninterference · Andrei Popescu, Johannes Hölzl, Tobias Nipkow
19. Rating Disambiguation Errors · Andrea Asperti, Wilmer Ricciotti
20. Scalable Formal Machine Models · Greg Morrisett
21. Shall We Juggle, Coinductively? · Keisuke Nakano
22. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof · Lukas Bulwahn