LEADER 05019nam 22007575 450 001 996465748303316 005 20230223091350.0 010 $a3-642-32347-2 024 7 $a10.1007/978-3-642-32347-8 035 $a(CKB)3400000000085765 035 $a(SSID)ssj0000746011 035 $a(PQKBManifestationID)11446064 035 $a(PQKBTitleCode)TC0000746011 035 $a(PQKBWorkID)10860047 035 $a(PQKB)10905921 035 $a(DE-He213)978-3-642-32347-8 035 $a(MiAaPQ)EBC3070515 035 $a(PPN)168321629 035 $a(EXLCZ)993400000000085765 100 $a20120810d2012 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aInteractive Theorem Proving$b[electronic resource] $eThird International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings /$fedited by Lennart Beringer, Amy Felty 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (XI, 419 p. 37 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7406 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-32346-4 320 $aIncludes bibliographical references and index. 327 $aMetiTarski: Past and Future -- Computer-Aided Cryptographic Proofs -- A Differential Operator Approach to Equational Differential Invariants -- Abella: A Tutorial -- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers -- Construction of Real Algebraic Numbers in Coq -- A Refinement-Based Approach to Computational Algebra in Coq -- Bridging the Gap: Automatic Verified Abstraction of C -- Abstract Interpretation of Annotated Commands -- Verifying and Generating WP Transformers for Procedures on Complex Data -- Bag Equivalence via a Proof-Relevant Membership Relation -- Applying Data Refinement for Monadic Programs to Hopcroft?s Algorithm -- Synthesis of Distributed Mobile Programs Using Monadic Types in Coq -- Towards Provably Robust Watermarking -- Priority Inheritance Protocol Proved Correct -- Formalization of Shannon?s Theorems in SSReflect-Coq -- Stop When You Are Almost-Full: Adventures in Constructive Termination -- Certification of Nontermination Proofs -- A Compact Proof of Decidability for Regular Expression Equivalence -- Using Locales to Define a Rely-Guarantee Temporal Logic -- Charge! - A Framework for Higher-Order Separation Logic in Coq -- Mechanised Separation Algebra -- Directions in ISA Specification -- More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification -- A Language of Patterns for Subterm Selection -- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL -- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem -- Standalone Tactics Using OpenTheory -- Functional Programs: Conversions between Deep and Shallow Embeddings. 330 $aThis book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non-)termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7406 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer science 606 $aSoftware engineering 606 $aData protection 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aData and Information Security 606 $aTheory of Computation 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aData protection. 615 14$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aData and Information Security. 615 24$aTheory of Computation. 676 $a005.131 702 $aBeringer$b Lennart$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aFelty$b Amy$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aITP 2012 906 $aBOOK 912 $a996465748303316 996 $aInteractive Theorem Proving$92010767 997 $aUNISA