Formal Methods and Software Engineering: 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November ... (Lecture Notes in Computer Science)

✍ Scribed by Yi Li (editor), Sofiène Tahar (editor)

• Publisher: Springer
• Year: 2023
• Tongue: English
• Leaves: 320
• Category: Library

✦ Synopsis

This book constitutes the proceedings of the 24th International Conference on Formal Methods and Software Engineering, ICFEM 2023, held in Brisbane, QLD, Australia, during November 21–24, 2023.

The 13 full papers presented together with 8 doctoral symposium papers in this volume were carefully reviewed and selected from 34 submissions, the volume also contains one invited paper. The conference focuses on applying formal methods to practical applications and presents papers for research in all areas related to formal engineering methods.

✦ Table of Contents

Preface
Organization
Abstracts of Invited Talks
Compositional Reasoning at The Software/Hardware Interface
Separation of Concerns for Complexity Mitigation in System and Domain Formal Modelling – A Dive into Algebraic Event-B Theories
A Foundation for Interaction
Practical Verified Concurrent Program Security
On Analysing Weak Memory Concurrency
Certified Proof and Non-Provability
Verifying Compiler Optimisations
Contents
Invited Paper
Verifying Compiler Optimisations
1 Introduction
2 Data-Flow Sub-graphs
3 Term Rewriting Rules
4 Verifying Term Rewriting Rules
5 Generating Code for Optimisations
6 Conclusions
References
Regular Papers
An Idealist's Approach for Smart Contract Correctness
1 Introduction
2 Overview
2.1 Smart Contracts
2.2 Vulnerability and Correctness
2.3 An Illustrative Example
3 Specification Language
3.1 High-Level Overview
3.2 Formalization
4 Verification
4.1 Function Validation
4.2 Generating Proof Obligations
5 Implementation and Evaluation
5.1 Implementation
5.2 Experimental Evaluation
6 Related Work and Conclusion
References
Active Inference of EFSMs Without Reset
1 Introduction
2 Background and Related Work
2.1 Running Example
2.2 Related Work
2.3 Definitions
2.4 Inferring Functions with Genetic Programming
3 The ehW-Inference Algorithm
3.1 Assumptions
3.2 Homing and Characterizing
3.3 Inputs and Data Structures
3.4 ehW-Inference Backbone
3.5 Generalisation
3.6 Oracle Procedure
4 Inferring a Vending Machine Controller
5 Conclusions and Future Work
References
Learning Mealy Machines with Local Timers
1 Introduction
2 Related Work
3 Preliminaries
3.1 Mealy Machines
3.2 The Rivest-Schapire Algorithm
4 Mealy Machines with Local Timers
4.1 Syntax and Semantics
4.2 Expanded Forms and Equivalence
5 Learning MMLTs Efficiently
5.1 Timer Queries
5.2 Timed Counterexample Analysis
5.3 Hypothesis Refinement
5.4 Hypothesis Completion
5.5 Output Query Complexity
6 Practical Evaluation
7 Conclusion and Future Work
References
Compositional Vulnerability Detection with Insecurity Separation Logic
1 Introduction
2 Motivation
3 Attacker Model
4 Insecurity Separation Logic (InsecSL)
5 Symbolic Execution
6 Implementation
7 Evaluation
8 Related Work and Conclusion
References
Dynamic Extrapolation in Extended Timed Automata
1 Introduction
2 Preliminary
2.1 Extended Timed Automata
2.2 Symbolic Semantics
2.3 M-Extrapolation in XTA
3 Dynamic Extrapolation
3.1 Reducing Relevant Paths
3.2 Dynamic LU-Extrapolation
3.3 A Note on Timed Automata Networks
4 Experiments and Results
5 Conclusion
References
Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models
1 Introduction
2 Related Work
2.1 Adversarial Manipulations in NLP Tasks
2.2 Robustness of Neural Networks
3 Formalization
3.1 Formalizing Perturbations to General Inputs
3.2 Formalizing Language Models
3.3 Character-Level Perturbation
4 Experiments
4.1 Experiment Setup
4.2 Evaluation
5 Discussion
6 Conclusion
References
Trace Models of Concurrent Valuation Algebras
1 Introduction
2 Ordered Valuation Algebras
2.1 Extension of Local Operators
3 Concurrent Valuation Algebras
3.1 Reasoning in a CVA
4 Tuple Systems
5 Action Trace Model
5.1 Interleaving Product
5.2 Concatenating Product
6 State Trace Model
6.1 Gluing Product
6.2 Strong Morphisms Between and
7 Relative State Trace Model
7.1 Colax Morphism from to rel
8 Local Computation
9 Conclusion
References
Branch and Bound for Sigmoid-Like Neural Network Verification
1 Introduction
2 Preliminaries
2.1 Neural Networks
2.2 Robustness Property
2.3 Linear Relaxation of Sigmoid-Like Functions
3 Branch and Bound for Sigmoid-Like Neural Networks
4 Neuron Splitting
5 Branching Strategy
6 Experiments
6.1 Experimental Setup
6.2 Experimental Results
6.3 Experiments on Branching Strategy
7 Conclusion
References
Certifying Sequential Consistency of Machine Learning Accelerators
1 Introduction
2 Background
2.1 Control Data Flow Graph
2.2 Versatile Tensor Accelerator
2.3 NVIDIA Deep Learning Accelerator
3 Formalization
4 Proof Sketch
5 Case Studies
5.1 Case Study 1: VTA
5.2 Case Study 2: NVDLA
6 Related Work
7 Conclusions and Future Work
References
Guided Integration of Formal Verification in Assurance Cases
1 Introduction
2 Background
2.1 AdvoCATE
3 Tool-Supported Methodology for Integration of Formal Verification in Assurance Cases
3.1 Methodology
3.2 Tool Support in AdvoCATE
4 Application Examples
4.1 Application Example 1: Venus for Object Detection
4.2 Application Example 2: VerifAI for NN Testing
5 Conclusions
References
Validation-Driven Development
1 Introduction
2 Background
2.1 Event-B
2.2 Validation Obligations
3 Validation-Driven Development
3.1 Workflow
3.2 Specification Structuring and Refinement
4 Case Study
4.1 System Description
4.2 Problem Structuring
4.3 Specification and Validation
5 Related Work
5.1 BDD Usage in Formal Requirement Specification
5.2 Bridging the Gap Between Natural Language Requirements and Formal Specification
5.3 Requirements Tracing
6 Conclusion and Future Work
References
Incremental Property Directed Reachability
1 Introduction
2 Preliminaries
3 Incremental Property Directed Reachability
3.1 Extending PDR with an Internal State
3.2 Incremental Property Directed Reachability (IPDR)
4 Related Work
5 Implementation and Experimental Evaluation
6 Conclusions
References
Proving Local Invariants in ASTDs
1 Introduction and Related Work
2 Overview of the ASTD Notation
2.1 Automaton
2.2 Kleene Closure
2.3 Sequence
2.4 Guard
3 Proof Obligations for Invariant Satisfaction
3.1 Definitions
3.2 Proof Obligation Generation
3.3 Proof Obligations for Initialisations
3.4 Proof Obligations for Local Transitions
3.5 Proving Proof Obligations and Strengthening Invariants
4 Conclusion
References
Doctoral Symposium Papers
Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol
1 Introduction
2 An Overview of the Burn-to-Claim Protocol
3 Specifications of the Protocol
4 The Model for Cross-Blockchain Interactions
5 System Verification
5.1 Discussion
6 Conclusion and Future Works
References
Early and Systematic Validation of Formal Models
1 Introduction
2 Background
3 Challenges
3.1 Structuring the Validation Workflow
3.2 Validation and Refinement
3.3 Creating the VDD Framework
4 Results and Planned Contributions
5 Conclusion and Future Work
References
Verifying Neural Networks by Approximating Convex Hulls
1 Introduction
2 Related Work
2.1 Complete and Incomplete Approaches
2.2 Single-Neuron and Multi-neuron Constraints
3 Methodology
3.1 Formalization of Neural Network
3.2 Approximation of Neural Network
4 Approach
5 Evaluation
6 Discussion and Conclusion
6.1 Discussion
6.2 Conclusion
References
Eager to Stop: Efficient Falsification of Deep Neural Networks
1 Introduction
2 Problem Statement and Related Work
3 Proposed Solution
4 Conclusion and Future Work
References
A Runtime Verification Framework for Cyber-Physical Systems Based on Data Analytics and LTL Formula Learning
1 Introduction
2 The Proposed Approach
3 Case Study: Water Distribution System
4 Conclusion
References
Unified Verification of Neural Networks' Robustness and Privacy in Computer Vision
1 Introduction
2 Preliminaries and Problem Statement
2.1 Robustness Verification
2.2 Privacy-Preserved Utility Task
3 Proposed Solutions and Future Work
References
IoT Software Vulnerability Detection Techniques through Large Language Model
1 Introduction
2 Literature Review
2.1 Large Language Model
2.2 Prompt Engineering
2.3 Challenges
3 Proposed Approach
4 Current Work
4.1 Experiments
4.2 Results and Analysis
5 Future Work
5.1 Dataset and Experiments
5.2 Prompt Engineering
6 Conclusion
References
Vulnerability Detection via Typestate-Guided Code Representation Learning
1 Introduction
2 Related Work
3 TSVD Approach
3.1 Typestate Sequence Generation
3.2 Contrastive Typestate Sequence Embedding
3.3 Typestate Sequence Selection
3.4 Detection Model Training
4 Evaluation
5 Conclusion and Future Work
References
Correction to: Learning Mealy Machines with Local Timers
Correction to: Chapter 4 in: Y. Li and S. Tahar (Eds.): Formal Methods and Software Engineering, LNCS 14308, https://doi.org/10.1007/978-981-99-7584-6_4
Author Index