Skip to main content
SpringerLink
Log in
Book cover

Interactive Theorem Proving

Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings

  • Conference proceedings
  • © 2012

Overview

Editors:
  1. Lennart Beringer

    1. Department of Computer Science, Princeton University, Princeton, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Amy Felty

    1. School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Up to date results
  • State of the art research
  • Fast-track conference proceedings

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 7406)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: ITP 2012.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (29 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Talks

    1. MetiTarski: Past and Future

      • Lawrence C. Paulson
      Pages 1-10

    2. Computer-Aided Cryptographic Proofs

      • Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin
      Pages 11-27

    3. A Differential Operator Approach to Equational Differential Invariants

      • André Platzer
      Pages 28-48

  3. Invited Tutorial

    1. Abella: A Tutorial

      • Andrew Gacek
      Pages 49-50

  4. Formalization of Mathematics I

    1. A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers

      • Ruben Gamboa, John Cowles
      Pages 51-66

    2. Construction of Real Algebraic Numbers in Coq

      • Cyril Cohen
      Pages 67-82

    3. A Refinement-Based Approach to Computational Algebra in Coq

      • Maxime Dénès, Anders Mörtberg, Vincent Siles
      Pages 83-98

  5. Program Abstraction and Logics

    1. Bridging the Gap: Automatic Verified Abstraction of C

      • David Greenaway, June Andronick, Gerwin Klein
      Pages 99-115

    2. Abstract Interpretation of Annotated Commands

      • Tobias Nipkow
      Pages 116-132

    3. Verifying and Generating WP Transformers for Procedures on Complex Data

      • Patrick Michel, Arnd Poetzsch-Heffter
      Pages 133-148

  6. Data Structures and Synthesis

    1. Bag Equivalence via a Proof-Relevant Membership Relation

      • Nils Anders Danielsson
      Pages 149-165

    2. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm

      • Peter Lammich, Thomas Tuerk
      Pages 166-182

    3. Synthesis of Distributed Mobile Programs Using Monadic Types in Coq

      • Marino Miculan, Marco Paviotti
      Pages 183-200

  7. Security

    1. Towards Provably Robust Watermarking

      • David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring
      Pages 201-216

    2. Priority Inheritance Protocol Proved Correct

      • Xingyuan Zhang, Christian Urban, Chunhan Wu
      Pages 217-232

    3. Formalization of Shannon’s Theorems in SSReflect-Coq

      • Reynald Affeldt, Manabu Hagiwara
      Pages 233-249

  8. (Non-)Termination and Automata

    1. Stop When You Are Almost-Full

      • Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt
      Pages 250-265

    2. Certification of Nontermination Proofs

      • Christian Sternagel, René Thiemann
      Pages 266-282

    3. A Compact Proof of Decidability for Regular Expression Equivalence

      • Andrea Asperti
      Pages 283-298
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

About this book

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.

Editors and Affiliations

  • Department of Computer Science, Princeton University, Princeton, USA

    Lennart Beringer

  • School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, Canada

    Amy Felty

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation