Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, Proceedings

by Chris Hawblitzel (Editor)

Scalable Formal Machine Models.- Mechanized Semantics for Compiler Verification.- Automation in Computer-Aided Proofs, Attacks and Designs.- Program Certification by Higher-Order Model Checking.- A Formally-Verified Alias Analysis.- Mechanized Verification of Computing Dominators for Formalizing Compilers.- On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor.- An Executable Semantics for CompCert C.- Producing Certified Functional Code from Inductive Specifications.- The New Quickcheck for Random, Exhaustive and Symbolic Testing under One Roof.- Proving Concurrent Noninterference.- Noninterference for Operating System Kernels.- Compositional Verification of a Baby Virtual Memory Manager.- Shall We Juggle, Coinductively?.- Proof Abella Formalization of λ-Calculus Cube Property.- A String of Proofs of Fermat's Little Theorem.- Compact Proof Certificates for Linear Logic.- Constructive Completeness for Modal Logic with Transitive Closure.- Rating Disambiguation Errors.- A Formal Proof of Square Root and Division Elimination in Embedded Programs.- Coherent and Strongly Discrete Rings in Type Theory.- Improving Real Analysis in A User-Friendly Approach to Integrals and Derivatives.

316 pages, Paperback

First published November 22, 2012