Linked e-resources
Details
Table of Contents
Intro
Preface
Organization
Invited Talks
Distributed Process Calculi with Local States
Maintenance Meets Model Checking-Predictive Maintenance via Fault Trees and Formal Methods
Towards Verifying Neural-Symbolic Multi-Agent Systems
Contents
Software Verification
A Unifying Approach for Control-Flow-Based Loop Abstraction
1 Introduction
2 Preliminaries
3 Loop Abstractions
3.1 Theory
3.2 Combining Strategies for Loop Abstraction
4 Evaluation
4.1 Benchmark Environment
4.2 Experiments
5 Conclusion
References
Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers
1 Introduction
2 Our Proving Process Steps
2.1 Generating and Processing Verification Conditions
2.2 Simplifications and Bounds Derivation
2.3 Eliminating Floating-Point Operations
3 Deriving Provable Error Bounds
4 Verification of Heron's Method for Approximating the Square Root Function
5 Verifying AdaCore's Sine Implementation
6 Benchmarking the Proving Process
6.1 Counter-examples
7 Conclusion
References
Information Exchange Between Over- and Underapproximating Software Analyses
1 Introduction
2 Background
2.1 Program Syntax and Semantics
2.2 Existing Artifacts
3 Validation Artifact GIA
4 Using GIAs in Cooperative Validation
5 Implementation and Evaluation
6 Conclusion
References
Program Analysis
A Query Language for Language Analysis
1 Introduction
2 Languages as Databases
3 The Lang-SQL Query Language
4 Rewriting Lang-n-Check as Lang-SQL Queries
5 Evaluation
6 Related Work
7 Conclusion
References
Field-Sensitive Program Slicing
1 Introduction
2 Slicing Composite Data Structures
3 Constrained-Edges Program Dependence Graph
3.1 Extending the PDG
3.2 Slicing the CE-PDG: Constrained Traversal
3.3 The Slicing Algorithm
3.4 Dealing with Loops
4 Implementation and Empirical Evaluation
5 Related Work
6 Conclusion
References
SPouT: Symbolic Path Recording During Testing
A Concolic Executor for the JVM
1 Introduction
2 SPouT: Directing the Flow of Espresso
2.1 SPouT's Design
2.2 Memory Architecture
2.3 Symbolic Encoding of String Operations
2.4 Supported Languages and Implemented Features
3 Demonstration and Evaluation
4 Conclusion
References
Verifier Technology
Cooperation between Automatic and Interactive Software Verifiers
1 Introduction
2 Preliminaries
2.1 Verification Witnesses
2.2 ACSL
3 A Component Framework for Cooperative Verification
3.1 Witness2ACSL
3.2 ACSL2Witness
3.3 Witness2Assert
4 Evaluation
4.1 Experimental Setup
4.2 Benchmark Set with Useful Witnesses
4.3 Experimental Results
4.4 Case Study on Interactive Verification with Manual Annotations
5 Conclusion
Preface
Organization
Invited Talks
Distributed Process Calculi with Local States
Maintenance Meets Model Checking-Predictive Maintenance via Fault Trees and Formal Methods
Towards Verifying Neural-Symbolic Multi-Agent Systems
Contents
Software Verification
A Unifying Approach for Control-Flow-Based Loop Abstraction
1 Introduction
2 Preliminaries
3 Loop Abstractions
3.1 Theory
3.2 Combining Strategies for Loop Abstraction
4 Evaluation
4.1 Benchmark Environment
4.2 Experiments
5 Conclusion
References
Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers
1 Introduction
2 Our Proving Process Steps
2.1 Generating and Processing Verification Conditions
2.2 Simplifications and Bounds Derivation
2.3 Eliminating Floating-Point Operations
3 Deriving Provable Error Bounds
4 Verification of Heron's Method for Approximating the Square Root Function
5 Verifying AdaCore's Sine Implementation
6 Benchmarking the Proving Process
6.1 Counter-examples
7 Conclusion
References
Information Exchange Between Over- and Underapproximating Software Analyses
1 Introduction
2 Background
2.1 Program Syntax and Semantics
2.2 Existing Artifacts
3 Validation Artifact GIA
4 Using GIAs in Cooperative Validation
5 Implementation and Evaluation
6 Conclusion
References
Program Analysis
A Query Language for Language Analysis
1 Introduction
2 Languages as Databases
3 The Lang-SQL Query Language
4 Rewriting Lang-n-Check as Lang-SQL Queries
5 Evaluation
6 Related Work
7 Conclusion
References
Field-Sensitive Program Slicing
1 Introduction
2 Slicing Composite Data Structures
3 Constrained-Edges Program Dependence Graph
3.1 Extending the PDG
3.2 Slicing the CE-PDG: Constrained Traversal
3.3 The Slicing Algorithm
3.4 Dealing with Loops
4 Implementation and Empirical Evaluation
5 Related Work
6 Conclusion
References
SPouT: Symbolic Path Recording During Testing
A Concolic Executor for the JVM
1 Introduction
2 SPouT: Directing the Flow of Espresso
2.1 SPouT's Design
2.2 Memory Architecture
2.3 Symbolic Encoding of String Operations
2.4 Supported Languages and Implemented Features
3 Demonstration and Evaluation
4 Conclusion
References
Verifier Technology
Cooperation between Automatic and Interactive Software Verifiers
1 Introduction
2 Preliminaries
2.1 Verification Witnesses
2.2 ACSL
3 A Component Framework for Cooperative Verification
3.1 Witness2ACSL
3.2 ACSL2Witness
3.3 Witness2Assert
4 Evaluation
4.1 Experimental Setup
4.2 Benchmark Set with Useful Witnesses
4.3 Experimental Results
4.4 Case Study on Interactive Verification with Manual Annotations
5 Conclusion