Verified Software: Theories, Tools, Experiments
4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012 Proceedings
Published on 28. January 2012
XI, 326 pages
978-3-642-27705-4 (ISBN)
Description
This volume contains the proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2012, held in Philadelphia, PA, USA, in January 2012. The 20 revised full papers presented together with 2 invited talks and 2 tutorials were carefully revised and selected from 54 initial submissions for inclusion in the book. The goal of the VSTTE conference is to advance the state of the art through the interaction of theory development, tool evolution, and experimental validation. The papers address topics such as: specification and verification techniques, tool support for specification languages, tool for various design methodologies, tool integration and plug-ins, automation in formal verification, tool comparisons and benchmark repositories, combination of tools and techniques, customizing tools for particular applications, challenge problems, refinement methodologies, requirements modeling, specification languages, specification/verification case-studies, software design methods, and program logic.
More details
Other editions
Additional editions
Rajeev Joshi | Peter Müller | Andreas Podelski
Verified Software: Theories, Tools, Experiments
4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012 Proceedings
Book
01/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Cyber War, Formal Verification and Certified Infrastructure
- A Certified Multi-prover Verification Condition Generator
- Introduction
- Logical Contexts
- Dependently Typed de Bruijn Indices
- Terms and Propositions
- Logical Contexts, Semantics
- The Core Programming Language
- Informal Description
- Formal Syntax of Expressions
- Operational Semantics
- Weakest Precondition Calculus
- Extraction of a Certified Verification Tool
- Concrete WP Computation
- Producing Concrete Syntax with Explicit Binders
- Extraction and Experimentation
- Conclusions, Related Works and Perspectives
- References
- Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT
- Introduction
- Macro-Assembler Semantics
- C Semantics
- Integrated C-IL+MASM-Semantics
- Calling Convention
- Semantics
- Pervasive Theory
- Compiler Consistency
- Results
- Future Work
- Conclusion
- References
- The Location Linking Concept: A Basis for Verification of Code Using Pointers
- Introduction
- Specification of a System of Linked Locations
- A Formal Specification
- Shared Conceptual State
- Position Type
- Operations
- Memory Management
- Performance and Extensions
- Implementation Flexibility
- Application
- Specification of a Stack Concept
- Pointer-Based Implementation of Stacks
- Verification Process
- Closely Related Work
- Summary
- References
- Verifying Implementations of Security Protocols by Refinement
- Introduction
- Background: The VCC Verifier
- Case Study: Trusted Platform Module
- Creating and Loading Objects
- Key Management as a Security Protocol
- Refinement Approach
- Refinement in VCC
- High-Level Protocol Definition (L0)
- From Term Algebra to Byte Strings (L1)
- Physical Code (L2)
- Empirical Results
- Related Work
- Conclusions
- References
- Deciding Functional Lists with Sublist Sets
- Introduction
- Examples
- Logic FLS2 of Functional Lists with Sublists Sets
- Preliminaries
- Logic FLS of Functional Lists with Sublists
- Decision Procedure for FLS
- Extension with Sets of Sublists and Content Sets
- Conclusion
- References
- Developing Verified Programs with Dafny
- References
- Verifying Two Lines of C with Why3: An Exercise in Program Verification
- Introduction
- Unobfuscation
- Overview of Why3
- Verification
- Specification
- Correctness Proof
- Discussion
- References
- Annotated Source Code
- Development and Evaluation of LAV:An SMT-Based Error Finding Platform
- Introduction
- Motivating Example
- Modelling Variables, Data Types, and Blocks
- Modelling Control Flow
- Correctness Conditions
- Transforming a Code Model into an SMT Goal
- Implementation
- Evaluation and Comparison to Related Tools
- Application in Education
- Conclusions and Further Work
- References
- A Lightweight Technique for Distributed and Incremental Program Verification
- Introduction
- The SPARK Language and Tools
- The SPARK Language
- The SPARK Tool Chain
- Verification in Practice
- Increasing Verification Throughput
- Memcached
- Integrating Memcached into the SPARK Toolchain
- Experiments
- Incremental Solving
- Distributed Solving
- Related Work
- Conclusion
- References
- A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar
- Introduction
- Background
- Scope of Comparison
- Translation of a Simple Java Program
- Comparison of Language Features
- Basic Assertion Language
- Basic Control Flow
- Annotations
- Specification of Contracts
- Modeling Data Structures and Object Oriented Type Systems
- Unique Features and Tool Support
- Preliminary Validation: Ruby to Boogie and Pilar
- Type System Modeling
- Handling Arrays
- Modeling Fields
- Control Flow
- Summary
- Related Work
- Conclusion and Future Work
- References
- LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
- Introduction
- BMC and LLBMC's Built-In Checks
- LLVM
- The Approach of LLBMC
- From LLVM-IR to ILR
- Adding Checks to the ILR Formula
- Simplification of the ILR Formula
- Counterexample Generation
- Encoding Memory Checks
- Evaluation
- Related Work
- Conclusions and Future Work
- References
- The Marriage of Exploration and Deduction
- Modeling and Validating the Train Fare Calculation and Adjustment SystemUsing VDM++
- Introduction
- Project Overview
- The TFCAS System: An Informal Overview
- Goals and Approach of the Project
- VDM++ Model of the TFCAS
- Architecture of the System
- A Simple Example of the TFCAS's Functionality
- Analysis of Identified Issues
- Testing and Validating Process
- Experiments
- Lessons Learned
- Related Work
- Conclusions
- References
- Formalized Verification of Snapshotable Trees: Separation and Sharing
- Introduction
- Case Study: Snapshotable Trees
- Interface: Operations on Snapshotable Trees
- Example Client Code
- Implementations of Snapshotable Trees
- Abstract Specification and Client Code Verification
- Specification of the ITree Interface
- Iterator Specification
- Client Code Verification
- Implementation A1B1
- Iterator
- On the Verification of Implemented Code
- Related Work
- Conclusion and Future Work
- References
- Appendix
- Comparing Verification Condition Generation with Symbolic Execution: An Experience Report
- Introduction
- Background
- Verification Condition Generation
- Symbolic Execution
- Experiment and Results
- Additional Observations
- Heap Compression
- Branching
- Related Work
- Conclusion
- References
- Verification of TLB Virtualization Implemented in C
- Introduction
- Verification Methodology
- VCC Background
- Modelling Hardware
- Specification
- Host Hardware Model
- Virtual Hardware Model
- Memory Virtualization
- Correctness of TLB Virtualization
- Implementation and Verification in VCC
- Specification
- Implementation
- Verification
- Conclusion and Future Work
- References
- Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH
- Introduction
- The Tool Chain
- The Specification Language
- Translation of the SPS to Duration Calculus
- The Correctness Properties
- The Tool
- Planning of the Feasibility Study
- Study Goals and Questions
- Selection of the Sample
- Feasibility Study Design
- Analysis of the Results
- Benefit
- Observations
- Threats to Validity
- Construct Validity
- External Validity
- Conclusion
- References
- Our Experience with the CodeContracts Static Checker
- References
- Isabelle/Circus: A Process Specification and Verification Environment
- Introduction
- Background
- Isabelle, HOL and Isabelle/HOL
- Advanced Specification Constructs in Isabelle/HOL
- Circus and Its UTP Foundation
- Isabelle/Circus
- Alphabets and Variables
- Synchronization Infrastructure: Name Sets and Channels
- Actions and Processes
- Using Isabelle/Circus
- Writing Specifications
- Relational and Functional Refinement in Circus
- Refinement Proofs
- Conclusions
- References
- Termination Analysis of Imperative Programs Using Bitvector Arithmetic
- Introduction
- A Brief Overview of LLVM and Its Use in KITTeL
- LLVM-IR
- Termination Analysis Using LLVM
- Translating LLVM-IR Programs into Transition Systems
- Representing Transition Systems Using int-Based TRSs
- Termination Analysis of int-Based TRSs
- Encoding Bitvector Arithmetic
- Phase 1
- Phase 2
- Experimental Results and Evaluation
- Conclusions
- References
- Specifying and Verifying the Correctness of Dynamic Software Updates
- Introduction
- Defining Dynamic Software Update Correctness
- Prior Work on Update Correctness
- Client-Oriented Specifications
- Verification via Program Merging
- Syntax
- Semantics
- Program Merging Transformation
- Equivalence
- Experiments
- Programs
- Effectiveness
- Related Work
- Summary
- References
- Symbolic Execution Enhanced System Testing
- Introduction
- Background
- Approach
- Testing Algorithms
- Experience
- Conclusion
- References
- Infeasible Code Detection
- Introduction
- Examples of Infeasible Code
- Infeasible Code, Effectual Sets, and Path Covers
- A Path Cover Algorithm
- Checking Constrained Path Infeasibility
- Implementation
- Evaluation
- Conclusion
- References
- Author Index
