2. ITP 2011: Berg en Dal, The Netherlands

Invited Papers

• Don S. Batory:
  Towards Verification of Product Lines. 1
  
• Georges Gonthier:
  Advances in the Formalization of the Odd Order Theorem. 2
  
• Bart Jacobs, Ronny Wichers Schreur:
  Logical Formalisation and Analysis of the Mifare Classic Card in PVS. 3-17
  
• Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov:
  Challenges in Verifying Communication Fabrics. 18-21
  

Regular Papers

• Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal:
  Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. 22-38
  
• Lennart Beringer:
  Relational Decomposition. 39-54
  
• Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza:
  Structural Analysis of Narratives with the Coq Proof Assistant. 55-70
  
• Renaud Clavel, Laurence Pierre, Régis Leveugle:
  Towards Robustness Analysis Using PVS. 71-86
  
• Peter Gammie:
  Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. 87-102
  
• Georges Gonthier:
  Point-Free, Set-Free Concrete Linear Algebra. 103-118
  
• Sylvain Heraud, David Nowak:
  A Formalization of Polytime Functions. 119-134
  
• Johannes Hölzl, Armin Heller:
  Three Chapters of Measure Theory in Isabelle/HOL. 135-151
  
• Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl:
  Termination of Isabelle Functions via Termination of Rewriting. 152-167
  
• Ramana Kumar, Tjark Weber:
  Validating QBF Validity in HOL4. 168-183
  
• Ondrej Kuncar:
  Proving Valid Quantified Boolean Formulas in HOL Light. 184-199
  
• Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
  Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. 200-215
  
• Andreas Lochbihler, Lukas Bulwahn:
  Animating the Formalised Semantics of a Java-Like Language. 216-232
  
• Tarek Mhamdi, Osman Hasan, Sofiène Tahar:
  Formalization of Entropy Measures in HOL. 233-248
  
• David Monniaux, Pierre Corbineau:
  On the Generation of Positivstellensatz Witnesses in Degenerate Cases. 249-264
  
• Magnus O. Myreen, Jared Davis:
  A Verified Runtime for a Verified Theorem Prover. 265-280
  
• Tobias Nipkow:
  Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. 281-296
  
• Michael Norrish:
  Mechanised Computability Theory. 297-311
  
• Peter Reid, Ruben Gamboa:
  Automatic Differentiation in ACL2. 312-324
  
• Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein:
  seL4 Enforces Integrity. 325-340
  

Proof Pearls

• Chunhan Wu, Xingyuan Zhang, Christian Urban:
  A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). 341-356
  

Rough Diamonds

• Anthony C. J. Fox:
  LCF-Style Bit-Blasting in HOL4. 357-362
  
• Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell:
  Lem: A Lightweight Tool for Heavyweight Semantics. 363-369
  
• Phil Scott, Jacques D. Fleuriot:
  Composable Discovery Engines for Interactive Theorem Proving. 370-375
  
• Matej Urbas, Mateja Jamnik:
  Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. 376-382
  

Last update Fri May 25 08:24:34 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page