Certified Programs and Proofs

Name: Certified Programs and Proofs | First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011, Proceedings

Jean-Pierre Jouannaud Zhong Shao(Herausgeber*in)

Springer (Verlag)

Erschienen am 15. November 2011

XV, 401 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-25379-9 (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

Intro
Title
Preface
Organization
Table of Contents
APLAS/CPP Invited Talks
Engineering Theories with Z3
Introduction
References
Algebra, Logic, Locality, Concurrency
References
Session 1: Logic and Types
Constructive Formalization of Hybrid Logic with Eventualities
Introduction
Propositional Logic
Mathematical Development
Decidability, Finite Types and Finite Sets
Formalization of Propositional Logic
Modal Logic
Mathematical Development
Demo Theorem
Formalization of Modal Logic
Hybrid Logic
Mathematical Development
Demo Theorem for Hybrid Logic
Formalization of Hybrid Logic
Conclusions
References
Proof-Carrying Code in a Session-Typed Process Calculus
Introduction
Dependent Session Types
Proof Irrelevance
Affirmation
Progress and Preservation
Concluding Remarks
References
Session 2: Certificates
Automated Certification of Implicit Induction Proofs
Introduction
Background and Notations
Noetherian Induction for Implicit Induction Proofs
Case Study: Validation of a Conformance Algorithm for the ABR Protocol
The Spike Specification
An Example of Implicit Induction Proof
Certifying Implicit Induction Proofs
Improvements
Conclusions and Future Work
References
A Proposal for Broad Spectrum Proof Certificates
Introduction
Proof Theory and Proof Certificates
The Basics of Sequent Calculus
Encoding Computation with the Sequent Calculus
Focused Proof Systems
LKF: A Focused Proof System for Classical Logic
Positive and Negative Macro Inference Rules
Some Examples of Proof Certificates
Non-Matrix Proof Systems
Fixed Points and Equality
Computation and Model Checking
Related Work
Future Work
Conclusion
References
Session 3: Invited Talk
Univalent Semantics of Constructive Type Theories
Session 4: Formalization
Formalization of Wu's Simple Method in Coq
Introduction
Related Work
Overview of Wu's Method
Cartesian Geometry
Rings and Ideals
Pseudo-Division and Pseudo-Remainder
Formalization in Coq
Algebraization
Certified Implementation
Benchmark
Conclusion
References
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
Introduction
Nominal Logic Preliminaries
Lambda Terms and Conversion
Defining -Constants with Nominal Isabelle
Basic Constants in -Calculus
The Proof of the Second Fixed Point Theorem
Conclusion
Related Work
References
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
Introduction
Types and Substrings
Grammars and Parse Trees
Parse Trees and the Parsing Context
Terminal Parsers and Parser Combinators
Updating the Parsing Context
Termination, Soundness and Prefix-Soundness
Completeness and Prefix-Completeness
Parser Generator Completeness
Implementation Issues
Related Work
Conclusion
References
A Decision Procedure for Regular Expression Equivalence in Type Theory
Finite Sets in Type Theory
Informal Motivations
Inductively Finite Sets in Type Theory
Regular Expressions
Derivatives
Similarity
Brzozowski Main Result
Description of the Decision Procedure
Representation in Type Theory
Some Examples
References
Session 5: Proof Assistants
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Introduction
The SAT and SMT Problems
SAT Solvers
SMT Solvers
A Modular and Efficient Coq Checker for SAT and SMT Proof Witnesses
Small Checkers for SAT
A Small Checker for Resolution Chains
Small Checkers for CNF Computation
Small Checkers for Congruence Closure and Linear Arithmetic
Refining the Term Representation
A Small Checker to Compute Congruence Closure
A Small Checker for Linear Arithmetic
The Simplifier Small Checker
Building a Coq Tactic
Results and Comparison with Other Works
Related Works
Experiments
Conclusion and Future Works
References
Modular SMT Proofs for Fast Reflexive Checking Inside Coq
Introduction
Overview
Certificate Checking and Generation for UF
Certificate Checking and Generation for LRA and LIA
Design of a Modular Nelson-Oppen Proof-Verifier
Experiments
Related Work
Conclusion and Perspectives
References
Tactics for Reasoning Modulo AC in Coq
Introduction
User Interface, Notation
Deciding Equality Modulo AC
The Algorithm and Its Proof
Reification
Matching Modulo AC
Bridging the Gaps
Neutral Elements
Subterms
Conclusions
Related Works
Directions for Future Works
References
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
Introduction
Related Work
LCF-Style Theorem Proving
Z3: Language and Proof Terms
Bit-Vectors in Higher-Order Logic
Proof Reconstruction
Experimental Results
Proof Generation with Z3
Bit-Blasting in HOL4
Proof Reconstruction in HOL4
Profiling
Conclusions
References
Session 6: Teaching
Teaching Experience: Logic and Formal Methods with Coq
Introduction
Syllabus
Traditional Logic: Weeks 1 and 2
Propositional Logic: Weeks 3 and 4
Predicate Logic: Weeks 5 and 6
Midterm Exam and Case Study: Week 7
Formal Induction: Week 8
Modal Logic: Weeks 9 and 10
Hoare Logic: Weeks 11 and 12
Other Topics: Week 13
What We Cut
Course Format
Results of Course
Related Work
Conclusion
References
The Teaching Tool CALCCHECK : A Proof-Checker for Gries and Schneider's" Logical Approach to Discrete Math"
Introduction
Related Work
CALCCHECK Overview
Teaching with CALCCHECK
Formalising LADM
Implementation Aspects
Conclusion and Future Work
References
Session 7: Invited Talk
VeriSmall: Verified Smallfoot Shape Analysis
Smallfoot
Syntax of Separation Logic
Semantics of Separation Logics
Fresh Variables
Paramodulation
Isolation
Soundness of Isolate
Symbolic Execution
Ghost Variables
Soundness of Symbolic Execution
Conclusion
References
Session 8: Programming Languages
Verification of Scalable Synchronous Queue
Introduction
The Inference Rules
Notations and Definitions
Reasoning Algorithms under Garbage Collection
Rules for Packaged-CAS Commands
Improved Rules for Control Flow Commands
Scalable Synchronous Queue
Proof for Synchronous Queue
Adapted Rules for casHead, casTail, n.casData, and n.casNext
Predicates for State Assertions
The Rely/Guarantee Conditions
Thread's Shared and Private States
The Proof, and What We Find
Related Work and Conclusion
References
COQ Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
Introduction
Overloading Rules
FFMM: Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
Syntax
Overloading Rules
Overloading Resolution
FFMM in Coq
Type Safety Proof
Lessons
Extensibility of Coq Mechanization
Witness Finding
Related Work
Conclusion and Future Work
References
Mechanizing the Metatheory of mini-XQuery
Introduction
Background
Basic Metatheory
Type Soundness
Determinacy
Operational Equivalences
Subtyping
Discussion
Related Work
Conclusions
References
Automatically Verifying Typing Constraints for a Data Processing Language
Introduction
Related Work
Overview
Review of Dminor (Data Processing Language)
Bemol (Intermediate Verification Language)
Syntax and Operational Semantics
Operational Semantics
Hoare Logic and Verification Condition Generation
Translation from Dminor to Bemol
Translation Function
Examples
Soundness
Formalisation and Machine-Checked Proofs
Implementation
High-Level Overview
Axiomatisation
Comparison between Dminor and DVerify
Conclusion
References
Session 9: Hardware Certification
Hardware-Dependent Proofs of Numerical Programs
Introduction
Overview of the Approach
Example: Double-Rounding
Example: Architecture Dependent Overflow
Example: KB3D
Example: Scalar Product
Underlying Technique
Principles of Interpretation in Why
Model of Data
Interpretation of Assembly Instructions
Translation of Annotated Functions
Conclusion
References
Coquet: A Coq Library for Verifying Hardware
Overview of Our System
Formal Development
Circuit Interfaces
Type Isomorphisms
Plugs
Abstract Syntax
Structural Specifications
Abstractions
Atoms and Modular Proofs
Proving Some Combinatorial Circuits
Proving a Half-Adder
n-Bits Integers
Two Specifications of a 1-Bit Adder
Ripple-Carry Adder
Divide and Conquer Adder
Sequential Circuits: Time and Loops
Interesting Corollaries
Comparisons with Related Work
Conclusion and Future Works
References
First Steps towards the Certification of an ARM Simulator Using Compcert
Introduction
Simulation of Systems-on-Chip
The Need for Certification
Main Lines of SimSoC-Cert
Overall Architecture
Stating Correctness Theorems
ARM Model
Processor Behavior
Coq Semantics of ARM Operations
ARM Operations in Simlight
Differences with the Coq Model of ARM Operations
Translation from Pseudo-code AST to Compcert-C AST
Current Proofs
Conclusion
References
Session 10: Miscellaneous
Full Reduction at Full Throttle
Implementations for the $\lambda $-Calculus
Calculus of Symbolic Reduction
Abstract Setting
Tagged Normalization
Tagless Normalization
Extension to the Calculus of Inductive Constructions
The Symbolic CIC
The Translation
Optimizations
Coinductive Types
Benchmarks
References
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
Introduction
Formalising Computational Frames for Coq-CIL
Oracles and Signatures
About Probabilities
Adversarial Process
Resource Constraints and Indistinguishability
Coq-CIL: Computational Indistinguishability Logic
Indistinguishability as a Distance Relation on Oracles
Contexts and the Sub rule
BSM
Bounded Storage Model
Protocol Description
Protocol Proved Using CIL
Conclusion
References
Session 11: Proof Pearls
Proof Pearl: The Marriage Theorem
Introduction
Related Work
Language and Formalisation
The Proof by Halmos and Vaughan
Sequences versus Indexed Families
Rado's Proof
The Mizar Formalisation
References
Author Index

Inhalt (PDF)

Systemvoraussetzungen

Als PDF speichern Als Link merken