PPaperPicks
← All conferences
Editions20262024

FM 2026

A

International Symposium on Formal Methods

Official site ↗
70
accepted papers
255
authors
May 18-22, 2026
dates
Japan
location

70 / 70 papers

  1. 1
    A Formal Framework for Predicting Distributed System Performance Under Faults
    Ziwei Zhou
    ,
    Si Liu
    ,
    Zhou Zhou
    ,
    Peixin Wang
    ,
    Min Zhang
  2. 2
    A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures
    Wolfram Pfeifer
    ,
    Werner Dietl
    ,
    Mattias Ulbrich
  3. 3
    A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
    Jiawei Chen
    ,
    José Luiz Vargas de Mendonça
    ,
    Konstantinos Mamouras
    ,
    Jean-Baptiste Jeannin
  4. 4
    A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning
    Zhiheng Cai
    ,
    Zhihang Sun
    ,
    Fei He
  5. 5
    Accelerating Kind Realizability: A Multi-stage Incremental Realizability Checking Framework
    Sirui Liu
    ,
    Wei Dong
  6. 6
    Active Automata Learning with Noisy Data: From Big to Small Data
    Felix Wallner
    ,
    Bernhard K. Aichernig
    ,
    Benjamin von Berg
    ,
    Maximilian Rindler
  7. 7
    Array-Carrying Symbolic Execution for Function Contract Generation
    Weijie Lu
    ,
    Jingyu Ke
    ,
    Hongfei Fu
    ,
    Zhouyue Sun
    ,
    Yi Zhou
    ,
    Guoqiang Li
    ,
    Haokun Li
  8. 8
    Asynchronous Team Automata
    Davide Basile
    ,
    Maurice H. ter Beek
    ,
    José Proença
  9. 9
    Automated LTL Specification Generation from Industrial Aerospace Requirements
    Zhi Ma
    ,
    Xiao Liang
    ,
    Cheng Wen
    ,
    Rui Chen
    ,
    Bin Gu
    ,
    Shengchao Qin
    ,
    Cong Tian
    ,
    Mengfei Yang
  10. 10
    Automatic Memory Management for Dataflows
    Michael Lienhardt
  11. 11
    BDD-Based Deadlock Avoidance for Automated Guided Vehicles in Warehouse Logistics (Case Study Paper)
    Benjamin von Berg
    ,
    Bernhard K. Aichernig
    ,
    Fabian Wedenik
  12. 12
    Can LLM Aid in Solving Constraints with Inductive Definitions?
    Weizhi Feng
    ,
    Shidong Shen
    ,
    Jiaxiang Liu
    ,
    Taolue Chen
    ,
    Fu Song
    ,
    Zhilin Wu
  13. 13
    Certifying Constraints in Hardware Model Checking
    Nils Froleyks
    ,
    Emily Yu
    ,
    Armin Biere
    ,
    Keijo Heljanko
  14. 14
    Complexity of Consistency Testing for the Release-Acquire Semantics
    R. Govind
    ,
    S. Krishna
    ,
    Sanchari Sil
    ,
    B. Srivathsan
  15. 15
    ConFixer: Robustness Semantics Based Configuration Bug Fixing for Automated Driving Systems
    Xiaodong Zhang
    ,
    Songyang Yan
    ,
    Zijiang Yang
  16. 16
    Correct-by-Construction Dynamic Reachability: A Galois-Connected Approach to Bidirected Dyck Languages
    Xiaofei Zhao
  17. 17
    Differential Verification of Information Flow in SEAndroid Policies
    Lorenzo Ceragioli
    ,
    Letterio Galletta
    ,
    Edoardo Lunati
  18. 18
    Digital Twins: a Briefing for Formalists
    John S. Fitzgerald
    ,
    Cláudio Gomes
    ,
    Peter Gorm Larsen
    ,
    Mikkel Schmidt Andersen
    ,
    Santiago Gil
    ,
    Morten Haahr Kristensen
  19. 19
    Distributed Runtime Verification in Proximity-Based Networks: A Tutorial on the Aggregate Programming Approach
    Giorgio Audrito
    ,
    Ferruccio Damiani
    ,
    Giordano Scarso
    ,
    Volker Stolz
    ,
    Gianluca Torta
  20. 20
    Efficient Multi-level Mine Dewatering Using Uppaal Stratego
    Muhammad Naeem
    ,
    Cristina Seceleanu
    ,
    Alf J. Isaksson
    ,
    Tiberiu Seceleanu
  21. 21
    Error-Awareness Accelerates Active Automata Learning
    Loes Kruger
    ,
    Sebastian Junges
    ,
    Jurriaan Rot
  22. 22
    EUF-based Solving Dyck-Reachability with Applications to Static Analysis
    Yide Du
    ,
    Zhenbang Chen
    ,
    Kunlin Liu
    ,
    Guofeng Zhang
    ,
    Xudong Wang
    ,
    Ke Ma
    ,
    Wei Dong
    ,
    Ji Wang
  23. 23
    Exact Moment Estimation of Stochastic Differential Dynamics
    Shenghua Feng
    ,
    Jie An
    ,
    Naijun Zhan
    ,
    Fanjiang Xu
  24. 24
    Exact Verification of Graph Neural Networks with Incremental Constraint Solving
    Minghao Liu
    ,
    Chia-Hsuan Lu
    ,
    Marta Kwiatkowska
  25. 25
    Fast SMT-Based Fault Tolerance Verification for Wide Area Networks
    Ning Kang
    ,
    Peng Zhang
    ,
    Hao Li
    ,
    Jianyuan Zhang
  26. 26
    FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
    Xindi Zhang
    ,
    Furong Ye
    ,
    Zhihan Chen
    ,
    Shaowei Cai
  27. 27
    Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22, 2026, Proceedings, Part I
    Augusto Sampaio
    ,
    Mariëlle Stoelinga
  28. 28
    Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22, 2026, Proceedings, Part II
    Augusto Sampaio
    ,
    Mariëlle Stoelinga
  29. 29
    Formal Reasoning About Confidence and Automated Verification of Neural Networks
    Mohammad Afzal
    ,
    S. Akshay
    ,
    Blaise Genest
    ,
    Ashutosh Gupta
  30. 30
    Formal Verification for Security Certification: From a First Success to Sustainable Industrial Usage
    Adel Djoudi
    ,
    Nikolai Kosmatov
  31. 31
    Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
    Tianqi Zhao
    ,
    Qinxiang Cao
    ,
    Shenghua Feng
    ,
    Minghui Zhou
    ,
    Naijun Zhan
    ,
    Yongzhi Cao
    ,
    Junfeng Zhao
    ,
    Haiyan Zhao
    ,
    Hao Wang
    ,
    Zhenjiang Hu
  32. 32
    Formally Explaining Neural Network Classification
    Tomás Kolárik
    ,
    Grigory Fedyukovich
    ,
    Faezeh Labbaf
    ,
    Fabrizio Leopardi
    ,
    Natasha Sharygina
    ,
    Michael Wand
  33. 33
    From Execution to Necessity: Proof-Based Metrics for Code Coverage (Short Paper)
    Karl Mattsson
    ,
    Peter Backeman
  34. 34
    Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
    James Tobler
    ,
    Graeme Smith
  35. 35
    Highly Incremental: A Simple Programmatic Approach for Many Objectives
    Philipp Schröer
    ,
    Joost-Pieter Katoen
  36. 36
    History-Constrained Systems
    Louwe B. Kuijer
    ,
    David Purser
    ,
    Henry Sinclair-Banks
    ,
    Patrick Totzke
  37. 37
    Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
    Radu Florin Tulcan
    ,
    Rose Bohrer
    ,
    Yoàv Montacute
    ,
    Kevin Zhou
    ,
    Yusuke Kawamoto
    ,
    Ichiro Hasuo
  38. 38
    Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
    Niuniu Qi
    ,
    Hanrui Zhao
    ,
    Zhengfeng Yang
    ,
    Xia Zeng
    ,
    Mengxin Ren
    ,
    Chao Peng
    ,
    Zhiming Liu
  39. 39
    Maximum Realizability for LTL Modulo Theories
    Andoni Rodríguez
    ,
    César Sánchez
  40. 40
    Mining Verdict Boundaries for Neural Network Verification
    Jiawei Ren
    ,
    Guanqin Zhang
    ,
    Zhenya Zhang
    ,
    Yulei Sui
  41. 41
    Mixed Flow-Sensitive Static Analysis: Engineering Modularity
    Helmut Seidl
    ,
    Vesal Vojdani
    ,
    Julian Erhard
    ,
    Michael Schwarz
  42. 42
    ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair (Short Tool Paper)
    Zhiyong Chen
    ,
    Jialun Cao
    ,
    Chang Xu
    ,
    Shing-Chi Cheung
  43. 43
    Pacing Types for Asynchronous Stream Equations
    Florian Kohn
    ,
    Arthur Correnson
    ,
    Jan Baumeister
    ,
    Bernd Finkbeiner
  44. 44
    Performance Heuristics for GR(1) Unrealizable Core Computation
    Shachaf Cohen
    ,
    Shahar Maoz
  45. 45
    Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness (Long Tool Paper)
    Aron Ricardo Perez-Lopez
    ,
    Po-Chun Chien
    ,
    Florian Lonsing
    ,
    Samantha Archer
    ,
    Ahmed Irfan
    ,
    Clark W. Barrett
  46. 46
    Pragmatic Uses of AI in Formal Methods-Based Railway Projects: Early Lessons and Perspectives (Extended Abstract)
    Thierry Lecomte
    ,
    Dalay Almeida
    ,
    Norman Maury
  47. 47
    Probabilistic Model Checking Taken by Storm - A Tutorial on the Probabilistic Model Checker Storm
    Matthias Volk
    ,
    Linus Heck
    ,
    Sebastian Junges
    ,
    Joost-Pieter Katoen
    ,
    Tim Quatmann
  48. 48
    QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits (Long Tool Paper)
    Zihao Li
    ,
    Ji Guan
    ,
    Mingsheng Ying
  49. 49
    Quantitative Monitoring of Signal First-Order Logic
    Marek Chalupa
    ,
    Thomas A. Henzinger
    ,
    N. Ege Saraç
    ,
    Emily Yu
  50. 50
    Reachability-Guided Abstraction Refinement
    Pierre Ganty
    ,
    Nicolas Manini
    ,
    Francesco Ranzato