Interactive Theorem Proving

Name: Interactive Theorem Proving | Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings

Marko Van Eekelen Herman Geuvers Julien Schmaltz Freek Wiedijk(Herausgeber*in)

Springer (Verlag)

Erschienen am 2. August 2011

XI, 383 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-22863-6 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken