This book constitutes the refereed proceedings of the First International Conference on Interactive Theorem proving, ITP 2010, held in Edinburgh, UK, in July 2010. The 33 revised full papers presented were carefully reviewed and selected from 74 submissions. The papers are organized in topics such as counterexample generation, hybrid system verification, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.
Author(s): Gerwin Klein (auth.), Matt Kaufmann, Lawrence C. Paulson (eds.)
Series: Lecture Notes in Computer Science 6172 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 495
Tags: Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Formal Languages; Programming Languages, Compilers, Interpreters; Artificial Intelligence (incl. Robotics); Antibodies
Front Matter....Pages -
A Formally Verified OS Kernel. Now What?....Pages 1-7
Proof Assistants as Teaching Assistants: A View from the Trenches....Pages 8-8
A Certified Denotational Abstract Interpreter....Pages 9-24
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure....Pages 25-34
A New Foundation for Nominal Isabelle....Pages 35-50
(Nominal) Unification by Recursive Descent with Triangular Substitutions....Pages 51-66
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks....Pages 67-82
Extending Coq with Imperative Features and Its Application to SAT Verification....Pages 83-98
A Tactic Language for Declarative Proofs....Pages 99-114
Programming Language Techniques for Cryptographic Proofs....Pages 115-130
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder....Pages 131-146
Formal Proof of a Wave Equation Resolution Scheme: The Method Error....Pages 147-162
An Efficient Coq Tactic for Deciding Kleene Algebras....Pages 163-178
Fast LCF-Style Proof Reconstruction for Z3....Pages 179-194
The Optimal Fixed Point Combinator....Pages 195-210
Formal Study of Plane Delaunay Triangulation....Pages 211-226
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison....Pages 227-242
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture....Pages 243-258
Automated Machine-Checked Hybrid System Safety Proofs....Pages 259-274
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study....Pages 275-290
Case-Analysis for Rippling and Inductive Proof....Pages 291-306
Importing HOL Light into Coq....Pages 307-322
A Mechanized Translation from Higher-Order Logic to Set Theory....Pages 323-338
The Isabelle Collections Framework....Pages 339-354
Interactive Termination Proofs Using Termination Cores....Pages 355-370
A Framework for Formal Verification of Compiler Optimizations....Pages 371-386
On the Formalization of the Lebesgue Integration Theory in HOL....Pages 387-402
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem....Pages 403-418
Equations: A Dependent Pattern-Matching Compiler....Pages 419-434
A Mechanically Verified AIG-to-BDD Conversion Algorithm....Pages 435-449
Inductive Consequences in the Calculus of Constructions....Pages 450-465
Validating QBF Invalidity in HOL4....Pages 466-480
Higher-Order Abstract Syntax in Isabelle/HOL....Pages 481-484
Separation Logic Adapted for Proofs by Rewriting....Pages 485-489
Developing the Algebraic Hierarchy with Type Classes in Coq....Pages 490-493
Back Matter....Pages -
