• Lidia Losavio, Marco Paganoni and Carlo A. Furia
  Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
• Jorge Blázquez Saborido, Manuel Montenegro and Clara Segura
  Verified Implementation of Associative Containers with Iterators Using Threaded Red-Black Trees
• Reiner Hähnle, Cosimo Laneve and Adele Veschetti
  Formal Verification of Legal Contracts: A Translation-based Approach
• Matthias Grundmann and Hannes Hartenstein
  Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+
• Martin Hána, Nikolai Kosmatov, Virgile Prevosto and Julien Signoles
  Formal Verification of PKCS#1 Signature Parser using Frama-C
• Jean-Christophe Filliatre, Andrei Paskevich and Olivier Danvy
  When Separation Arithmetic is Enough
• Manar Altamimi, Asieh Salehi Fathabadi and Vahid Yazdanpanah
  Formal Modeling of Trust in AI-Driven Autonomous Delivery Vehicles
• Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim
  Model Checking Buffered Durable Linearizability in CSP
• Georgiana Caltais, Andrei Covaci and Hossein Hojjat
  Concurrency Under Control: Systematic Analysis of SDN Race Hazards
• Gabriel Dengler, Sven Apel and Holger Hermanns
  Automata Learning – Expect Delays!
• Konstantin Britikov, Grigory Fedyukovich and Natasha Sharygina
  CHC-Based Reachability Analysis via Cycle Summarization
• David Cortés, Jean Leneutre, Vadim Malvone, James Ortiz and Pierre-Yves Schobbens
  Extending Timed Automata with Clock Derivatives
• Michele Alberti, François Bobot, Julien Girard-Satabin, Alban Grastien, Aymeric Varasse and Zakaria Chihani
  The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification
• Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin and Gianluigi Zavattaro
  Reachability Analysis of Function-as-a-Service Scheduling Policies
• Ion Chirica and Mário Pereira
  Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
• Sophie Rain, Anja Petković Komel, Michael Rawson and Laura Kovács
  Game Modeling of Blockchain Protocols
• Carlos Isasa, Noah Abou El Wafa, Cláudio Gomes, Peter Gorm Larsen and André Platzer
  Safe Temperature Regulation: Formally Verified and Real-World Validated
• Angelo Ferrando, Peng Lu and Vadim Malvone
  Auto-Generating Visual Editors for Formal Logics with Blockly
• Neda Saeedloei and Feliks Kluzniak
  Distributed Timed Scenarios
• Eshita Zaman, Christopher Johannsen, Andrew S Miner, Gianfranco Ciardo and Samik Basu
  CTL Model Checking Partially Specified Systems
• Jonathan Hellwig, Lukas Schäfer, Long Qian, Matthias Althoff and André Platzer
  From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
• Douglas Fraser, Alice Miller, Marco Cook and Dimitrios Pezaros
  Online Model Checking for Anomaly Detection in Industrial Control Systems
• Fletcher Chapin, Ankur Varma, Samuel Akinwande, Meagan Mauter and Sriram Sankaranarayanan
  Using Bayesian Inference and Flowpipe Construction to Bound Predictions of Biogas Production at Wastewater Treatment Plants
• Gidon Ernst and Grigory Fedyukovich
  Quick Theory Exploration for Algebraic Data Types via Program Transformations

Aim

Reproducibility of experiments is crucial to foster an atmosphere of open, reusable and trustworthy research. To improve and reward reproducibility and to give more visibility and credit to the effort of tool developers in our community, authors of accepted papers will be invited to submit possible artifacts associated with their paper for evaluation, and based on the level of reproducibility they will be awarded one or more badges.

The goals of the artifact evaluation are manifold. We want to encourage authors to provide more substantial evidence to their papers and to reward authors who aim for reproducibility of their results, and therefore create artifacts. Also, we want to give more visibility and credit to the effort of tool developers in our community. Furthermore, we want to simplify the independent replication of results presented in the paper and to ease future comparisons with existing approaches.

Objectives and Scope

In the last decades, we have witnessed a proliferation of approaches that integrate several modelling, verification and simulation techniques, facilitating more versatile and efficient analysis of software-intensive systems. These approaches provide powerful support for the analysis of different functional and non-functional properties of the systems, complex interaction of components of different nature as well as validation of diverse aspects of system behaviour. The iFM conference series is a forum for discussing recent research advances in the development of integrated approaches to formal modelling and analysis. The conference covers 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. To credit the effort of tool developers, we use EAPLS artifact badging.