LEADER 04707nam 22008535 450 001 996466275603316 005 20230329190404.0 010 $a3-642-35308-8 024 7 $a10.1007/978-3-642-35308-6 035 $a(CKB)3400000000102898 035 $a(SSID)ssj0000810186 035 $a(PQKBManifestationID)11524391 035 $a(PQKBTitleCode)TC0000810186 035 $a(PQKBWorkID)10828234 035 $a(PQKB)11693792 035 $a(DE-He213)978-3-642-35308-6 035 $a(MiAaPQ)EBC6307351 035 $a(MiAaPQ)EBC5585123 035 $a(Au-PeEL)EBL5585123 035 $a(OCoLC)819661495 035 $a(PPN)168328410 035 $a(EXLCZ)993400000000102898 100 $a20121116d2012 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aCertified Programs and Proofs$b[electronic resource] $eSecond International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, Proceedings /$fedited by Chris Hawblitzel, Dale Miller 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (X, 305 p. 64 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7679 300 $aInternational conference proceedings. 311 $a3-642-35307-X 320 $aIncludes bibliographical references and author index. 327 $aScalable 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. 330 $aThis book constitutes the refereed proceedings of the Second International Conference on Certified Programs and Proofs, CPP 2012, held in Kyoto, Japan, in December 2012. The 18 revised regular papers presented were carefully reviewed and selected from 37 submissions. They deal with those topics in computer science and mathematics in which certification via formal techniques is crucial. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7679 606 $aComputer science 606 $aMachine theory 606 $aCompilers (Computer programs) 606 $aComputer science?Mathematics 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aFormal Languages and Automata Theory 606 $aCompilers and Interpreters 606 $aSymbolic and Algebraic Manipulation 606 $aSoftware Engineering 606 $aArtificial Intelligence 615 0$aComputer science. 615 0$aMachine theory. 615 0$aCompilers (Computer programs). 615 0$aComputer science?Mathematics. 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aFormal Languages and Automata Theory. 615 24$aCompilers and Interpreters. 615 24$aSymbolic and Algebraic Manipulation. 615 24$aSoftware Engineering. 615 24$aArtificial Intelligence. 676 $a004.01/51 702 $aHawblitzel$b Chris$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aMiller$b Dale$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aCPP 2012 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996466275603316 996 $aCertified Programs and Proofs$92557693 997 $aUNISA