This volume LNCS 14300 constitutes the refereed proceedings of the 18th International Conference, IFM 2023, in November 2023, held in Leiden, The Netherlands. The 16 full papers presented together with 2 short papers were carefully reviewed and selected from 51 submissions. The conference focuses on all aspects of the design of integrated techniques, including language design, verification and validation, automated tool support, and the use of such techniques in software engineering practice.
Author(s): Paula Herber (editor), Anton Wijs (editor)
Series: Lecture Notes in Computer Science; 14300
Publisher: Springer
Year: 2023
Language: English
Pages: 420
Preface
Organization
Abstract of Invited Talks
Formal Signoff Flows • Barbara Jobstmann
Industrial Experience with a Verification-Aware Programming Language • K. Rustan M. Leino
Contents
Invited Presentations
SMT: Something You Must Try • Erika Ábrahám, József Kovács, and Anne Remke
Analysis and Verification
Automated Sensitivity Analysis for Probabilistic Loops • Marcel Moosbrugger, Julian Müllner, and Laura Kovács
DIFFDP: Using Data Dependencies and Properties in Difference Verification with Conditions • Marie-Christine Jakobs and Tim Pollandt
CHC Model Validation with Proof Guarantees • Rodrigo Otoni, Martin Blicha, Patrick Eugster, and Natasha Sharygina
Verify This: Memcached—A Practical Long-Term Challenge for the Integration of Formal Methods • Gidon Ernst and Alexander Weigl
Deductive Verification
Towards Formal Verification of a TPM Software Stack • Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, and Téo Bernier
Reasoning About Exceptional Behavior at the Level of Java Bytecode • Marco Paganoni and Carlo A. Furia
Analysis and Formal Specification of OpenJDK’s BitSet • Andy S. Tatman, Hans-Dieter A. Hiep, and Stijn de Gouw
Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation • Lukas Armborst, Sophie Lathouwers, and Marieke Huisman
Hardware and Memory Verification
Lifting the Reasoning Level in Generic Weak Memory Verification • Lara Bargmann and Heike Wehrheim
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction • Miroslav N. Velev
Refinement and Separation: Modular Verification of Wandering Trees • Gerhard Schellhorn, Stefan Bodenmüller, and Wolfgang Reif
Verification and Learning
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method • Jannik Dunkelau and Michael Leuschel
Reinforcement Learning Under Partial Observability Guided by Learned Environment Models • Edi Muškardin, Martin Tappler, Bernhard K. Aichernig, and Ingo Pill
Temporal Logics
Mission-Time LTL (MLTL) Formula Validation via Regular Expressions • Jenna Elwing, Laura Gamboa-Guzman, Jeremy Sorkin, Chiara Travesset, Zili Wang, and Kristin Yvonne Rozier
Symbolic Model Checking of Relative Safety LTL Properties • Alberto Bombardelli, Alessandro Cimatti, Stefano Tonetta, and Marco Zamboni
Extending PlusCal for Modeling Distributed Algorithms • Horatiu Cirstea and Stephan Merz
Autonomous Systems
Formal Modelling and Analysis of a Self-Adaptive Robotic System • Juliane Päßler, Maurice H. ter Beek, Ferruccio Damiani, Silvia Lizeth Tapia Tarifa, and Einar Broch Johnsen
CAN-VERIFY: A Verification Tool For BDI Agents • Mengwei Xu, Thibault Rivoalen, Blair Archibald, and Michele Sevegnani
PhD Symposium Presentations
Scalable and Precise Refinement Types for Imperative Languages • Florian Lanzinger, Joshua Bachmeier, Mattias Ulbrich, and Werner Dietl
Shuffling Posets on Trajectories • Luc Edixhoven
A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress) • Artur Graczyk, Marialena Hadjikosti, and Andrei Popescu
Correction to: Integrated Formal Methods • Paula Herber and Anton Wijs
Author Index
