Integrated Formal Methods

Name: Integrated Formal Methods | 18th International Conference, IFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings
Brand: Springer
Price: 117.69 EUR
Availability: OnlineOnly

18th International Conference, IFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings

Paula Herber Anton Wijs(Editor)

Springer (Publisher)

Published on 10. November 2023

XIX, 400 pages

E-Book

PDF with digital watermarking

System requirements

978-3-031-47705-8 (ISBN)

€117.69incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Abstract of Invited Talks
Formal Signoff Flows
Industrial Experience with a Verification-Aware Programming Language
Contents
Invited Presentations
SMT: Something You Must Try
1 Introduction
2 Satisfiability Checking
2.1 SAT Solving
2.2 SMT Solving
3 Applications
3.1 A Toy Encoding Example
3.2 Planning with Optimization Modulo Theories
3.3 Reachability Analysis for Hybrid Systems with HyPro
3.4 Parameter Synthesis for Probabilistic Systems
4 Hybrid Petri Nets and Rate Adaption
4.1 Hybrid Petri Nets
4.2 Rate Adaption
4.3 Formulation as an SMT Problem
5 Some Final Remarks
References
Analysis and Verification
Automated Sensitivity Analysis for Probabilistic Loops
1 Introduction
2 Preliminaries
2.1 Syntax and Semantics of Probabilistic Loops
2.2 C-finite Recurrences
2.3 Higher Moment Analysis Using Recurrences
3 Sensitivity Analysis
3.1 Sensitivity Analysis for Admissible Loops
3.2 Sensitivity Analysis for Non-admissible Loops
4 Experiments and Evaluation
5 Related Work
6 Conclusion
References
diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions
1 Introduction
2 Foundations of Difference Verification with Conditions
3 Dependency and Property Aware Difference Detection
4 Evaluation
4.1 Experimental Setup
4.2 Experimental Results
5 Related Work
6 Conclusion
References
CHC Model Validation with Proof Guarantees
1 Introduction
2 Background
2.1 Constrained Horn Clauses
2.2 Related Witness Validation Approaches
3 Validation of CHC Models
4 Implementation
5 Evaluation
5.1 Benchmarks and Tools
5.2 Model Validation Results
5.3 Proof Checking Results
6 Conclusions
References
VerifyThis: Memcached-A Practical Long-Term Challenge for the Integration of Formal Methods
1 Introduction
2 System Description
3 Challenge Goals
4 Participation, Time Schedule, Conclusion
References
Deductive Verification
Towards Formal Verification of a TPM Software Stack
1 Introduction
2 Frama-C Verification Platform
3 The TPM Software Stack and the tpm2-tss Library
4 Dynamic Memory Allocation
5 Memory Management
6 Lemmas
7 Verification Results
8 Related Work
9 Conclusion and Future Work
References
Reasoning About Exceptional Behavior at the Level of Java Bytecode
1 Introduction
2 Motivating Example
3 Specifying and Verifying Exceptional Behavior
3.1 Specifying Exceptional Behavior
3.2 The Vimp Intermediate Representation
3.3 Modeling Exceptional Control Flow
3.4 Transformation Order and Boogie Code Generation
3.5 Implementation Details
4 Experiments
4.1 Programs
4.2 Results
5 Related Work
6 Conclusions
References
Analysis and Formal Specification of OpenJDK's BitSet
1 Introduction
2 The BitSet Class
3 Formal Specification
3.1 Class Invariant
3.2 The wordsToSeq() Model Method
3.3 The get(int,int) Method
4 Issues in BitSet
4.1 A Bug in get(int,int) Caused by a Negative length()
4.2 Bugs Caused by valueOf(...) Corrupting length()
4.3 Solution Directions
5 Towards Formal Verification of the BitSet Class
5.1 Background
5.2 Proof Sketch of get(int,int)
5.3 Required Extensions to KeY
6 Conclusion
References
Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation
1 Introduction
2 Design of the Specification Translator
3 Translating Annotations
3.1 OpenJML
3.2 Krakatoa
3.3 VerCors
4 Evaluation
4.1 Reuse of Specifications
4.2 Reuse of Tools
5 Related Work
6 Conclusion
References
Hardware and Memory Verification
Lifting the Reasoning Level in Generic Weak Memory Verification
1 Introduction
2 Program Syntax
3 Axiomatic Reasoning
3.1 Axioms
3.2 Reasoning Example on Axiom Level
4 Rules
5 Correctness Proof of WRC via Proof Rules
6 Related Work
7 Conclusion
References
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction
1 Introduction
2 Background on Using Positive Equality to Formally Verify Pipelined Processors
3 Efficient Modeling of the RISC-V Architecture at a High Level of Abstraction
3.1 Abstraction of the Register File
3.2 Abstraction of the Decoding Logic
3.3 Abstraction of the CSR Memory Array
3.4 Non-Pipelined Specifications
3.5 Formal Verification of Liveness
3.6 Invariant Constraints Were Not Needed for the Correct Designs, but Were Proved for Debugging the 4-Stage Pipelined Processor
4 Modeling of Spatial Redundancy in Pipelined Processors at a High Level of Abstraction for Formal Verification of Safety
5 Results
6 Conclusion
References
Refinement and Separation: Modular Verification of Wandering Trees
1 Introduction
2 Wandering Trees
3 Structured Specifications of Algebraic Data Types
3.1 Algebraic Definitions
3.2 Modeling the Heap and Separation Logic
4 Modular Software Systems
5 Modularization
5.1 Specification of the Index
5.2 Index Refinement
5.3 Tree Refinement
5.4 Pointer Structures in the Heap and on Flash
6 Verification
6.1 Correctness of the Tree Component
6.2 Correctness of Wandering Trees
6.3 Correctness of Flash Representation
7 Conclusion
References
Verification and Learning
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method
1 Introduction
2 Background
2.1 ProB and the B Method
2.2 Performance Fuzzing
2.3 Thompson Sampling
3 The BanditFuzz Algorithm
4 Adapting BanditFuzz for ProB
4.1 Fuzzing for Classical B Instead of SMT-LIB
4.2 Targeted Fuzzing and Mutating
4.3 Well-Defined ASTs
5 Running the Performance Fuzzer
5.1 Fuzzing only
5.2 Performance Fuzzing Between ProB's Backends
5.3 Performance Fuzzing Between ProB's Settings
5.4 Performance Fuzzing Between the SMT-LIB Translations
6 Related Work
7 Discussion
8 Conclusions
References
Reinforcement Learning Under Partial Observability Guided by Learned Environment Models
1 Introduction
2 Preliminaries
2.1 Models
2.2 Learning MDPs
3 QA-Learning: RL Assisted by Automata Learning
3.1 Overview
3.2 Extended State Space
3.3 Partially Observable Q-Learning
3.4 Convergence
3.5 Generalization and Limitations
4 Evaluation
5 Related Work
6 Conclusion
References
Temporal Logics
Mission-Time LTL (MLTL) Formula Validation via Regular Expressions
1 Introduction
2 Preliminaries: Mission-Time LTL and Bit String Computations
3 MLTL Regular Expressions
4 WEST Algorithm and Analysis
4.1 Proof of Correctness of WEST
4.2 Theoretical Complexity
4.3 Experimental Benchmarking
5 Correctness of WEST Tool Implementation
5.1 Intelligent Fuzzing
6 Regular Expression Simplification Theorem (REST)
6.1 Theoretical Analysis of REST
6.2 Experimental Benchmarking of REST
7 Using WEST: An Example
8 Closing Remarks
8.1 Future Work
References
Symbolic Model Checking of Relative Safety LTL Properties
1 Introduction
2 Motivating Examples
2.1 Bounded Response Example
2.2 Safety Contracts
2.3 LTL G p vs. Invariant
3 Related Work
4 Notation and Preliminary Definitions
4.1 Notation for Sequences, Concatenation and Prefix
4.2 Safety and Relative Safety
4.3 LTL and Safety Fragments
4.4 Symbolic Transition System and Invariant Checking
4.5 Symbolic Techniques Reducing LTL Model Checking to Invariant Checking
5 Symbolic Compilation of Safety LTL
5.1 Symbolic Compilation of Full LTL
5.2 Symbolic Compilation of SafetyLTL
5.3 Symbolic Construction of Live Systems
6 Algorithm
6.1 Simple Algorithm Without Loops
6.2 CEGAR Loop Algorithm
6.3 Extending Algorithm with Lookahead
7 Experimental Evaluation
7.1 Benchmarks
7.2 Experimental Results and Analysis
8 Conclusions and Future Work
References
Extending PlusCal for Modeling Distributed Algorithms
1 Introduction
2 TLA+ and PlusCal
2.1 The Specification Language TLA+
2.2 The Algorithmic Langage PlusCal
2.3 Translating PlusCal to TLA+
3 Distributed PlusCal
3.1 Sub-processes
3.2 Communication Channels
4 Evaluation
4.1 Two Distributed Algorithms Expressed in Distributed PlusCal
4.2 Related Work
5 Conclusion
References
Autonomous Systems
Formal Modelling and Analysis of a Self-Adaptive Robotic System
1 Introduction
2 Case Study: Pipeline Inspection by AUV
3 Modelling the AUV Case Study with ProFeat
3.1 The Feature Model
3.2 The Managed Subsystem
3.3 The Environment
3.4 The Managing Subsystem
4 Analysis
5 Related Work
6 Discussion and Future Work
References
CAN-verify: A Verification Tool For BDI Agents
1 Introduction
2 Can-Overview
3 CAN-verify Components and Features
4 Examples
5 Discussion and Conclusion
References
PhD Symposium Presentations
Scalable and Precise Refinement Types for Imperative Languages
1 Introduction
2 Combining Refinement Type Systems and Deductive Verification
3 Refinement Types for Mutable Objects
3.1 Combining Uniqueness and Refinement Types
3.2 Consistent Updates with Packing Types
3.3 Formalization and Proof Idea
4 Conclusion and Outlook
References
Shuffling Posets on Trajectories
1 Introduction
2 Shuffle on Trajectories
3 Posets
4 Shuffling Posets
5 Future Work
References
A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress)
1 Vision
2 Achieving the Vision
2.1 Robot Programming Environment
2.2 Verification and Analysis Infrastructure
3 (Very Rough Summary of) Related Work
References
Correction to: Integrated Formal Methods
Correction to: P. Herber and A. Wijs (Eds.): Integrated Formal Methods, LNCS 14300, https://doi.org/10.1007/978-3-031-47705-8
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Integrated Formal Methods

Description

More details

Other editions

Additional editions

Content

System requirements