Ebook: Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings

This 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.

---

This 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.

---

This 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.
Content:
Front Matter....Pages -
MetiTarski: Past and Future....Pages 1-10
Computer-Aided Cryptographic Proofs....Pages 11-27
A Differential Operator Approach to Equational Differential Invariants....Pages 28-48
Abella: A Tutorial....Pages 49-50
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers....Pages 51-66
Bridging the Gap: Automatic Verified Abstraction of C....Pages 67-82
Abstract Interpretation of Annotated Commands....Pages 83-98
Verifying and Generating WP Transformers for Procedures on Complex Data....Pages 99-115
Bag Equivalence via a Proof-Relevant Membership Relation....Pages 116-132
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm....Pages 133-148
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq....Pages 149-165
Towards Provably Robust Watermarking....Pages 166-182
Priority Inheritance Protocol Proved Correct....Pages 183-200
Formalization of Shannon’s Theorems in SSReflect-Coq....Pages 201-216
Stop When You Are Almost-Full....Pages 217-232
Certification of Nontermination Proofs....Pages 233-249
A Compact Proof of Decidability for Regular Expression Equivalence....Pages 250-265
Using Locales to Define a Rely-Guarantee Temporal Logic....Pages 266-282
Charge!....Pages 283-298
Mechanised Separation Algebra....Pages 299-314
Directions in ISA Specification....Pages 315-331
More SPASS with Isabelle....Pages 332-337
A Language of Patterns for Subterm Selection....Pages 338-344
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL....Pages 345-360
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem....Pages 361-376
Standalone Tactics Using OpenTheory....Pages 377-392
Functional Programs: Conversions between Deep and Shallow Embeddings....Pages 393-404
Back Matter....Pages 405-411
....Pages 412-417