TY  - BOOK
AU  - Hawblitzel,Chris
AU  - Miller,Dale
TI  - Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings 
SN  - 9783642353086
PY  - 2012///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Software engineering
KW  - Programming languages (Electronic computers)
KW  - Computer logic
KW  - Mathematical logic
KW  - Mathematics
KW  - Artificial intelligence
N1  - Scalable Formal Machine Models -- Mechanized Semantics for Compiler Verification -- Automation in Computer-Aided Cryptography: 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 Isabelle: 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 Pearl: Abella Formalization of λ-Calculus Cube Property -- A String of Pearls: 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 Coq: A User-Friendly Approach to Integrals and Derivatives
UR  - http://dx.doi.org/10.1007/978-3-642-35308-6
ER  -