| Description |
1 online resource (xi, 417 pages) : illustrations |
| Series |
Lecture notes in computer science, 1611-3349 ; 7406 |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 7406. 1611-3349
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
MetiTarski: Past and Future / Lawrence C. Paulson -- Computer-Aided Cryptographic Proofs / Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz and Santiago Zanella Béguelin -- A Differential Operator Approach to Equational Differential Invariants (Invited Paper) / André Platzer -- Abella: A Tutorial / Andrew Gacek -- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers / Ruben Gamboa and John Cowles -- Construction of Real Algebraic Numbers in Coq / Cyril Cohen -- A Refinement-Based Approach to Computational Algebra in Coq / Maxime Dénès, Anders Mörtberg and Vincent Siles -- Bridging the Gap: Automatic Verified Abstraction of C / David Greenaway, June Andronick and Gerwin Klein -- Abstract Interpretation of Annotated Commands / Tobias Nipkow -- Verifying and Generating WP Transformers for Procedures on Complex Data / Patrick Michel and Arnd Poetzsch-Heffter -- Bag Equivalence via a Proof-Relevant Membership Relation / Nils Anders Danielsson -- Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm / Peter Lammich and Thomas Tuerk -- Synthesis of Distributed Mobile Programs Using Monadic Types in Coq / Marino Miculan and Marco Paviotti -- Towards Provably Robust Watermarking / David Baelde, Pierre Courtieu, David Gross-Amblard and Christine Paulin-Mohring |
|
Priority Inheritance Protocol Proved Correct / Xingyuan Zhang, Christian Urban and Chunhan Wu -- Formalization of Shannon's Theorems in SSReflect-Coq / Reynald Affeldt and Manabu Hagiwara -- Stop When You Are Almost-Full: Adventures in Constructive Termination / Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt -- Certification of Nontermination Proofs / Christian Sternagel and René Thiemann -- A Compact Proof of Decidability for Regular Expression Equivalence / Andrea Asperti -- Using Locales to Define a Rely-Guarantee Temporal Logic / William Mansky and Elsa L. Gunter -- Charge! A Framework for Higher-Order Separation Logic in Coq / Jesper Bengtson, Jonas Braband Jensen and Lars Birkedal -- Mechanised Separation Algebra / Gerwin Klein, Rafal Kolanski and Andrew Boyton -- Directions in ISA Specification / Anthony Fox -- More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification / Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand and Christoph Weidenbach -- A Language of Patterns for Subterm Selection / Georges Gonthier and Enrico Tassi -- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL / Fabian Immler and Johannes Hölzl -- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem / Lars Noschinski -- Standalone Tactics Using OpenTheory / Ramana Kumar and Joe Hurd -- Functional Programs: Conversions between Deep and Shallow Embeddings / Magnus O. Myreen |
| Summary |
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 |
| Analysis |
Computer science |
|
Software engineering |
|
Data protection |
|
Logic design |
|
Artificial intelligence |
|
Mathematical Logic and Formal Languages |
|
Logics and Meanings of Programs |
|
Systems and Data Security |
|
Computation by Abstract Devices |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed August 27, 2012) |
| Subject |
Automatic theorem proving -- Congresses
|
|
Software engineering -- Congresses
|
|
Informatique.
|
|
Automatic theorem proving
|
|
Software engineering
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Beringer, Lennart
|
|
Felty, Amy.
|
| ISBN |
9783642323478 |
|
3642323472 |
|
3642323464 |
|
9783642323461 |
|
