Verified Software. Theories, Tools, and Experiments

Name: Verified Software. Theories, Tools, and Experiments | 10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers

Ruzica Piskac Philipp Rümmer(Herausgeber*in)

Springer (Verlag)

Erschienen am 23. November 2018

XVI, 345 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-03592-1 (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
Preface
Organization
Abstracts of Invited Talks
Contract-based Compositional Verification of Infinite-State Reactive Systems
Verified Software: Theories, Tools, . and Engineering
Synthesis of Surveillance Strategies for Mobile Sensors
Contents
A Tree-Based Approach to Data Flow Proofs
1 Introduction
2 Example
3 Preliminaries
3.1 Path-Closed Tree Languages
3.2 Programs, Specifications, Floyd Proofs
4 Data Flow in Data Flow Graph vs. Data Flow in Program Traces
4.1 Data Flow Trees from the Data Flow Graph
4.2 Data Flow Trees from the Control Flow Graph
4.3 DFT(P#) = path-closure(DFT(Traces(P))
5 Data Flow Proofs and Cartesian Floyd Proofs
6 Related Work
7 Future Work
References
Executable Counterexamples in Software Model Checking
1 Introduction
2 Concrete Semantics for Executable Counterexamples
2.1 A Simple Imperative Language
2.2 Extending with External Functions and Memory
2.3 Counterexamples and Mock Environments
3 A Framework for Constructing Executable Counterexamples
4 Executable Counterexample Generation in SeaHorn
5 Experimental Evaluation
6 Related Work
7 Conclusion
References
Extending VIAP to Handle Array Programs
1 Introduction
2 Translation
3 VIAP
3.1 Instantiation
3.2 Proof Strategies
3.3 Multi-dimensional Arrays
4 Related Work
5 Concluding Remarks and Future Work
References
Lattice-Based Refinement in Bounded Model Checking
1 Introduction
2 Preliminaries
3 Construction of the Lattice of Facts
3.1 Definitions
3.2 Algorithm
4 Lattice-Based Bounded Model Checking
4.1 Definitions
4.2 Algorithm
5 Implementation and Evaluation
References
Verified Certificate Checking for Counting Votes
1 Introduction
2 The Protocol and Its HOL Formalisation
2.1 An Example Certificate
2.2 The HOL Formalisation
2.3 The Certificate Verifier
3 Translation into CakeML and Code Extraction
4 Experimental Results
5 Discussion
6 Related Work
7 Conclusion
References
Program Verification in the Presence of I/O
1 Introduction
2 Overview
3 File System Interaction
3.1 File System Model
3.2 File System FFI
4 A Verified TextIO Library
4.1 File System Properties
4.2 Library Implementation and Specifications
5 Case Study: A Verified Diff
6 Related Work
7 Conclusion
A Appendix: Further Example Programs
A.1 Cat
A.2 Sort
A.3 grep
References
TWAM: A Certifying Abstract Machine for Logic Programs
1 Introduction
2 Certifying Compilation in Proof-Passing Style
3 The Typed WAM (TWAM)
3.1 Syntax
3.2 Example: Code Section for Plus
3.3 Operational Semantics
3.4 Statics
3.5 Metatheory
4 Implementation
5 Related Work
6 Future Work
References
A Java Bytecode Formalisation
1 Introduction
2 The Need for Hierarchy of Instructions
3 Hierarchical Definition of Semantics
4 Static Semantics
5 Program Verification
6 Discussion on Bytecode Design
7 Related Work
8 Conclusions
References
Formalising Executable Specifications of Low-Level Systems
1 Introduction
2 Motivation
3 Preliminaries
4 The Deep Embedding
5 The SOS Interpreter
6 Hoare Logic
7 Case Study: Verifying Properties of Pip
8 Related Work
9 Conclusions and Further Work
A Appendix: Denotational Semantics
References
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
1 Problem, Contribution, and Outlook
2 Background
2.1 ABNF
2.2 ACL2
3 ABNF Formalization
3.1 Abstract Syntax
3.2 Semantics
3.3 Concrete Syntax
4 ABNF Grammar Parser
4.1 Implementation
4.2 Verification
5 Related Work
References
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components
1 Introduction
2 Motivating Example
2.1 Note on Implementation
3 Architectures
3.1 Metatheorems
4 The First Algorithm
5 The Second Algorithm
5.1 Example Revisited
5.2 Note
6 Related Work
7 Conclusion
References
SideTrail: Verifying Time-Balancing of Cryptosystems
1 Introduction
1.1 Related Work
2 Time-Balancing
3 Implementation
4 Case Study of the s2n TLS Library
4.1 Timing Stubs
4.2 Experiments
4.3 Discussion on the Timing Model
4.4 Verification Inspired Refactoring
5 Future Work
6 Conclusion
References
Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity
1 Introduction
2 Overview of Solidity
2.1 Contracts and Messages
2.2 Type Names
2.3 Statements
2.4 Expressions
2.5 Memory Objects in Solidity
3 Formalization
3.1 Big Step Semantics
3.2 Current State of the Coq Development
4 Related Work
5 Conclusions and Future Work
References
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
1 Introduction
2 Formal Foundations and Program Equivalence
3 Program Transformations
3.1 Handling Context-Independent Transformations Using Rewrite Rules
3.2 Handling Context-Dependent Transformations Using Coupling Predicates
4 Transformation Application Strategy
4.1 Using Congruence Rules to Simplify Proofs
4.2 Missing Premises and Widening
4.3 Potential for Automation of Proofs Using Rewrite Rules
5 Evaluation and Case Study
6 Related Work
7 Conclusion
References
Practical Methods for Reasoning About Java 8's Functional Programming Features
1 Introduction
2 Deductive Verification, the Java Modeling Language and the OpenJML Tool
3 Verifying Java's FP Features
3.1 Overly General Function Types
3.2 Implicit Iteration
4 Our Experience with a Case Study
4.1 Case Study Artifact
4.2 Implementation
4.3 Observations
5 Conclusion
References
Verification of Binarized Neural Networks via Inter-neuron Factoring
1 Introduction
2 Related Work
3 Preliminaries
4 Verification of BNNs via Hardware Verification
4.1 From BNN to Hardware Verification
4.2 Counting Optimization
5 Evaluation and Outlook
References
The Map Equality Domain
1 Introduction
2 Example
3 Related Work
4 Preliminaries
5 The Map Equality Domain
5.1 The Domain of Equalities and Disequalities
5.2 The Weak Equivalence Domain
5.3 The Map Equality Domain
5.4 Abstract Post Operator
6 Evaluation
References
Loop Detection by Logically Constrained Term Rewriting
1 Introduction
2 Preliminaries
3 Loop Criteria
4 Implementation
5 Applications
6 Conclusion
References
Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment
1 Introduction
2 Data Races and Shared Accesses
3 Low-Level Programming Disciplines
4 Formal Model and Relation to the Real World
5 Theorem and Correctness Proof
6 Untrusted Code
7 Transport-Triggered Memory
8 Mixed-Size/Misaligned Accesses
9 Inter-processor Interrupts
10 Bypassing the Store Buffer
11 Modifying Code
12 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken