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