Skip to main content
SpringerLink
Log in

Interactive Theorem Proving

Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings

  • Conference proceedings
  • © 2011

Overview

Editors:
  1. Marko Eekelen

    1. Faculteit Informatica, Open Universiteit, Heerlen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Herman Geuvers

    1. FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Nijmegen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Julien Schmaltz

    1. Faculteit Informatica, Open Universiteit, Heerlen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Freek Wiedijk

    1. FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Nijmegen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Fast track conference proceedings
  • Unique visibility
  • State of the art research

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

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

Included in the following conference series:

Conference proceedings info: ITP 2011.

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 Papers

    1. Towards Verification of Product Lines

      • Don Batory
      Pages 1-1

    2. Advances in the Formalization of the Odd Order Theorem

      • Georges Gonthier
      Pages 2-2

    3. Logical Formalisation and Analysis of the Mifare Classic Card in PVS

      • Bart Jacobs, Ronny Wichers Schreur
      Pages 3-17

    4. Challenges in Verifying Communication Fabrics

      • Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov
      Pages 18-21

  3. Regular Papers

    1. Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq

      • Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal
      Pages 22-38

    2. Relational Decomposition

      • Lennart Beringer
      Pages 39-54

    3. Structural Analysis of Narratives with the Coq Proof Assistant

      • Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza
      Pages 55-70

    4. Towards Robustness Analysis Using PVS

      • Renaud Clavel, Laurence Pierre, Régis Leveugle
      Pages 71-86

    5. Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments

      • Peter Gammie
      Pages 87-102

    6. Point-Free, Set-Free Concrete Linear Algebra

      • Georges Gonthier
      Pages 103-118

    7. A Formalization of Polytime Functions

      • Sylvain Heraud, David Nowak
      Pages 119-134

    8. Three Chapters of Measure Theory in Isabelle/HOL

      • Johannes Hölzl, Armin Heller
      Pages 135-151

    9. Termination of Isabelle Functions via Termination of Rewriting

      • Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
      Pages 152-167

    10. Validating QBF Validity in HOL4

      • Ramana Kumar, Tjark Weber
      Pages 168-183

    11. Proving Valid Quantified Boolean Formulas in HOL Light

      • Ondřej Kunčar
      Pages 184-199

    12. Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

      • L. Lambán, F. J. Martín-Mateos, J. Rubio, J. L. Ruiz-Reina
      Pages 200-215

    13. Animating the Formalised Semantics of a Java-Like Language

      • Andreas Lochbihler, Lukas Bulwahn
      Pages 216-232

    14. Formalization of Entropy Measures in HOL

      • Tarek Mhamdi, Osman Hasan, Sofiène Tahar
      Pages 233-248

    15. On the Generation of Positivstellensatz Witnesses in Degenerate Cases

      • David Monniaux, Pierre Corbineau
      Pages 249-264
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

About this book

This book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011.
The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.

Editors and Affiliations

  • Faculteit Informatica, Open Universiteit, Heerlen, The Netherlands

    Marko Eekelen, Julien Schmaltz

  • FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Nijmegen, The Netherlands

    Herman Geuvers, Freek Wiedijk

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation