Certified Programs and Proofs
First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011, Proceedings
Published on 15. November 2011
XV, 401 pages
978-3-642-25379-9 (ISBN)
Description
This book constitutes the referred proceedings of the First International Conference on Certified Programs and Proofs, CPP 2011, held in Kenting, Taiwan, in December 2011.
The 24 revised regular papers presented together with 4 invited talks were carefully reviewed and selected from 49 submissions. They are organized in topical sections on logic and types, certificates, formalization, proof assistants, teaching, programming languages, hardware certification, miscellaneous, and proof perls.
The 24 revised regular papers presented together with 4 invited talks were carefully reviewed and selected from 49 submissions. They are organized in topical sections on logic and types, certificates, formalization, proof assistants, teaching, programming languages, hardware certification, miscellaneous, and proof perls.
More details
Other editions
Additional editions
Jean-Pierre Jouannaud | Zhong Shao
Certified Programs and Proofs
First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011, Proceedings
Book
11/2011
Springer
€53.49
Shipment within 7-9 days
Content
- 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
