Interactive Theorem Proving
Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings
Published on 2. August 2011
XI, 383 pages
978-3-642-22863-6 (ISBN)
Description
This book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011.
The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, 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.
The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, 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.
More details
Other editions
Additional editions
Marko Van Eekelen | Herman Geuvers | Julien Schmaltz
Interactive Theorem Proving
Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings
Book
08/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Papers
- Towards Verification of Product Lines
- Reference
- Advances in the Formalization of the Odd Order Theorem
- Logical Formalisation and Analysis of the Mifare Classic Card in PVS
- Introduction
- Shift Registers, Generally
- Adding a Filter Function Parameter
- The Mifare LFSR and Filter Function
- Rollback Results
- Rolling Back Communication
- The Mifare Classic Authentication Protocol
- Formalising Attacks
- The Two-Table Attack
- The Odd-from-Even Attack
- Conclusions
- References
- Challenges in Verifying Communication Fabrics
- Communication Fabrics
- Verification Challenges
- xMAS Approach to Modeling and Verification
- Quality of Service Analysis and Optimization
- References
- Regular Papers
- Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
- Introduction
- Reasoning with Interfaces
- Interface ICell
- Method Proxyset
- Class Cell
- Interface IRecell
- Class Recell
- Class World
- Abstract Representation
- Uniform Predicates
- Stacks
- Semantic Commands
- Specification Logic
- Connecting the Assertion Logic with the Specification Logic
- Recursion
- Instantiation to an Object-Oriented Language
- Semantics of the Programming Language
- Syntactic Hoare Triples and the Concrete Assertion Logic
- Related Work
- Conclusion and Future Work
- References
- Relational Decomposition
- Introduction
- Related Work
- The Principle of Decomposition
- Introducing Interpolating Witnesses
- Properties of Decomposition Operators
- Application: Decomposed Justification of Relational Hoare Logic
- Language Definition and Unary Program Logic
- Derivation of Relational Proof Rules
- New Rules for Dissonant Loops
- Extensions and Applications
- Discussion
- References
- Structural Analysis of Narratives with the Coq Proof Assistant
- Introduction
- Related Works
- Logical Approaches to Narratology
- Related Applications of Linear Logic
- Proof Assistants Support for LL
- ILL as a Representational Theory for Narratology
- Modelling of Narratives Specification through an ILL Sequent
- Interpreting a Proof as a Narrative
- Using the Coq Proof Assistant for Narrative Properties Analysis
- ILL Encoding into Coq
- Well-Formed Narrative Generation: Proving an ILL Sequent In Coq
- Stability of an ILL Narrative Sequent: Well-Formed Sequents
- Second Order Analysis of Narratives Specification
- Conclusion
- References
- Towards Robustness Analysis Using PVS
- Introduction
- Previous Results
- Related Works
- First Solution Using ACL2
- Fault Models in PVS
- Single Faults
- Spatial Multiplicity
- Temporal Multiplicity
- From VHDL to PVS
- Translation
- Proof Process
- Experiments
- Cash Withdrawal System
- FIR Filter
- CAN Interface
- Conclusion
- References
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
- Introduction
- Semantics of Knowledge-Based Programs
- Automata for KBPs
- A Sufficient Condition for Finite-State Implementations
- An Effective Construction
- A Synthesis Algorithm
- Perfect Recall for a Single Agent
- The Robot
- Perfect Recall in Broadcast Environments with Deterministic Protocols
- The Muddy Children
- Perspective and Related Work
- References
- Point-Free, Set-Free Concrete Linear Algebra
- Introduction
- Matrix Operations
- A Combinatorial and Algebraic Hierarchy
- Basic Algebra
- Block and Reshaping Operations
- Gaussian Elimination and Row Spaces
- Extended Gaussian Elimination
- Rank Theory
- Set Operations
- Algebras and Subrings
- General Direct Sums
- On Subspace Equality
- Monoidal Set Operations
- A Direct Sum Package
- Module and Representation Theory
- Group Representation
- Simple Modules
- Some Classic Results
- P-Stability and Extraspecial Representations
- References
- A Formalization of Polytime Functions
- Introduction
- Preliminaries
- Multivariate Polynomials
- Notations
- Characterizing Polytime Functions
- Cobham's Class
- Bellantoni-Cook's Class
- Compiling Bellantoni-Cook into Cobham
- Compiling Cobham into Bellantoni-Cook
- Applications
- Application to the Second Author's Toolbox
- Application to Certicrypt
- Conclusions and Future Work
- References
- Three Chapters of Measure Theory in Isabelle/HOL
- Introduction
- Preliminaries
- Extended Reals
- Measure Theory
- The s-Algebra
- Measure Spaces
- Lebesgue Integral
- Radon-Nikodým Derivative
- Product Measure and Fubini's Theorem
- Lebesgue Measure
- Discussion
- Related Work
- Conclusion
- References
- Termination of Isabelle Functions via Termination of Rewriting
- Introduction
- Preliminaries
- Higher-Order Logic
- Supported Fragment
- Function Definitions By Well-Founded Recursion
- IsaFoR - Term Rewriting Formalized in Isabelle/HOL
- Terminology and Notation
- The Reduction to Rewriting
- Encoding Expressions and Defining Equations
- Embedding Functions
- Rewrite Lemmas
- The Simulation Property
- Reduction of Termination Goals
- Proof of the Simulation Property
- Examples
- Extensions
- Conclusion
- References
- Validating QBF Validity in HOL4
- Introduction
- Related Work
- Background and Theory
- Quantified Boolean Formulae
- Skolem Functions and Models
- Certificates of Validity
- Higher-Order Logic
- Checking Validity Certificates in HOL4
- Overview
- Preparing the Formula for MiniSat
- Hypothesis Elimination
- Example
- Experimental Results
- Run-Times
- Profiling and Future Improvements
- Conclusions
- References
- Proving Valid Quantified Boolean Formulas in HOL Light
- Introduction
- Related Work
- Theory
- Quantified Boolean Formulas
- QBF Models
- Squolem's Certificates of Validity
- System Description
- Preprocessing
- Validating Squolem's Model
- Adding Quantifiers
- Proving the Quantified Model Term
- LIFT
- Implementation and Evaluation
- Implementation of Rules
- Alpha-Equivalence Optimization
- Run-Times
- Conclusions and Future Work
- References
- Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
- Introduction
- Algebraic Simplicial Topology
- The Normalization Theorem in ACL2
- Simplicial Sets and Chain Complexes
- The Normalized Chain Complex
- Defining the Reduction
- The Main Theorems
- Simplicial Polynomials
- The Ring of Simplicial Polynomials
- Formal Proofs in the Polynomial Framework
- Lifting Proofs from the Polynomial Framework
- Conclusions and Further Work
- References
- Animating the Formalised Semantics of a Java-Like Language
- Introduction
- Related Work
- Background: The Code Generator Framework and Refinement
- Code Generation in Isabelle
- The Predicate Compiler
- Isabelle Locales and Code Generation
- Tabling the Reflexive Transitive Closure
- An Executable Definite Description Operator
- JinjaThreads: Well-Formedness Checker and Interpreter
- Overview of JinjaThreads
- The Type System and Well-Formedness Conditions
- The Semantics
- The Scheduler
- Tabulation
- Efficiency of the Interpreter
- Guidelines for Executable Formalisations
- Conclusion and Future Work
- References
- Formalization of Entropy Measures in HOL
- Introduction
- Related Work
- Extended Real Numbers
- Formalization of Measure, Integration and Probability
- Measure Theory
- Lebesgue Integral
- Probability Theory
- Measures of Entropy in HOL
- Shannon Entropy
- Relative Entropy
- Applications
- Conclusions
- References
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- Introduction
- Witnesses
- Nonnegativity Witnesses
- Unsatisfiability Witnesses for Polynomial Inequalities
- Solving the Sums-of-Squares Problem
- Reduction to Semidefinite Programming
- How to Deal with Degenerate Cases
- Simplified Algorithm
- More Efficient Algorithm
- Extensions and Alternative Implementation
- Sub-algorithms and Implementation
- Preliminary Reductions
- Examples
- Conclusion and Further Works
- References
- A Verified Runtime for a Verified Theorem Prover
- Introduction
- The Milawa System
- The Trusted Core
- The Verified Theorem Prover
- The Role of a Verified Runtime
- Requirements and Design Decisions
- I/O Requirements
- Designing for Performance and Scalability
- The Jitawa Specification
- Syntax
- Evaluation Semantics
- Parsing and Printing
- Top-Level Specification
- The Jitawa Implementation
- Compilation to Bytecode
- From Bytecode to Machine Code
- I/O
- Top-Level Correctness Theorem
- The Combination of Milawa and Jitawa
- Discussion and Related Work
- References
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
- Introduction
- Basics
- Worklist Algorithms
- While Combinators
- Worklist Algorithms
- Sets over a Quasi-Order
- Collecting Modulo Subsumption
- Implementing Sets Modulo
- Maps
- Implementing Sets Modulo by Maps
- Implementing Maps by Tries
- Stepwise Implementation in General
- Application to Plane Graphs
- Plane Graph Isomorphisms
- Sets of Graphs Modulo Isomorphism
- Application to Hales's Proof
- Conclusion
- References
- Mechanised Computability Theory
- Introduction
- The -Calculus: First Steps
- Normal Order Reduction
- Rewriting with -Equivalence
- Bracket Abstraction
- Church Arithmetic
- Reflection and the Universal Machine in the -Calculus
- Church de Bruijn Terms
- The Universal Machine
- The Recursive Functions
- Computational Equivalence
- Computability Theorems
- Related Work
- Conclusion
- References
- Automatic Differentiation in ACL2
- Introduction
- Related Work
- Introducing the Defderivative Event
- The Implementation of Defderivative
- Finding the Derivative
- Proof Structure
- The Path to Elementary Functions
- Adding New Derivative Facts: Hyperbolic Trigonometric Functions
- Conclusions
- References
- seL4 Enforces Integrity
- Introduction
- Access Control Enforcement and seL4
- Example
- seL4
- Access Control Enforcement
- Formalisation of Integrity Preservation
- Authority Types
- Subjective Policy Wellformedness
- Policy/Abstraction Refinement
- Specification of Integrity
- Top Level Statements
- Proof and Application
- Proof
- Application
- Limitations
- Related Work
- Conclusions
- References
- Proof Pearls
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
- Introduction
- Preliminaries
- The Myhill-Nerode Theorem, First Part
- Myhill-Nerode, Second Part
- Conclusion and Related Work
- References
- Rough Diamonds
- LCF-Style Bit-Blasting in HOL4
- Introduction
- Representation of Bit-Vectors
- Bit-Vector Operations
- Bit-Blasting
- Summary
- References
- Lem: A Lightweight Tool for Heavyweight Semantics
- Motivation
- Portable Definitions with Lem
- Implementation
- Future work
- References
- Composable Discovery Engines for Interactive Theorem Proving
- Introduction
- Framework
- Composition
- Trees
- Chains
- Results
- Conclusion
- References
- Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers
- Introduction
- The Diagrammatic Language
- Sentential Reasoner
- Formalisation of Diagrams in Isabelle/HOL
- Translation
- Heterogeneous Integration
- References
- Author Index
