iFM 2023

18th International Conference on integrated Formal Methods 13-15 November 2023, Leiden, the Netherlands

Free Stock photos by Vecteezy

Program

13 November 2023	Main conference	Theater room, Scheltema Leiden
14 November 2023	Main conference	Theater room, Scheltema Leiden
15 November 2023	Main conference	Theater room, Scheltema Leiden
15-16 November 2023	FMAS 2023 workshop	Theater room and Expo room,Scheltema Leiden
16 November 2023	PhD symposium	Ketelhuis room, Scheltema Leiden

iFM 2023 program (last updated: 2 October 2023)

Monday 13 November 20023 (Theater room, Scheltema Leiden)

8:30 – 8:45	Registration
8:45 – 9:00	Opening(Marcello Bonsangue, general chair iFM 2023)
9:00 – 10:00	Keynote presentation (chair: Marcello Bonsangue) Formal Signoff Flows Barbara Jobstmann (EPFL and Cadence Design Systems, CH)
10:00 – 10:30	Coffee/Tea break
10:30 – 12:00	Session 1: Analysis and Verification (chair: t.b.a.) 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
12:00 – 14:00	Lunch break
14:00 – 15:00	Session 2: Deductive Verification I (chair: t.b.a.) Towards Formal Verification of a TPM Software Stack Yani Ziani, Nikolai Kosmatov, Frederic Loulergue, Daniel Gracia Perez and Téo Bernier Reasoning About Exceptional Behavior At the Level of Java Bytecode Marco Paganoni and Carlo A. Furia
15:00 – 15:30	Coffee/Tea break
15:30 – 17:00	Session 3: Artifacts and Posters (chair: t.b.a.)
17:00 – 19:30	Reception (Ketelhuis and Foyer, Scheltema Leiden)

Tuesday 14 November 20023 (Theater room, Scheltema Leiden)

9:00 – 10:00	Keynote presentation (chair: Anton Wijs) Industrial experience with a verification-aware programming language Rustan Leino (Amazon Web Services, US)
10:00 – 10:30	Coffee/Tea break
10:30 – 12:00	Session 4: Hardware and Memory Verification (chair: t.b.a.) 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 Velev Refinement and Separation: Modular Verification of Wandering Trees Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif
12:00 – 14:00	Lunch break
14:00 – 15:00	Session 5: Deductive Verification II (chair: t.b.a.) Analysis and Formal Specification of OpenJDK’s BitSet Andy S. Tatman, Hans-Dieter Hiep and Stijn De Gouw Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation Lukas Armborst, Sophie Lathouwers and Marieke Huisman/u>
15:00 – 15:30	Coffee/Tea break
15:30 – 17:00	Session 6: Verify This (chairs: Gidon Ernst and Alexander Weigl) Memcached—A Practical Long-term Challenge for the Integration of Formal Methods
17:00 – 22:00	Social event and dinner (t.b.a.)

Wednesday 15 November 20023 (Theater room, Scheltema Leiden)

9:00 – 10:00	Session 7: Verification and Learning (chair: t.b.a.) 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 Muskardin, Martin Tappler, Ingo Pill and Bernhard K. Aichernig
10:00 – 10:30	Coffee/Tea break
10:30 – 12:00	Session 8: Temporal Logics (chair: t.b.a.) Mission-time LTL (MLTL) Formula Validation Via Regular Expressions Zili Wang, Chiara Travesset, Jeremy Sorkin, Jenna Elwing, Laura P. Gamboa Guzman 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 (TLA+) Horatiu Cirstea and Stephan Merz
12:00 – 14:00	Lunch break
14:00 – 15:00	Joint iFM/FMAS keynote presentation (chair: t.b.a.) SMT: Something you Must Try Erika Ábrahám (RWTH Aachen University, DE)
15:00 – 15:30	Coffee/Tea break
15:30 – 17:00	Joint iFM/FMAS Session: Autonomous Systems (chair: t.b.a.) AFormal 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: Verification Tool for BDI Agents Mengwei Xu, Thibault Rivoalen, Blair Archibald and Michele Sevegnani t.b.a.