Skip to main content
SpringerLink
Log in
Book cover
  • Conference proceedings
  • © 2011

Interactive Theorem Proving

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

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)

Conference series link(s): ITP: International Conference on Interactive Theorem Proving

Conference proceedings info: ITP 2011.

Sections

Buy it now

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

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

Table of contents (29 papers)

  1. Front Matter

    PDF

  2. Invited Papers

    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

    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

    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

Back to top

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.
Back to top

Keywords

Back to top

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

Back to top

Bibliographic Information

Back to top

Publish with us

Policies and ethics

Back to top
Access via your institution

Buy it now

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

Search

Navigation