2. ITP 2011: Berg en Dal, The Netherlands
Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk (Eds.): Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings. Springer 2011 Lecture Notes in Computer Science ISBN 978-3-642-22862-9
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
- 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
- Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl: Termination of Isabelle Functions via Termination of Rewriting. 152-167
- 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
- David Monniaux, Pierre Corbineau: On the Generation of Positivstellensatz Witnesses in Degenerate Cases. 249-264
- Tobias Nipkow: Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. 281-296
- Michael Norrish: Mechanised Computability Theory. 297-311
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team