ITP 2012 Accepted Papers

Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt. Stop when you are Almost-Full

Maxime Dénès, Anders Mörtberg and Vincent Siles. A refinement-based approach to computational algebra in Coq

Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand and Christoph Weidenbach. More SPASS with Isabelle—Superposition with Hard Sorts and Configurable Simplification

Georges Gonthier and Enrico Tassi. A language of patterns for subterm selection

Ruben Gamboa and John Cowles. A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers

David Greenaway, June Andronick and Gerwin Klein. Bridging the Gap: Automatic Verified Abstraction of C

Peter Lammich and Thomas Tuerk. Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm

Andrea Asperti. A compact proof of decidability for regular expression equivalence

Gerwin Klein, Rafal Kolanski and Andrew Boyton. Mechanised Separation Algebra (Rough Diamond)

Nils Anders Danielsson. Bag Equivalence via a Proof-Relevant Membership Relation

David Baelde, Pierre Courtieu, David Gross-Amblard and Christine Paulin-Mohring. Towards Provably Robust Watermarking

Tobias Nipkow. Abstract Interpretation of Annotated Commands

René Thiemann and Christian Sternagel. Certification of Nontermination Proofs

Fabian Immler and Johannes Hölzl. Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL

Cyril Cohen. Construction of real algebraic numbers in Coq

Reynald Affeldt and Manabu Hagiwara. Formalization of Shannon's Theorems in SSReflect-Coq

Marino Miculan and Marco Paviotti. Synthesis of distributed mobile programs using hybrid modal types in Coq

Jesper Bengtson, Jonas Braband Jensen and Lars Birkedal. Tactics for Verifiying Object-Oriented Programs with Higher-Order Separation Logic in Coq

Lars Noschinski. Proof Pearl: A Probabilistic Proof for the Girth-Chromatic number Theorem

Patrick Michel and Arnd Poetzsch-Heffter. Verifying and Generating WP Transformers for Procedures on Complex Data

Xingyuan Zhang, Christian Urban and Chunhan Wu. Proving the Priority Inheritance Protocol Correct

Anthony Fox. Directions in ISA Specification (Rough Diamond)

Ramana Kumar and Joe Hurd. Standalone Tactics using OpenTheory (Rough Diamond)

Magnus O. Myreen. Functional programs: conversions between deep and shallow embeddings (Rough Diamond)

William Mansky and Elsa Gunter. Using Locales to Define a Rely-Guarantee Temporal Logic