Formal methods and software engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2022, Brisbane, QLD, Australia, November 21-24, 2023 : proceedings

Formal methods and software engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2022, Brisbane, QLD, Australia, November 21-24, 2023 : proceedings / Yi Li, Sofiène Tahar, editors.

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 2124, 2023. The 13 full papers presented together with 8 doctoral symposium papers in this volume were carefully review...

Full description

Saved in:
Bibliographic Details
Corporate Author: International Conference on Formal Engineering Methods Brisbane, Qld.
Other Authors: Li, Yi (Editor), Tahar, Sofiène, 1966- (Editor)
Format: eBook
Language:English
Published: Singapore : Springer, [2023]
Series:Lecture notes in computer science ; 14308.
Subjects:
Formal methods (Computer science) > Congresses.
Software engineering > Congresses.
Formal methods (Computer science)
Software engineering
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
Online Access:Click for online access
Table of Contents:
  • Intro
  • 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

Similar Items