Days: Monday, September 9th Tuesday, September 10th Wednesday, September 11th Thursday, September 12th Friday, September 13th
View this program: with abstractssession overviewtalk overview
| 09:00 | The Pyramid Of (Formal) Software Verification (abstract) |
| 09:00 | Advancing Quantum Computing with Formal Methods (abstract) |
| 09:00 | Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testin (abstract) |
See PAVeTrust program (pavetrust.github.io/program/) for further details.
See CPA program (cpa.sosy-lab.org/2024/program.html) for further details.
See LOPSTR program (lopstr.github.io/2024) for further details.
See FMICS program (fmics.inria.fr/2024/) for further details.
See FACS program (facs-conference.github.io/2024/program/) for further details.
| 11:00 | No risk, no fun: a tutorial on risk management (abstract) |
See TAP program (tapconference.github.io/2024/program.html) for further details.
See PAVeTrust program (pavetrust.github.io/program/) for further details.
See CPA program (cpa.sosy-lab.org/2024/program.html) for further details.
| 14:00 | Runtime Verification in Real-Time with the Copilot Language: A Tutorial (abstract) |
| 14:00 | ASMETA tool set for rigorous system design (abstract) |
| 14:00 | Practical Deductive Verification of OCaml Programs (abstract) |
| 14:00 | Formalising Requirements for Systems Verification (abstract) |
See PAVeTrust program (pavetrust.github.io/program/) for further details.
See CPA program (cpa.sosy-lab.org/2024/program.html) for further details.
See LOPSTR program (lopstr.github.io/2024) for further details.
See FMICS program (fmics.inria.fr/2024/) for further details.
See FACS program (facs-conference.github.io/2024/program/) for further details.
See TAP program (tapconference.github.io/2024/program.html) for further details.
See PAVeTrust program (pavetrust.github.io/program/) for further details.
See CPA program (cpa.sosy-lab.org/2024/program.html) for further details.
View this program: with abstractssession overviewtalk overview
| 09:00 | Software Verification with CPAchecker 3.0: Tutorial and User Guide (abstract) |
| 09:00 | Satisfiability Modulo Theories: A Beginner's Tutorial (abstract) |
See Doctoral Symposium program (www.easychair.org/smart-program/FM24/ProgramDS.html) for further details.
| 09:00 | On Time and Space (Of Humans) |
| 09:00 | Safe and Easy Compile-Time Generative Programming (abstract) |
See FMTea website (fmtea.github.io) for further details.
See TLA+ CE program (conf.tlapl.us/2024-fm/) for further details.
See Overture website (www.overturetool.org/workshops/22nd-overture-workshop.html) for further details.
See LOPSTR program (lopstr.github.io/2024) for further details.
See FMICS program (fmics.inria.fr/2024/) for further details.
See FACS program (facs-conference.github.io/2024/program/) for further details.
See TLA+ CE program (conf.tlapl.us/2024-fm/) for further details.
See Doctoral Symposium program (www.easychair.org/smart-program/FM24/ProgramDS.html) for further details.
See TAP program (tapconference.github.io/2024/program.html) for further details.
See PPDP program (ppdp2024.github.io) for further details.
See FMTea website (fmtea.github.io) for further details.
See Overture website (www.overturetool.org/workshops/22nd-overture-workshop.html) for further details.
| 14:00 | A Tutorial on Stream-based Monitoring (abstract) |
| 14:00 | The Java Verification Tool KeY: A Tutorial (abstract) |
See Doctoral Symposium program (www.easychair.org/smart-program/FM24/ProgramDS.html) for further details.
| 14:00 | B+ or how to model system properties in a formal software model (abstract) |
See PPDP program (ppdp2024.github.io) for further details.
See FMTea website (fmtea.github.io) for further details.
See LOPSTR program (lopstr.github.io/2024) for further details.
See FMICS program (fmics.inria.fr/2024/) for further details.
See FACS program (facs-conference.github.io/2024/program/) for further details.
See TLA+ CE program (conf.tlapl.us/2024-fm/) for further details.
See Doctoral Symposium program (www.easychair.org/smart-program/FM24/ProgramDS.html) for further details.
| 16:00 | Thoughts on the interplay between corporate, government, and university R&D |
See TAP program (tapconference.github.io/2024/program.html) for further details.
See PPDP program (ppdp2024.github.io) for further details.
See FMTea website (fmtea.github.io) for further details.
See Overture website (www.overturetool.org/workshops/22nd-overture-workshop.html) for further details.
The reception buffet will be held in the courtyard of Building 3 of Politecnico di Milano:
View this program: with abstractssession overviewtalk overview
| 09:00 | FM24 Opening |
| 09:20 | Adversarial Robustness Certification for Bayesian Neural Networks |
See PPDP program (ppdp2024.github.io) for further details.
| 10:50 | Free Facts: An Alternative to Inefficient Axioms in Dafny (abstract) |
| 11:10 | Understanding Synthesized Reactive Systems Through Invariants (abstract) |
| 11:30 | Efficient Formally Verified Maximal End Component Decomposition for MDPs (abstract) |
| 11:50 | Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (abstract) |
| 12:10 | The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems (abstract) |
| 10:50 | Partially Observable Stochastic Games with Neural Perception Mechanisms (abstract) |
| 11:10 | VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models (abstract) |
| 11:30 | Bridging Dimensions: Confident Reachability for High-Dimensional Controllers (abstract) |
| 11:50 | Certified Quantization Strategy Synthesis for Neural Networks (abstract) |
| 12:10 | A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks (abstract) |
See FMICS program (fmics.inria.fr/2024/) for further details.
See PPDP program (ppdp2024.github.io) for further details.
| 14:00 | The Business of Proof |
| 15:00 | Industry partner pitches |
See PPDP program (ppdp2024.github.io) for further details.
| 15:50 | Integrating Loop Acceleration into Bounded Model Checking (abstract) |
| 16:10 | A Local Search Algorithm for MaxSMT(LIA) (abstract) |
| 16:30 | B2SAT: A Bare-Metal Reduction of B to SAT (abstract) |
| 16:50 | Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic (abstract) |
| 17:10 | A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic (abstract) |
| 17:30 | Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets (abstract) |
| 15:50 | Code-level Safety Verification for Automated Driving: A Case Study (abstract) |
| 16:10 | AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models (abstract) |
| 16:30 | UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking (abstract) |
| 16:50 | Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT) (abstract) |
| 17:10 | Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design (abstract) |
| 17:30 | Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning (abstract) |
See PPDP program (ppdp2024.github.io) for further details.
View this program: with abstractssession overviewtalk overview
| 09:00 | Getting Chip Card Payments Right |
| 10:00 | Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems (Journal first) (abstract)  |
| 10:50 | State Matching and Multiple References in Adaptive Active Automata Learning (abstract) |
| 11:10 | DFAMiner: Mining minimal separating DFAs from labelled samples (abstract) |
| 11:30 | Automated Repair of Information Flow Security in Android Implicit Inter-App Communication (abstract) |
| 11:50 | Learning Branching-Time Properties in CTL and ATL via Constraint Solving (abstract) |
| 12:10 | Alloy repair hint generation based on historical data (abstract) |
| 10:50 | Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic (abstract) |
| 11:10 | Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs (abstract) |
| 11:30 | PyBDR: Set-boundary based Reachability Analysis Toolkit in Python (abstract) |
| 11:50 | CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases (abstract) |
| 12:10 | The Opacity of Timed Automata (abstract) |
| 14:00 | FME Fellowship Award |
| 15:00 | Extending rely-guarantee thinking to handle real-time scheduling (Journal first) (abstract) PRESENTER: Cliff Jones |
Milan by historic tram.
Rendezvous at:
Piazza Castello, at the corner with via Beltrami
Click here for the position in Google Maps
The dinner will be held at:
Liberty Ballroom at Osteria del Treno
Via San Gregorio, 46 - 20124 Milano
Click here for the position in Google Maps
View this program: with abstractssession overviewtalk overview
| 09:00 | Formal Methods for Robotics and Human-Robot Interaction |
| 10:00 | RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first) (abstract) PRESENTER: James Baxter |
| 10:50 | Extending Isabelle/HOL’s Code Generator with support for the Go programming language (abstract) |
| 11:10 | Proving Functional Program Equivalence via Directed Lemma Synthesis (abstract) |
| 11:30 | Staged Specification Logic for Verifying Higher-Order Imperative Programs (abstract) |
| 11:50 | Chamelon : a delta-debugger for OCaml (abstract) |
| 12:10 | Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last (abstract) |
| 10:50 | CauMon: An Informative Online Monitor for Signal Temporal Logic (abstract) |
| 11:10 | Switching Controller Synthesis for Hybrid Systems Against STL Formulas (abstract) |
| 11:30 | On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains (abstract) |
| 11:50 | Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems (abstract) |
| 12:10 | Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems (abstract) |
| 14:00 | Reachability Analysis for Multiloop Programs Using Transition Power Abstraction (abstract) |
| 14:20 | Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0 (abstract) |
| 14:40 | Accurate Static Data Race Detection for C (abstract) |
| 15:00 | Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption (abstract) |
| 14:00 | Compositional Verification of Cryptographic Circuits against Fault Injection Attacks (abstract) |
| 14:20 | FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First) (abstract) PRESENTER: Yuan Fei |
| 14:40 | Fast Attack Graph Defense Localization via Bisimulation (abstract) |
| 15:00 | Detecting speculative execution vulnerabilities on weak memory models (abstract) |
| 15:50 | Unifying Weak Memory Verification using Potentials (abstract) |
| 16:10 | Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata (abstract) |
| 16:30 | Automated Static Analysis of Quality of Service Properties of Communicating Systems (abstract) |
| 15:50 | Stochastic Games for User Journeys (abstract) |
| 16:10 | Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows (abstract) |
| 16:30 | fm-weck: Containerized Execution of Formal Methods Tools (abstract) |
| 16:50 | HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification (abstract) |