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 LEADER 02274nam 2200565 a 450 001 9910778622403321 005 20230421033211.0 010 $a0-309-17543-7 010 $a0-309-52284-6 010 $a0-585-02631-9 035 $a(CKB)110986584753438 035 $a(EBL)3375676 035 $a(SSID)ssj0000240529 035 $a(PQKBManifestationID)11220211 035 $a(PQKBTitleCode)TC0000240529 035 $a(PQKBWorkID)10266368 035 $a(PQKB)10742038 035 $a(MiAaPQ)EBC3375676 035 $a(Au-PeEL)EBL3375676 035 $a(CaPaEBR)ebr10041096 035 $a(OCoLC)923257980 035 $a(EXLCZ)99110986584753438 100 $a19961009d1997 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aSafe water from every tap$b[electronic resource] $eimproving water service to small communities /$fCommittee on Small Water Supply Systems, Water Science and Technology Board, Commission on Geosciences, Environment, and Resources, National Research Council 210 $aWashington, D.C. $cNational Academy Press$d1997 215 $a1 online resource (230 p.) 300 $aDescription based upon print version of record. 311 $a0-309-05527-X 320 $aIncludes bibliographical references and index. 327 $a""Front Matter""; ""Preface""; ""Contents""; ""Executive Summary""; ""1 Small Water Supply Systems: An Unsolved Problem""; ""2 Status of Small Water Systems""; ""3 Technologies for the Small System""; ""4 Evaluating Technologies for Small Systems""; ""5 Ensuring Small Water Supply System Sustainability""; ""6 Training Operators for Small Systems""; ""Index"" 606 $aDrinking water$zUnited States 606 $aWater-supply engineering$zUnited States 606 $aMunicipal water supply$zUnited States 615 0$aDrinking water 615 0$aWater-supply engineering 615 0$aMunicipal water supply 676 $a363.6/1/0973 712 02$aNational Research Council (U.S.).$bCommittee on Small Water Supply Systems. 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910778622403321 996 $aSafe water from every tap$93788136 997 $aUNINA