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)
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)
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.)
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.