TY  - BOOK
AU  - Beringer,Lennart
AU  - Felty,Amy
TI  - Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 
SN  - 9783642323478
PY  - 2012///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Software engineering
KW  - Computer security
KW  - Computers
KW  - Computer logic
KW  - Mathematical logic
KW  - Artificial intelligence
N1  - MetiTarski: 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
UR  - http://dx.doi.org/10.1007/978-3-642-32347-8
ER  -