FM 2026 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (579)

A Thomas A. HenzingerA. Henzinger, Thomas Institute of Science and Technology Austria (ISTA)Austria Quantitative Monitoring of Signal First-Order Logic
Tim A.C. WillemseA.C. Willemse, Tim Eindhoven University of Technology Committee Member in Tutorial Track Committee within the FM Tutorials-track
Erika AbrahamAbraham, Erika RWTH Aachen UniversityGermany Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track
Mohammad AfzalAfzal, Mohammad TCS Research Pune and IIT Bombay IndiaIndia Formal Reasoning About Confidence and Automated Verification of Neural Networks Formal Reasoning About Confidence and Automated Verification of Neural Networks
Wolfgang AhrendtAhrendt, Wolfgang Chalmers University of TechnologySweden Committee Member in Program Committee within the FM Research Track-track
Bernhard AichernigAichernig, Bernhard Johannes Kepler University LinzAustria Session Chair of TAP Session 1: Formal Languages, Reachability, and Program Verification (part of FM TAP Track)
Bernhard AichernigAichernig, Bernhard Johannes Kepler University, LinzAustria Active Automata Learning with Noisy Data: From Big to Small Data BDD-based Deadlock Prevention for Automated Guided Vehicles in Warehouse Logistics Committee Member in Program Committee within the FM Research Track-track
Yamine Ait AmeurAit Ameur, Yamine IRIT/INPT-ENSEEIHTFrance Session Chair of ABZ Gedenkschrift for Jean-Raymond Abrial (part of FM ABZ) Encoding BDI Syntax with Theories in Event-B
S. AkshayAkshay, S. Indian Institute of Technology, Bombay, IndiaIndia Formal Reasoning About Confidence and Automated Verification of Neural Networks Formal Reasoning About Confidence and Automated Verification of Neural Networks
Augustin AlbertAlbert, Augustin LIXFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Elvira AlbertAlbert, Elvira Towards Formally Verified Smart Contracts Compilation
Alessandro AldiniAldini, Alessandro University of UrbinoItaly Committee Member in Program Committee within the FM Research Track-track
Dalay AlmeidaAlmeida, Dalay CLEARSYFrance Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives
Ricardo AlmeidaAlmeida, Ricardo University of Glasgow, UK Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Jie AnAn, Jie Institute of Software Chinese Academy of SciencesChina Exact Moment Estimation of Stochastic Differential Dynamics
Mikkel Schmidt AndersenAndersen, Mikkel Schmidt Aarhus UniversityDenmark Digital Twins: a Briefing for Formalists
Oana AndreiAndrei, Oana University of GlasgowUnited Kingdom Committee Member in Program Committee within the FM Research Track-track
Étienne AndréAndré, Étienne Nantes UniversitéFrance Artifact Evaluation Co-Chair in Organizing Committee for FM 2026 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Pedro AntoninoAntonino, Pedro The Blockhouse Technology Limited Committee Member in Program Committee within the FM Research Track-track
Mari AokiAoki, Mari NASAUnited States Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial
Toshiaki AokiAoki, Toshiaki JAISTJapan Doctoral Symposium Co-Chair in Organizing Committee for FM 2026 Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track Doctoral Symposium Co-Chair in Program committee within the FM Doctoral Symposium-track Encoding BDI Syntax with Theories in Event-B Relational Verification of Identity Disclosure Using Alloy Practical Applications of Formal Methods to Automotive Systems: From In-Vehicle Systems to Autonomous Driving
Keijiro ArakiAraki, Keijiro Kyushu Institute of Technology, Japan Overture Keynote Talk
Dhyan AranhaAranha, Dhyan University of Amsterdam; Cote d'Azur UniversityNetherlands SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Paolo ArcainiArcaini, Paolo National Institute of InformaticsJapan Financial Chair in Organizing Committee for FM 2026
Samantha ArcherArcher, Samantha Stanford UniversityUnited States Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness
Alessandro ArmandoArmando, Alessandro University of Genova & Fondazione Bruno Kessler Committee Member in Program Committee within the FM Research Track-track
Cyrille ArthoArtho, Cyrille KTH Royal Institute of Technology, Sweden Doctoral Symposium Co-Chair in Organizing Committee for FM 2026 Doctoral Symposium Co-Chair in Program committee within the FM Doctoral Symposium-track
Giorgio AudritoAudrito, Giorgio Università di TorinoItaly Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach
Sowelu AvanzoAvanzo, Sowelu University of TurinItaly Formal Verification of Decentralized Autonomous Organizations
B Louwe B. KuijerB. Kuijer, Louwe University of LiverpoolUnited Kingdom History-Constrained Systems
Kaito BabaBaba, Kaito The University of TokyoJapan Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
Peter BackemanBackeman, Peter Mälardalen UniversitySweden From Execution to Necessity: Proof-Based Metrics for Code Coverage
Thom BadingsBadings, Thom University of OxfordUnited Kingdom Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Kyungmin BaeBae, Kyungmin POSTECHSouth Korea Committee Member in Program committee within the FM Doctoral Symposium-track
Christel BaierBaier, Christel TU Dresden, GermanyGermany Committee Member in Program Committee within the FM Research Track-track
Lydia BakiriBakiri, Lydia LIXFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Boutheina BannourBannour, Boutheina CEAFrance Specializing anti-unification for interaction models composition via gate connections
Lara BargmannBargmann, Lara University of OldenburgGermany Towards Proving Liveness on Weak Memory
Manel BarkallahBarkallah, Manel University of Namur Learning Formal Methods through Project-Based Modeling of Concurrent Systems with Anemone
Clark BarrettBarrett, Clark Stanford UniversityUnited States Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness Committee Member in Program Committee within the FM Research Track-track
Ezio BartocciBartocci, Ezio Technische Universität WienAustria Committee Member in Program Committee within the FM Research Track-track
Davide BasileBasile, Davide CNR-ISTIItaly Asynchronous Team Automata
Nick BattleBattle, Nick Semi-Retired Further Progress Towards Operation Proof Obligation Generation for VDM
Kevin BatzBatz, Kevin Cornell UniversityUnited States Verifying Sampling Algorithms via Distributional Invariants
Jan BaumeisterBaumeister, Jan CISPA Helmholtz Center for Information SecurityGermany Pacing Types for Asynchronous Stream Equations
Hugo BazilleBazille, Hugo EPITA Research LaboratoryFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Gabriele BelliniBellini, Gabriele University of MilanItaly Fuzzing executable ASMETA models
Izan Beltran FerreiroBeltran Ferreiro, Izan Axiomatic AISpain A Minimal Agent for Automated Theorem Proving
Julian BermanBerman, Julian Columbia UniversityUnited States SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Nicolas BerthierBerthier, Nicolas OCamlProFrance SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools
Carl BertonBerton, Carl Laboratoire MIS UR 4290, Université de Picardie Jules VerneFrance SAT-Based Syndrome Decoding and Low-Weight Codewords
Gustavo BetarteBetarte, Gustavo Facultad de Ingeniería, Universidad de la RepúblicaUruguay Committee Member in Program Committee within the FM Research Track-track
Mohamed BettazBettaz, Mohamed Czech Technical University in PragueCzechia Committee Member in Program Committee within the FM Research Track-track
Dirk BeyerBeyer, Dirk LMU MunichGermany Committee Member in Program Committee within the FM Research Track-track
Armin BiereBiere, Armin University of Freiburg, GermanyGermany Certifying Constraints in Hardware Model Checking
Nikolaj BjørnerBjørner, Nikolaj Microsoft Research Committee Member in Tutorial Track Committee within the FM Tutorials-track
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Committee Member in Program Committee within the FM Research Track-track
Rose BohrerBohrer, Rose National Institute of Advanced Industrial Science and Technology (AIST), JapanJapan Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance Committee Member in Tutorial Track Committee within the FM Tutorials-track
Andrea BombardaBombarda, Andrea University of BergamoItaly Evaluating the Practical Impact of Parallelism in Asmeta Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover
Silvia BonfantiBonfanti, Silvia University of BergamoItaly Evaluating the Practical Impact of Parallelism in Asmeta Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover
Patricia BouyerBouyer, Patricia CNRS Committee Member in Program Committee within the FM Research Track-track
Achim D. BruckerBrucker, Achim D. University of ExeterUnited Kingdom TAP Track Co-Chair in Organizing Committee for FM 2026 TAP Track Co-Chair in TAP Track Program Commitee within the FM TAP Track-track
Laura BussiBussi, Laura University of AmsterdamNetherlands Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Michael ButlerButler, Michael University of SouthamptonUnited Kingdom Committee Member in Tutorial Track Committee within the FM Tutorials-track Selection Committee Member in Journal-First Track Selection Committee within the FM Journal First-track SHARCS: Refinement-Centric Hazard Analysis of Requirements for Critical Systems
C Cristian CadarCadar, Cristian Imperial College LondonUnited Kingdom Testing and Analysis in the AI Era
Shaowei CaiCai, Shaowei Institute of Software at Chinese Academy of SciencesChina FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Zhiheng CaiCai, Zhiheng Tsinghua UniversityChina A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning
Radu CalinescuCalinescu, Radu University of York, UKUnited Kingdom The SLEEC Framework for Normative Requirements Engineering
Juan Diego CampoCampo, Juan Diego Universidad de la RepúblicaUruguay Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Jialun CaoCao, Jialun Hong Kong University of Science and TechnologyChina ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Yongzhi CaoCao, Yongzhi Peking UniversityChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Gustavo CarvalhoCarvalho, Gustavo Universidade Federal de PernambucoBrazil Committee Member in Program Committee within the FM Research Track-track Session Chair of FMTea Closing (part of FM Workshop: FMTea) Session Chair of FMTea Opening (part of FM Workshop: FMTea) Session Chair of FMTea FM4All Session 1 (part of FM Workshop: FMTea) Session Chair of FMTea Invited Talk 1 (part of FM Workshop: FMTea)
Darion CasselCassel, Darion Amazon Web ServicesUnited States Committee Member in Program Committee within the FM Research Track-track
Valentina CastiglioniCastiglioni, Valentina Eindhoven University of TechnologyNetherlands Committee Member in Program Committee within the FM Research Track-track
Ana CavalcantiCavalcanti, Ana University of YorkUnited Kingdom Committee Member in FME Board for FM 2026 The SLEEC Framework for Normative Requirements Engineering Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track Session Chair of FME Lucas Award (part of FM Main Plenaries / Invited Talks)
Lorenzo CeragioliCeragioli, Lorenzo IMT Lucca, ItalyItaly Differential Verification of Information Flow in SEAndroid Policies
Milan CeskaCeska, Milan Faculty of Information Technology, Brno University of Technology Committee Member in Program Committee within the FM Research Track-track
Marek ChalupaChalupa, Marek Institute of Science and Technology Austria Quantitative Monitoring of Signal First-Order Logic
Han-Myung ChangChang, Han-Myung Nanzan University Trace-Based Execution-Level Observability of VDM-SL Specifications
Agnishom ChattopadhyayChattopadhyay, Agnishom ImironJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Marsha ChechikChechik, Marsha University of TorontoCanada The SLEEC Framework for Normative Requirements Engineering
Jiawei ChenChen, Jiawei University of Michigan at Ann ArborUnited States A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
Minrui ChenChen, Minrui Kyushu UniversityJapan SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neural Theorem Proving
Rui ChenChen, Rui Beijing Institute of Control Engineering; Beijing Sunwise Information TechnologyChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Taolue ChenChen, Taolue Birkbeck, University of LondonUnited Kingdom Can LLM Aid in Solving Constraints with Inductive Definitions?
Yu-Fang ChenChen, Yu-Fang Academia SinicaTaiwan Committee Member in Program Committee within the FM Research Track-track
Zhenbang ChenChen, Zhenbang College of Computer, National University of Defense TechnologyChina Selective Concolic Testing EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Zhihan ChenChen, Zhihan Institute of Software, Chinese Academy of SciencesChina FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
Zhiyong ChenChen, Zhiyong Nanjing UniversityChina ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
Timofey CherganovCherganov, Timofey RusBITech-Astra LLCRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Sami CherifCherif, Sami Laboratoire MIS UR 4290, Université de Picardie Jules VerneFrance SAT-Based Syndrome Decoding and Low-Weight Codewords
Shing-Chi CheungCheung, Shing-Chi Department of Computer Science and Engineering, The HongKong University of Science and Technology, Hong Kong, China ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
Po-Chun ChienChien, Po-Chun LMU MunichGermany Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Yunja ChoiChoi, Yunja Kyungpook National UniversitySouth Korea Committee Member in Tutorial Track Committee within the FM Tutorials-track
Shachaf CohenCohen, Shachaf Tel Aviv UniversityIsrael Performance Heuristics for GR(1) Unrealizable Core Computation
Cesar CornejoCornejo, Cesar University of BergamoItaly Evaluating the Practical Impact of Parallelism in Asmeta
Miguel Corredera HidalgoCorredera Hidalgo, Miguel ENSEIRB-MATMECA, INP-BordeauxFrance SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Arthur CorrensonCorrenson, Arthur CISPA Helmholtz Center for Information Security Pacing Types for Asynchronous Stream Equations
Joana CoutinhoCoutinho, Joana OutSystemsPortugal (Extended Abstract) Verifiably UX Compliant and User-Intent Layout Generation
Alcino CunhaCunha, Alcino University of Minho; INESC TECPortugal Committee Member in Tutorial Track Committee within the FM Tutorials-track Validating Formal Specifications with LLM-generated Test Cases Committee Member in Program committee within the FM Doctoral Symposium-track Validating Formal Specifications with LLM-generated Test Cases Teaching Logic with Specification Challenges General Co-Chair in Organizing Committee within the FM ABZ-track
D Pedro R. D'ArgenioD'Argenio, Pedro R. Universidad Nacional de Córdoba - CONICET Committee Member in Program Committee within the FM Research Track-track
Deepak D'SouzaD'Souza, Deepak IISc BangaloreIndia Committee Member in Tutorial Track Committee within the FM Tutorials-track
Ferruccio DamianiDamiani, Ferruccio University of TurinItaly Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach
Susmoy DasDas, Susmoy University of GlasgowUnited Kingdom Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Daniel DaukševičDaukševič, Daniel Institute of Computer Science, Vilnius University, Vilnius,LithuaniaLithuania Cybersecurity Requirements Assurance in Critical Infrastructure Systems through the Application of Formal Verification and Artificial Intelligence-Based Methods Formal Verification of Healthcare Computer Network Architectures using Alloy and TLA+
Nancy DayDay, Nancy University of Waterloo, CanadaCanada Committee Member in Program Committee within the FM Research Track-track
Frank S. de Boerde Boer, Frank S. Centrum Wiskunde & Informatica, Leiden University Committee Member in Program Committee within the FM Research Track-track
José Luiz Vargas de Mendonçade Mendonça, José Luiz Vargas University of Michigan at Ann ArborUnited States A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
Steven de Oliveirade Oliveira, Steven OCamlProFrance SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools
Martina De SanctisDe Sanctis, Martina Gran Sasso Science InstituteItaly Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Claire DelaplaceDelaplace, Claire Laboratoire MIS UR 4290, Université de Picardie Jules VerneFrance SAT-Based Syndrome Decoding and Low-Weight Codewords
Louise DennisDennis, Louise University of ManchesterUnited Kingdom Counterexample-Guided Interval Weakening Security-Minded Modelling and Verification of Autonomous Satellite Docking
Werner DietlDietl, Werner University of WaterlooCanada A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures
Clare DixonDixon, Clare University of ManchesterUnited Kingdom Security-Minded Modelling and Verification of Autonomous Satellite Docking
Adel DjoudiDjoudi, Adel Thales Cybersecurity and Digital IdentityFrance Formal Verification for Security Certification: From a First Success to Sustainable Industrial Usage
Thi Thu Ha DoanDoan, Thi Thu Ha Japan Advanced Institute of Science and Technology Committee Member in Tutorial Track Committee within the FM Tutorials-track
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Automated Sketching and Repairing of Large Mechanised Proofs
Jin Song DongDong, Jin Song National University of SingaporeSingapore Committee Member in Program Committee within the FM Research Track-track Reasoning Beyond LLM: Formal Methods Agents
Wei DongDong, Wei National University of Defense TechnologyChina EUF-based Solving Dyck-Reachability with Applications to Static Analysis Accelerating Kind Realizability: A Multi-Stage Incremental Realizability Checking Framework
Yanni DongDong, Yanni Institute of Intelligent SoftwareChina Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Brijesh DongolDongol, Brijesh University of SurreyUnited Kingdom Reasoning over Relaxed Shared Memory Models: A Tutorial Committee Member in Tutorial Track Committee within the FM Tutorials-track Session Chair of Session 3: Concurrency & Memory Models (part of FM Research Track) Committee Member in Program Committee within the FM Research Track-track Session Chair of FMTea Session 1 (part of FM Workshop: FMTea)
Oliver DresslerDressler, Oliver --Germany SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Daniel DrodtDrodt, Daniel Technical University of DarmstadtGermany RustyDL: A Program Logic for Rust Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Yide DuDu, Yide College of Computer Science and Technology, NationalUniversity of Defense TechnologyChina EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Catherine DuboisDubois, Catherine ENSIIE Paris-Evry Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track
Guillaume DupontDupont, Guillaume INPT–ENSEEIHTFrance Committee Member in Program committee within the FM Doctoral Symposium-track Encoding BDI Syntax with Theories in Event-B
Vasil DyadovDyadov, Vasil Kaspersky LabRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education Identifying Design Flaws in a Lock-Free Task Pool with TLA+
Sarah DépernetDépernet, Sarah INRIA Nancy and Université de LorraineFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
E Paul EichlerEichler, Paul CISPA - Helmholtz Center for Information SecurityGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Mohamed ElwakilElwakil, Mohamed U.S. Coast Guard AcademyUnited States Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Julian ErhardErhard, Julian TU Munich; LMU MunichGermany Mixed Flow-Sensitive Static Analysis: Engineering Modularity
Lars-Henrik ErikssonEriksson, Lars-Henrik Uppsala UniversitySweden Committee Member in FME Board for FM 2026 Why does it fail? Explanation of verification failures
F João F. FerreiraF. Ferreira, João Faculty of Engineering, University of Porto & INESC-IDPortugal Committee Member in Program Committee within the FM Research Track-track
Marco FaellaFaella, Marco Università di Napoli "Federico II"Italy Committee Member in Program Committee within the FM Research Track-track
Marie FarrellFarrell, Marie The University of ManchesterUnited Kingdom Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track Session Chair of ABZ Session 6: Case Study (part of FM ABZ) Encoding BDI Syntax with Theories in Event-B Counterexample-Guided Interval Weakening Security-Minded Modelling and Verification of Autonomous Satellite Docking Case Study Track Co-Chair in Organizing Committee within the FM ABZ-track
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Formally Explaining Neural Network Classification
Shenghua FengFeng, Shenghua Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Exact Moment Estimation of Stochastic Differential Dynamics
Shenghua FengFeng, Shenghua Zhongguancun LaboratoryChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Weizhi FengFeng, Weizhi Institute of Software, Chinese Academy of SciencesChina Can LLM Aid in Solving Constraints with Inductive Definitions?
Eduardo FernandesFernandes, Eduardo Clever DevicesBrazil Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Natasha FernandesFernandes, Natasha Macquarie UniversityAustralia Committee Member in Program Committee within the FM Research Track-track
Carla FerreiraFerreira, Carla NOVA University LisbonPortugal Committee Member in Program Committee within the FM Research Track-track
Gianluca FilipponeFilippone, Gianluca Gran Sasso Science Institute, L'Aquila, ItalyItaly Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Pacing Types for Asynchronous Stream Equations
Michael FisherFisher, Michael University of Manchester, UKUnited Kingdom Counterexample-Guided Interval Weakening
John FitzgeraldFitzgerald, John Newcastle UniversityUnited Kingdom Digital Twins: a Briefing for Formalists A System-of-Systems Case Study for the Verification of Composed Digital Twins
Wan FokkinkFokkink, Wan Vrije Universiteit Amsterdam Committee Member in Program Committee within the FM Research Track-track
Simon FosterFoster, Simon University of YorkUnited Kingdom Verifying Properties of State-Based Models using Constraint Programming
José Fragoso SantosFragoso Santos, José INESC-ID; Instituto Superior Técnico - University of LisbonPortugal Committee Member in Program Committee within the FM Research Track-track
Marc FrappierFrappier, Marc Université de Sherbrooke, Canada Session Chair of ABZ Session 2: Safety and Security (part of FM ABZ)
Leo FreitasFreitas, Leo Newcastle University Committee Member in Tutorial Track Committee within the FM Tutorials-track Executing Kapture's Templates in VDM
Jan Friso GrooteFriso Groote, Jan Eindhoven University of Technology Committee Member in Program Committee within the FM Research Track-track
Nils FroleyksFroleyks, Nils KU LeuvenBelgium Certifying Constraints in Hardware Model Checking
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Array-Carrying Symbolic Execution for Function Contract Generation
Ryu FunaseFunase, Ryu The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Carlo A. FuriaFuria, Carlo A. Università della Svizzera italiana (USI)Switzerland Committee Member in FME Board for FM 2026 Session Chair of Session 4: LLMs Formal Methods (part of FM Research Track) Committee Member in Program Committee within the FM Research Track-track
G Letterio GallettaGalletta, Letterio IMT School for Advanced Studies LuccaItaly Differential Verification of Information Flow in SEAndroid Policies
Pierre GantyGanty, Pierre IMDEA Software Institute, SpainSpain Reachability-guided Abstraction Refinement
Chao GaoGao, Chao Kyoto UniversityJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Natalia GaraninaGaranina, Natalia A.P. Ershov Institute of Informatics Systems SB RASRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Angelo GargantiniGargantini, Angelo University of BergamoItaly Evaluating the Practical Impact of Parallelism in Asmeta Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover
Samir GenaimGenaim, Samir Universidad Complutense de MadridSpain Towards Formally Verified Smart Contracts Compilation
Blaise GenestGenest, Blaise IPAL - CNRS - CNRS@CREATEFrance Formal Reasoning About Confidence and Automated Verification of Neural Networks Formal Reasoning About Confidence and Automated Verification of Neural Networks
Sinem Getir YamanGetir Yaman, Sinem University of York, UKUnited Kingdom The SLEEC Framework for Normative Requirements Engineering
Mirco GiacobbeGiacobbe, Mirco University of BirminghamUnited Kingdom Neural Continuous-Time Supermartingale Certificates
Dimitra GiannakopoulouGiannakopoulou, Dimitra Amazon Web Services Committee Member in Program committee within the FM Doctoral Symposium-track
Santiago GilGil, Santiago Aarhus UniversityDenmark Digital Twins: a Briefing for Formalists
Mario GleirscherGleirscher, Mario ENSTA, IP ParisFrance Committee Member in Program Committee within the FM Research Track-track
Claudio GomesGomes, Claudio Aarhus University, DenmarkDenmark Digital Twins: a Briefing for Formalists
Akshay GopalakrishnanGopalakrishnan, Akshay McGill University Memory Consistency and Program Transformations
Gloria GoriGori, Gloria University of FlorenceItaly Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
R GovindGovind, R The Institute of Mathematical SciencesIndia Complexity of Consistency Testing for the Release-Acquire Semantics
Bin GuGu, Bin Beijing Institute of Control EngineeringChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Ji GuanGuan, Ji Institute of Software, Chinese Academy of SciencesChina QSeqSim: A Symbolic Simulator for Qiskit While Loops using Sequential Quantum Circuits
Bruno GuindaniGuindani, Bruno Politecnico di MilanoItaly Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
Ashutosh GuptaGupta, Ashutosh Indian Institute of Technology BombayIndia Formal Reasoning About Confidence and Automated Verification of Neural Networks Formal Reasoning About Confidence and Automated Verification of Neural Networks
Amit GurungGurung, Amit UPES Dehradun, INDIA, India Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Matthias GüdemannGüdemann, Matthias University of Applied Sciences MunichGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
H Ernst Moritz HahnHahn, Ernst Moritz University of TwenteNetherlands Committee Member in Program Committee within the FM Research Track-track
Raju HalderHalder, Raju Indian Institute of Technology PatnaIndia Committee Member in Tutorial Track Committee within the FM Tutorials-track
Joe HareHare, Joe Newcastle University Executing Kapture's Templates in VDM
John HarrisonHarrison, John Amazon Web ServicesUnited States s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Arnd HartmannsHartmanns, Arnd University of TwenteNetherlands Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking
Paul HarveyHarvey, Paul Rakuten Mobile Innovation StudioJapan Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment
Akira HasegawaHasegawa, Akira Japan Advanced Institute of Science and TechnologyJapan Revealing Intent–Implementation Gaps in Schedulers via Learning-Based Fuzzing
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking Committee Member in Program Committee within the FM Research Track-track Cutting out FM Angles from the Jungle of Automated Driving
Takato HataeHatae, Takato The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Klaus HavelundHavelund, Klaus Jet Propulsion Laboratory, California Institute of TechnologyUnited States Committee Member in Industry Day Program Committee within the FM Industry Day-track
Anne HaxthausenHaxthausen, Anne Technical University of DenmarkDenmark Journal-First Track Chair in Organizing Committee for FM 2026 Chair in Journal-First Track Selection Committee within the FM Journal First-track
Fei HeHe, Fei Tsinghua UniversityChina A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning
Linus HeckHeck, Linus Radboud UniversityNetherlands Probabilistic Model Checking Taken by Storm
Niklas HeidlerHeidler, Niklas Technical University Darmstadt, Software Engineering GroupGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Keijo HeljankoHeljanko, Keijo University of HelsinkiFinland Certifying Constraints in Hardware Model Checking
Holly HendryHendry, Holly University of YorkUnited Kingdom Large Language Models for Verification of Reactive Programs
Paula HerberHerber, Paula University of Munster, GermanyGermany Committee Member in Program Committee within the FM Research Track-track
Thomas T. HildebrandtHildebrandt, Thomas T. University of CopenhagenDenmark From Behaviour-Driven Development Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs
Aaron HillHill, Aaron ---United States SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Raik HiplerHipler, Raik University of LübeckGermany Machine Learning for Stream-Based Diagnosis
Hsi-Ming HoHo, Hsi-Ming University of Sussex Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Peter HoefnerHoefner, Peter Australian National UniversityAustralia Committee Member in Industry Day Program Committee within the FM Industry Day-track
Weijiang HongHong, Weijiang National University of Defense Technology, Changsha, ChinaChina Selective Concolic Testing
Falk HowarHowar, Falk TU Dortmund UniversityGermany Test Coverage of Automated Robotic Systems in Open World Environments Committee Member in Program Committee within the FM Research Track-track
Chiao HsiehHsieh, Chiao Kyoto UniversityJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Jonathan Julian Huerta y MuniveHuerta y Munive, Jonathan Julian Aalborg University in CopenhagenDenmark Automated Sketching and Repairing of Large Mechanised Proofs
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track
Juel HussainHussain, Juel University of ManchesterUnited Kingdom Security-Minded Modelling and Verification of Autonomous Satellite Docking
Reiner HähnleHähnle, Reiner TU Darmstadt Session Chair of Session 8: Model Checking & Program Synthesis (part of FM Research Track)
Reiner HähnleHähnle, Reiner Technical University of DarmstadtGermany RustyDL: A Program Logic for Rust Committee Member in Program Committee within the FM Research Track-track
I Atsushi IgarashiIgarashi, Atsushi Kyoto UniversityJapan Committee Member in Program Committee within the FM Research Track-track
Satoshi IkariIkari, Satoshi The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Vasily IlinIlin, Vasily Axiom MathUnited States Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
Soshi InoueInoue, Soshi Kyoto Institute of TechnologyJapan Towards Characterizing Commit Patterns in Formally Verified Open-Source Projects Using LLM-based Classification
Paola InverardiInverardi, Paola Gran Sasso Science InstituteItaly Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Ahmed IrfanIrfan, Ahmed SRI InternationalUnited States Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness
Alf IsakssonIsaksson, Alf ABB ABSweden Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego
Daisuke IshiiIshii, Daisuke JAIST Committee Member in Program committee within the FM Doctoral Symposium-track
Fuyuki IshikawaIshikawa, Fuyuki National Institute of InformaticsJapan General Chair in Organizing Committee for FM 2026 Session Chair of FM Keynote: Ruzica Piskac (part of FM Main Plenaries / Invited Talks) FM 2026 Opening General Co-Chair in Organizing Committee within the FM ABZ-track
Yosuke ItoIto, Yosuke Sompo Himawari Life Insurance Inc.Japan Formalizing Actuarial Mathematics in Proof Assistants
Noa IzsakIzsak, Noa CISPA Helmholtz Center for Information Security, GermanyGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
J Jean-Marie JacquetJacquet, Jean-Marie University of NamurBelgium Learning Formal Methods through Project-Based Modeling of Concurrent Systems with Anemone
Marie-Christine JakobsJakobs, Marie-Christine LMU Munich, GermanyGermany TAP Track Co-Chair in Organizing Committee for FM 2026 TAP Track Co-Chair in TAP Track Program Commitee within the FM TAP Track-track
Jean-Baptiste JeanninJeannin, Jean-Baptiste University of Michigan at Ann ArborUnited States A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
Huidong JiangJiang, Huidong Institute of Science TokyoJapan SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neural Theorem Proving
Einar Broch JohnsenJohnsen, Einar Broch University of OsloNorway Committee Member in FME Board for FM 2026 Committee Member in Program Committee within the FM Research Track-track
Victoria JohnsonJohnson, Victoria University of SheffieldUnited Kingdom Verifying Properties of State-Based Models using Constraint Programming
Cliff JonesJones, Cliff University of NewcastleUnited Kingdom Selection Committee Member in Journal-First Track Selection Committee within the FM Journal First-track
Sebastian JungesJunges, Sebastian Radboud University Probabilistic Model Checking Taken by Storm Error-awareness Accelerates Active Automata Learning
K Sinai KakishitaKakishita, Sinai Japan Advanced Institute of Science and TechnologyJapan Towards verified memory allocator for Rust
Cezary KaliszykKaliszyk, Cezary University of MelbourneAustralia AIPV Keynote: Autoformalization Across Proof Assistants: Languages, Proof Styles, and Automation
Ning KangKang, Ning Xi'an Jiaotong UniversityChina Fast SMT-Based Fault Tolerance Verification for Wide Area Networks
Andreas KatisKatis, Andreas KBR / NASA Ames Research CenterUnited States Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial
Takahiro KatoKato, Takahiro The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Probabilistic Model Checking Taken by Storm Highly Incremental: A Simple Programmatic Approach for Many Objectives Verifying Sampling Algorithms via Distributional Invariants
Yusuke KawamotoKawamoto, Yusuke National Institute of Advanced Industrial Science and Technology (AIST), JapanJapan Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
Jingyu KeKe, Jingyu Array-Carrying Symbolic Execution for Function Contract Generation
Jeroen KeirenKeiren, Jeroen Eindhoven University of Technology, The NetherlandsNetherlands Industry Day Co-Chair in Organizing Committee for FM 2026 Committee Member in Program Committee within the FM Research Track-track Session Chair of Industry Day Closing (part of FM Industry Day) Session Chair of Industry Session 3: AI-Assisted Requirements Engineering and Early-Stage Analysis (part of FM Industry Day) Industry Day Co-Chair in Industry Day Program Committee within the FM Industry Day-track
Philipp KernKern, Philipp Karlsruhe Institute of Technology (KIT)Germany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Mennatullah KhedrKhedr, Mennatullah Newcastle UniversityUnited Kingdom A System-of-Systems Case Study for the Verification of Composed Digital Twins
Joe KiniryKiniry, Joe Sigil Logic and Free & FairUnited States Committee Member in Industry Day Program Committee within the FM Industry Day-track
Alexander KnappKnapp, Alexander Committee Member in Program Committee within the FM Research Track-track
Tsutomu KobayashiKobayashi, Tsutomu Japan Aerospace Exploration Agency (JAXA)Japan Publicity Chair in Organizing Committee for FM 2026 Committee Member in Program Committee within the FM Research Track-track Session Chair of FMTea Closing (part of FM Workshop: FMTea) Session Chair of FMTea Opening (part of FM Workshop: FMTea) Session Chair of FMTea Invited Talk 2 (part of FM Workshop: FMTea) Session Chair of FMTea FM4All Session 2 (part of FM Workshop: FMTea) Session Chair of ABZ Session 6: Case Study (part of FM ABZ) Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment Case Study Track Co-Chair in Organizing Committee within the FM ABZ-track
Alexander KogtenkovKogtenkov, Alexander Kaspersky LabRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education Identifying Design Flaws in a Lock-Free Task Pool with TLA+
Florian KohnKohn, Florian CISPAGermany Pacing Types for Asynchronous Stream Equations
Tomáš KolárikKolárik, Tomáš University of LuganoSwitzerland Formally Explaining Neural Network Classification
Dmitry KondratyevKondratyev, Dmitry A.P. Ershov Institute of Informatics Systems SB RASRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Soonho KongKong, Soonho Amazon Web ServicesUnited States s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Elvis Konjoh SelabiKonjoh Selabi, Elvis Gran Sasso Science Institute and University of CamerinoItaly Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Nikolai KosmatovKosmatov, Nikolai Thales Research & TechnologyFrance Session Chair of TAP Session 2: Program Analysis, Testing & Coverage (part of FM TAP Track) Session Chair of Session 9: Automata & Reactive Models (part of FM Research Track) Committee Member in Program Committee within the FM Research Track-track Formal Verification for Security Certification: From a First Success to Sustainable Industrial Usage SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools Committee Member in Industry Day Program Committee within the FM Industry Day-track Session Chair of FM/TAP Keynote: Cristian Cadar (part of FM Main Plenaries / Invited Talks)
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria Committee Member in Program Committee within the FM Research Track-track
Shankaranarayanan KrishnaKrishna, Shankaranarayanan IIT BombayIndia Complexity of Consistency Testing for the Release-Acquire Semantics
Morten Haahr KristensenKristensen, Morten Haahr Aarhus UniversityDenmark Digital Twins: a Briefing for Formalists
Daniel KroeningKroening, Daniel AmazonUnited States The Industrial Perspective on GenAI for Formal Methods
Loes KrugerKruger, Loes Radboud UniversityNetherlands Session Chair of Session 6: SMT, SAT & Constraint Solving (part of FM Research Track) Error-awareness Accelerates Active Automata Learning
Shuhei KuritaKurita, Shuhei National Institute of InformaticsJapan Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
Stepan KuznetsovKuznetsov, Stepan TU Braunschweig & Huawei Hilbert Research CenterGermany Unifying Non-Atomicity for Weak Memory Models
Marta KwiatkowskaKwiatkowska, Marta University of OxfordUnited Kingdom Exact Verification of Graph Neural Networks with Incremental Constraint Solving Exact Verification of Graph Neural Networks with Incremental Constraint Solving
Thomas KühnKühn, Thomas Martin-Luther-University Halle-WittenbergGermany Automatic Assessment and Feedback on Undergraduates’ Structural Induction Proofs
L Faezeh LabbafLabbaf, Faezeh University of LuganoSwitzerland Formally Explaining Neural Network Classification
Linas LaibinisLaibinis, Linas Institute of Computer Science, Vilnius University, Vilnius,LithuaniaLithuania Formal Verification of Healthcare Computer Network Architectures using Alloy and TLA+
Regine LaleauLaleau, Regine Paris Est Creteil UniversityFrance Committee Member in Tutorial Track Committee within the FM Tutorials-track Session Chair of ABZ Session 4: Autonomy (part of FM ABZ)
Kim LarsenLarsen, Kim Aalborg UniversityDenmark Committee Member in Tutorial Track Committee within the FM Tutorials-track
Peter Gorm LarsenLarsen, Peter Gorm Aarhus UniversityDenmark Digital Twins: a Briefing for Formalists Further Progress Towards Operation Proof Obligation Generation for VDM A System-of-Systems Case Study for the Verification of Composed Digital Twins Overture Tool Overview
Pascale Le GallLe Gall, Pascale CentraleSupelecFrance Specializing anti-unification for interaction models composition via gate connections
Thierry LecomteLecomte, Thierry CLEARSYFrance Committee Member in Tutorial Track Committee within the FM Tutorials-track Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives
Juneyoung LeeLee, Juneyoung AWSUnited States Committee Member in Program Committee within the FM Research Track-track s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Alexandre LemosLemos, Alexandre OutSystemsPortugal (Extended Abstract) Verifiably UX Compliant and User-Intent Layout Generation
Fabrizio LeopardiLeopardi, Fabrizio University of LuganoSwitzerland Formally Explaining Neural Network Classification
Livia LestingiLestingi, Livia DEIB, Politecnico di MilanoItaly Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
Austin LetsonLetson, Austin Axiomatic AISpain A Minimal Agent for Automated Theorem Proving SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Martin LeuckerLeucker, Martin University of LübeckGermany Machine Learning for Stream-Based Diagnosis
Michael LeuschelLeuschel, Michael University of Düsseldorf Committee Member in Tutorial Track Committee within the FM Tutorials-track
Paul LezeauLezeau, Paul Imperial College; The London School of Geometry and NumberTheoryUnited Kingdom SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Guoqiang LiLi, Guoqiang Shanghai Jiao Tong UniversityChina Array-Carrying Symbolic Execution for Function Contract Generation
Hao LiLi, Hao Xi'an Jiaotong UniversityChina Fast SMT-Based Fault Tolerance Verification for Wide Area Networks
Haokun LiLi, Haokun Peking University Array-Carrying Symbolic Execution for Function Contract Generation
Haonan LiLi, Haonan MBZUAI A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Yi LiLi, Yi Nanyang Technological UniversitySingapore Committee Member in Program committee within the FM Doctoral Symposium-track Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems
Zihao LiLi, Zihao University of Chinese Academy of SciencesChina QSeqSim: A Symbolic Simulator for Qiskit While Loops using Sequential Quantum Circuits
Xiao LiangLiang, Xiao Xidian University Automated ITL Specification Generation from Industrial Aerospace Requirements
Michael LienhardtLienhardt, Michael Automatic Memory Management for Dataflows
Hyojae LimLim, Hyojae Korea Institute for Advanced Study (KIAS)South Korea Toward Textbook-Scale Autoformalization with Large Language Models
Shang-Wei LINLIN, Shang-Wei Singapore Institute of TechnologySingapore Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems
Marian Lingsch-RosenfeldLingsch-Rosenfeld, Marian LMU Munich Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Carlo LipizziLipizzi, Carlo Stevens Institute on TechnologyUnited States s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Chaoran LiuLiu, Chaoran Research and Development Center for Large Language Models,National Institute of InformaticsJapan Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
Cong LiuLiu, Cong CollinsUnited States Committee Member in Industry Day Program Committee within the FM Industry Day-track
Jiaxiang LiuLiu, Jiaxiang Institute of Software, Chinese Academy of SciencesChina Can LLM Aid in Solving Constraints with Inductive Definitions?
Kunlin LiuLiu, Kunlin School of Computer, National University of Defense Technology, ChinaChina EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Minghao LiuLiu, Minghao University of OxfordUnited Kingdom Exact Verification of Graph Neural Networks with Incremental Constraint Solving Exact Verification of Graph Neural Networks with Incremental Constraint Solving
Shaoying LiuLiu, Shaoying East China Normal University, ChinaChina Committee Member in Program committee within the FM Doctoral Symposium-track
Si LiuLiu, Si Texas A&M UniversityUnited States A Formal Framework for Predicting Distributed System Performance under Faults
Sirui LiuLiu, Sirui College of Computer Science, National University of DefenseTechnology, Changsha, ChinaChina Accelerating Kind Realizability: A Multi-Stage Incremental Realizability Checking Framework
Tianhai LiuLiu, Tianhai Karlsruhe Institute of Technology (KIT), and aicas GmbHGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Wei LiuLiu, Wei Concordia University, Montreal, CanadaCanada Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Xiaolin LiuLiu, Xiaolin KTH Royal Institute of TechnologySweden Visualizing Neural Network Behaviors for Verification
Yang LiuLiu, Yang Selective Concolic Testing
Zhiming LiuLiu, Zhiming Southwest University Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification Committee Member in Program Committee within the FM Research Track-track
Delphine LonguetLonguet, Delphine Thales Research & TechnologyFrance SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools
Florian LonsingLonsing, Florian UnaffiliatedAustria Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness
Chia-Hsuan LuLu, Chia-Hsuan University of OxfordUnited Kingdom Exact Verification of Graph Neural Networks with Incremental Constraint Solving Exact Verification of Graph Neural Networks with Incremental Constraint Solving
Weijie LuLu, Weijie Shanghai Jiao Tong UniversityChina Array-Carrying Symbolic Execution for Function Contract Generation
Anna LukinaLukina, Anna Delft University of TechnologyNetherlands Neural Continuous-Time Supermartingale Certificates
Edoardo LunatiLunati, Edoardo IMT School for Advanced Studies LuccaItaly Differential Verification of Information Flow in SEAndroid Policies
Deyun LyuLyu, Deyun National Institute of InformaticsJapan Web Chair in Organizing Committee for FM 2026 Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
M Ben M. AndrewM. Andrew, Ben University of ManchesterUnited Kingdom Counterexample-Guided Interval Weakening
Ke MaMa, Ke EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Zhi MaMa, Zhi Xidian UniversityChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Dara MacConvilleMacConville, Dara Maynooth UniversityIreland Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Nuno MacedoMacedo, Nuno University of Porto; INESC TECPortugal Validating Formal Specifications with LLM-generated Test Cases Committee Member in Program Committee within the FM Research Track-track Validating Formal Specifications with LLM-generated Test Cases
Erwan MaheMahe, Erwan CEAFrance Specializing anti-unification for interaction models composition via gate connections
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
Nicolas ManiniManini, Nicolas IMDEA Software InstituteSpain Reachability-guided Abstraction Refinement
Shahar MaozMaoz, Shahar Tel Aviv UniversityIsrael Performance Heuristics for GR(1) Unrealizable Core Computation
Diego MarmsolerMarmsoler, Diego University of Exeter Committee Member in Program Committee within the FM Research Track-track
Lina MarssoMarsso, Lina Polytechnique Montreal The SLEEC Framework for Normative Requirements Engineering
Enrique Martin-MartinMartin-Martin, Enrique Universidad Complutense de MadridSpain Towards Formally Verified Smart Contracts Compilation
Mieke MassinkMassink, Mieke CNR-ISTI Pisa, Italy Committee Member in Program Committee within the FM Research Track-track
Karl MattsonMattson, Karl Mälardalen UniversitySweden From Execution to Necessity: Proof-Based Metrics for Code Coverage
Norman MauryMaury, Norman CLEARSYFrance Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives
Anastasia MavridouMavridou, Anastasia KBR / NASA Ames Research CenterUnited States Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial Committee Member in Program Committee within the FM Research Track-track
Annabelle McIverMcIver, Annabelle Macquarie University Committee Member in Program Committee within the FM Research Track-track
Sean McLarenMcLaren, Sean University of GlasgowUnited Kingdom Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment
Hernan MelgrattiMelgratti, Hernan University of Buenos Aires, Argentina Committee Member in Program Committee within the FM Research Track-track
Alexandra MendesMendes, Alexandra Faculty of Engineering, University of Porto, PortugalPortugal Committee Member in Program Committee within the FM Research Track-track
Dominique MeryMery, Dominique Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, FranceFrance Session Chair of ABZ Session 1: Concurrent and Distributed Systems (part of FM ABZ) Session Chair of ABZ Session 1: Concurrent and Distributed Systems (part of FM ABZ) Systematic Development of Distributed Algorithms using Event-B - Experiences, reviews and prospects -
Stephan MerzMerz, Stephan Inria & Loria, Nancy, FranceFrance Committee Member in Tutorial Track Committee within the FM Tutorials-track
Canh Minh DoMinh Do, Canh Japan Advanced Institute of Science and TechnologyJapan Committee Member in Tutorial Track Committee within the FM Tutorials-track
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance Committee Member in Tutorial Track Committee within the FM Tutorials-track
Raffaela MirandolaMirandola, Raffaela Karlsruhe Institute of Technology (KIT)Germany Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Mara MiulescuMiulescu, Mara Eindhoven University of TechnologyNetherlands A Method for Testing Partial-Order Reduction Theories in Alloy
Rosemary MonahanMonahan, Rosemary Ireland Committee Member in Tutorial Track Committee within the FM Tutorials-track
Yoàv MontacuteMontacute, Yoàv National Institute of InformaticsJapan Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
Carroll MorganMorgan, Carroll University of New South Wales; Trustworthy Systems Committee Member in Program Committee within the FM Research Track-track
Alexandre MotaMota, Alexandre Universidade Federal de Pernambuco Committee Member in Program Committee within the FM Research Track-track
Mohammad Reza MousaviMousavi, Mohammad Reza King's College LondonUnited Kingdom Committee Member in Program Committee within the FM Research Track-track
Cesar MunozMunoz, Cesar NASAUnited States Committee Member in Tutorial Track Committee within the FM Tutorials-track
N Muhammad NaeemNaeem, Muhammad Mälardalen University, Västerås, SwedenSweden Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego
Fumiko NagoyaNagoya, Fumiko College of Commerce, Nihon University Committee Member in Tutorial Track Committee within the FM Tutorials-track
Misato NakabayashiNakabayashi, Misato NTT Social Informatics LaboratoriesJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Masaki NakamuraNakamura, Masaki Toyama Prefectural University Committee Member in Tutorial Track Committee within the FM Tutorials-track
Riki NakamuraNakamura, Riki The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Yoshihiko NakamuraNakamura, Yoshihiko National Institute of Technology, Tomakomai CollegeJapan Seven-Year Activity to Introduce B-Method to Japanese Technical College Students
Shinichi NakasukaNakasuka, Shinichi The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Stefan NaujokatNaujokat, Stefan TU Dortmund UniversityGermany Test Coverage of Automated Robotic Systems in Open World Environments
David NaumannNaumann, David Stevens Institute of TechnologyUnited States Committee Member in Program Committee within the FM Research Track-track
Thomas NeeleNeele, Thomas Eindhoven University of TechnologyNetherlands A Method for Testing Partial-Order Reduction Theories in Alloy
Danel NeiderNeider, Danel TU Dortmund UniversityGermany Test Coverage of Automated Robotic Systems in Open World Environments Committee Member in Program Committee within the FM Research Track-track
Grigory NeustroevNeustroev, Grigory Zeroth ResearchNetherlands Neural Continuous-Time Supermartingale Certificates
Joel NguetoumNguetoum, Joel CEAFrance Specializing anti-unification for interaction models composition via gate connections
Anh NguyenNguyen, Anh Japan Advanced Institute of Science and Technology Committee Member in Tutorial Track Committee within the FM Tutorials-track
Peter NightingaleNightingale, Peter University of YorkUnited Kingdom Verifying Properties of State-Based Models using Constraint Programming
Shunichiro NomuraNomura, Shunichiro The University of TokyoJapan Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint
Gethin NormanNorman, Gethin University of Glasgow Committee Member in Program Committee within the FM Research Track-track
Krystian NowakowskiNowakowski, Krystian Axiomatic AISpain A Minimal Agent for Automated Theorem Proving
Jose Nuno OliveiraNuno Oliveira, Jose University of Minho; INESC TECPortugal Committee Member in Program Committee within the FM Research Track-track
O Tomohiro OdaOda, Tomohiro Software Research Associates, Inc. Trace-Based Execution-Level Observability of VDM-SL Specifications ViennaTalk Overview
Kazuhiro OgataOgata, Kazuhiro Japan Advanced Institute of Science and Technology Tutorials Co-Chair in Organizing Committee for FM 2026 Tutorials Co-Chair in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program Committee within the FM Research Track-track
Takaomi OhnishiOhnishi, Takaomi National Institute of Technology, Tomakomai College, JapanJapan Seven-Year Activity to Introduce B-Method to Japanese Technical College Students
Tiago OliveiraOliveira, Tiago University of Minho and INESC TECPortugal Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
P Rémi ParrotParrot, Rémi Nantes Université - LS2NFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Romain PascualPascual, Romain MICS, CentraleSupélec, Université Paris-SaclayFrance Slicing Models for Equiconsistency with Alloy
Samuel PastvaPastva, Samuel Masaryk UniversityCzechia Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Reuven PelegPeleg, Reuven Hebrew University of JerusalemIsrael Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Nico PellegrinelliPellegrinelli, Nico University of BergamoItaly Evaluating the Practical Impact of Parallelism in Asmeta Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover
Bram PellenPellen, Bram Radboud UniversityNetherlands Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Chao PengPeng, Chao East China Normal UniversityChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Xinghao PengPeng, Xinghao Formal Verification of Soundness and Completeness for Polygon zkEVM
Luigia PetrePetre, Luigia Åbo Akademi UniversityFinland Committee Member in Program Committee within the FM Research Track-track Session Chair of FMTea Opening (part of FM Workshop: FMTea) FM4All - FME Guidelines for Teaching Formal Methods as a Knowledge Area in the ACM Curriculum FM4All - FME Guidelines for Teaching Formal Methods as a Knowledge Area in the ACM Curriculum
Laure PetrucciPetrucci, Laure CNRS; LIPN; Université Sorbonne Paris NordFrance Committee Member in Program Committee within the FM Research Track-track
Sara PettinariPettinari, Sara Gran Sasso Science InstituteItaly Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Wolfram PfeiferPfeifer, Wolfram Karlsruhe Institute of Technology (KIT)Germany A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures
Kittiphon PhalakarnPhalakarn, Kittiphon National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Ken PiercePierce, Ken The University of Newcastle Executing Kapture's Templates in VDM
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Towards Privacy-Preserving Verification
Nico PlatPlat, Nico Netherlands Committee Member in FME Board for FM 2026
Auguste PoirouxPoiroux, Auguste Math, Inc; EPFLSwitzerland SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Zi Pong LimPong Lim, Zi Nanyang Technological UniversitySingapore Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems
Tephilla PrincePrince, Tephilla Indian Institute of Technology, DharwadIndia Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
José ProençaProença, José CISTER & Faculty of Sciences, University of PortoPortugal Asynchronous Team Automata
Frederik PuPu, Frederik University of TorontoCanada SorryDB: Can AI Provers Complete Real-World Lean Theorems?
David PurserPurser, David University of LiverpoolUnited Kingdom History-Constrained Systems
Lisa PühlPühl, Lisa RWTH Aachen UniversityGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Q Niuniu QiQi, Niuniu East China Normal UniversityChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Shengchao QinQin, Shengchao Xidian UniversityChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Tim QuatmannQuatmann, Tim RWTH Aachen UniversityGermany Probabilistic Model Checking Taken by Storm Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking
R Francesco RanzatoRanzato, Francesco University of PadovaItaly Reachability-guided Abstraction Refinement
Balaji RaoRao, Balaji Stevens Institute of TechnologyUnited States s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Jean-François RaskinRaskin, Jean-François Université Libre de Bruxelles Committee Member in Program Committee within the FM Research Track-track
Jiawei RenRen, Jiawei University of New South WalesAustralia Mining Verdict Boundaries for Neural Network Verification
Mengxin RenRen, Mengxin East China Normal UniversityChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Carlo RendeRende, Carlo Aarhus University Further Progress Towards Operation Proof Obligation Generation for VDM
Borja RequenaRequena, Borja Axiomatic AISpain A Minimal Agent for Automated Theorem Proving
Pedro ResendeResende, Pedro OutSystemsPortugal (Extended Abstract) Verifiably UX Compliant and User-Intent Layout Generation
Pedro RibeiroRibeiro, Pedro University of York, UKUnited Kingdom The SLEEC Framework for Normative Requirements Engineering Large Language Models for Verification of Reactive Programs Verifying Properties of State-Based Models using Constraint Programming
Áron Ricardo Perez-LopezRicardo Perez-Lopez, Áron Stanford UniversityUnited States Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness
Elvinia RiccobeneRiccobene, Elvinia Computer Science Dept., University of MilanItaly Committee Member in Tutorial Track Committee within the FM Tutorials-track Committee Member in Program committee within the FM Doctoral Symposium-track Fuzzing executable ASMETA models Formal Verification of Decentralized Autonomous Organizations
Maximilian RindlerRindler, Maximilian Graz University of TechnologyAustria Active Automata Learning with Noisy Data: From Big to Small Data
Peter RiviereRiviere, Peter Japan Advanced Institute of Science and Technology (JAIST)Japan Encoding BDI Syntax with Theories in Event-B Relational Verification of Identity Disclosure Using Alloy
Thiago Rocha SilvaRocha Silva, Thiago University of Southern DenmarkDenmark From Behaviour-Driven Development Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs
Andoni RodríguezRodríguez, Andoni IMDEA Software Institute, SpainSpain Maximum Realizability for LTL Modulo Theories
Matteo RossiRossi, Matteo Politecnico di MilanoItaly Committee Member in Program Committee within the FM Research Track-track Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
Jurriaan RotRot, Jurriaan Radboud University NijmegenNetherlands Error-awareness Accelerates Active Automata Learning
Kristin Yvonne RozierRozier, Kristin Yvonne Iowa State University Committee Member in Program committee within the FM Doctoral Symposium-track
Robert RubbensRubbens, Robert University of Twente Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
S Ramesh SS, Ramesh Committee Member in Tutorial Track Committee within the FM Tutorials-track
Edward SabinusSabinus, Edward Martin-Luther-University Halle-WittenbergGermany Automatic Assessment and Feedback on Undergraduates’ Structural Induction Proofs
Hiroto SaigoSaigo, Hiroto Kyushu UniversityJapan SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neural Theorem Proving
Asieh Salehi FathabadiSalehi Fathabadi, Asieh University of SouthamptonUnited Kingdom Session Chair of ABZ Session 5: Methods (2) (part of FM ABZ) SHARCS: Refinement-Centric Hazard Analysis of Requirements for Critical Systems Human-Centred Formal Verification: A Vision for Bridging Technical Rigour with Stakeholder Needs in Autonomous Systems
Augusto SampaioSampaio, Augusto Universidade Federal de PernambucoBrazil Program Co-Chair in Organizing Committee for FM 2026 Committee Member in Tutorial Track Committee within the FM Tutorials-track Program Co-Chair in Program Committee within the FM Research Track-track Session Chair of FM Industry Keynote: Daniel Kroening (part of FM Main Plenaries / Invited Talks) FM 2026 Opening
Pierluigi San PietroSan Pietro, Pierluigi Politecnico di MilanoItaly Committee Member in Program Committee within the FM Research Track-track Committee Member in Program Committee within the FM Research Track-track
Akiyoshi SannaiSannai, Akiyoshi Kyoto UniversityJapan Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
N. Ege SaraçSaraç, N. Ege CISPA Helmholtz Center for Information SecurityGermany Quantitative Monitoring of Signal First-Order Logic
Leopoldo SarraSarra, Leopoldo Axiomatic AISpain A Minimal Agent for Automated Theorem Proving SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Naoto SatoSato, Naoto Hitachi, Ltd.Japan Industry Day Co-Chair in Organizing Committee for FM 2026 Session Chair of Industry Session 1: Automated Synthesis, Optimization, and Certification (part of FM Industry Day) Session Chair of Industry Day Opening (part of FM Industry Day) Industry Day Co-Chair in Industry Day Program Committee within the FM Industry Day-track
Sota SatoSato, Sota Kyoto UniversityJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Sota SatoSato, Sota National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Patrizia ScandurraScandurra, Patrizia University of Bergamo, ItalyItaly Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines
Giordano ScarsoScarso, Giordano University of TurinItaly Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach
Till SchallauSchallau, Till TU Dortmund UniversityGermany Test Coverage of Automated Robotic Systems in Open World Environments
Dominik SchmidSchmid, Dominik TU Dortmund UniversityGermany Test Coverage of Automated Robotic Systems in Open World Environments
Gerardo SchneiderSchneider, Gerardo University of GothenburgSweden Committee Member in Program Committee within the FM Research Track-track Committee Member in Program committee within the FM Doctoral Symposium-track
Daniel SchoepeSchoepe, Daniel Amazon Web Services, USAUnited States Committee Member in Program Committee within the FM Research Track-track
Philipp SchröerSchröer, Philipp RWTH Aachen UniversityGermany Highly Incremental: A Simple Programmatic Approach for Many Objectives
Michael SchwarzSchwarz, Michael National University of SingaporeSingapore Mixed Flow-Sensitive Static Analysis: Engineering Modularity
Cristina SeceleanuSeceleanu, Cristina Mälardalen UniversitySweden Committee Member in Program Committee within the FM Research Track-track Session Chair of Industry Session 2: Code-Level Verification, Repair, and Testing (part of FM Industry Day) Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego Committee Member in Industry Day Program Committee within the FM Industry Day-track
Tiberiu SeceleanuSeceleanu, Tiberiu Mälardalen UniversitySweden Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego
Helmut SeidlSeidl, Helmut TU MunichGermany Mixed Flow-Sensitive Static Analysis: Engineering Modularity
Martina SeidlSeidl, Martina Johannes Kepler University LinzAustria Committee Member in Program committee within the FM Doctoral Symposium-track
Emil SekerinskiSekerinski, Emil McMaster University, CanadaCanada Committee Member in Program Committee within the FM Research Track-track A Spectabular Model of an Automotive Adaptive Exterior Light System
Michele SevegnaniSevegnani, Michele University of GlasgowUnited Kingdom Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs
Rohith Kumar ShanmuganathanShanmuganathan, Rohith Kumar Carl von Ossietzky Universität Oldenburg / University of OldenburgGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Natasha SharyginaSharygina, Natasha USI Lugano, SwitzerlandSwitzerland Formally Explaining Neural Network Classification
Ilya ShchepetkovShchepetkov, Ilya Kaspersky LabRussia Identifying Design Flaws in a Lock-Free Task Pool with TLA+
Vladimir ShelekhovShelekhov, Vladimir A.P. Ershov Institute of Informatics Systems SB RASRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Shidong ShenShen, Shidong Institute of Software, Chinese Academy of SciencesChina Can LLM Aid in Solving Constraints with Inductive Definitions?
Nikolay ShilovShilov, Nikolay Innopolis UniversityRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Yon Shin TeoShin Teo, Yon Aumovio SESingapore Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems
Irina ShoshminaShoshmina, Irina Peter the Great St. Petersburg Polytechnic UniversityRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Ziqi ShuaiShuai, Ziqi School of Computer, National University of Defense Technology, ChinaChina Selective Concolic Testing
Julien SignolesSignoles, Julien Université Paris-Saclay, CEA, ListFrance Teaching Frama-C for Cybersecurity
Sanchari SilSil, Sanchari Chennai Mathematical InstituteIndia Complexity of Consistency Testing for the Release-Acquire Semantics
Adenilso SimãoSimão, Adenilso University of São PauloBrazil Committee Member in Program Committee within the FM Research Track-track
Henry Sinclair-BanksSinclair-Banks, Henry University of WarsawPoland History-Constrained Systems
Neeraj SinghSingh, Neeraj INPT-ENSEEIHT / IRIT, University of Toulouse, FranceFrance Tutorials Co-Chair in Organizing Committee for FM 2026 Tutorials Co-Chair in Tutorial Track Committee within the FM Tutorials-track Encoding BDI Syntax with Theories in Event-B
Shobhit SinghSingh, Shobhit Karlsruhe Institute of TechnologyGermany Slicing Models for Equiconsistency with Alloy
Fabien SironSiron, Fabien CEA, ListFrance Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Graeme SmithSmith, Graeme The University of QueenslandAustralia Committee Member in Tutorial Track Committee within the FM Tutorials-track Session Chair of Session 1: Information Flow Verification (part of FM Research Track) Generating Rely-Guarantee Conditions with the Conditional-Writes Domain Committee Member in Program Committee within the FM Research Track-track Session Chair of FMTea Session 2 (part of FM Workshop: FMTea) Autograding Weakest Precondition Proofs and Dafny Specifications
SoaibuzzamanSoaibuzzaman Bauhaus-University WeimarGermany Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Frank SoboczenskiSoboczenski, Frank University of York, Kings College London, Alan TuringInstituteUnited Kingdom Large Language Models for Verification of Reactive Programs
Ana SokolovaSokolova, Ana University of SalzburgAustria Committee Member in Program Committee within the FM Research Track-track
Reza SoltaniSoltani, Reza University of TwenteNetherlands Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Thai Son HoangSon Hoang, Thai University of SouthamptonUnited Kingdom SHARCS: Refinement-Centric Hazard Analysis of Requirements for Critical Systems
Fu SongSong, Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software TechnologyChina Can LLM Aid in Solving Constraints with Inductive Definitions?
Sho SonodaSonoda, Sho RIKEN / CyberAgentJapan Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
B SrivathsanSrivathsan, B Chennai Mathematical InstituteIndia Complexity of Consistency Testing for the Release-Acquire Semantics
Isobel StandenStanden, Isobel University of YorkUnited Kingdom The SLEEC Framework for Normative Requirements Engineering
Gaëtan StaquetStaquet, Gaëtan Nantes Université - École Centrale Nantes - CNRS - LS2N - UMR 6004France Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Sergey StaroletovStaroletov, Sergey Polzunov Altai State Technical UniversityRussia VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
Sebastian SteinStein, Sebastian University of SouthamptonUnited Kingdom Human-Centred Formal Verification: A Vision for Bridging Technical Rigour with Stakeholder Needs in Autonomous Systems
Amy StellStell, Amy University of ExeterUnited Kingdom Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Marielle StoelingaStoelinga, Marielle University of Twente and Radboud University, NijmegenNetherlands Program Co-Chair in Organizing Committee for FM 2026 Committee Member in Tutorial Track Committee within the FM Tutorials-track Program Co-Chair in Program Committee within the FM Research Track-track Session Chair of FM/ABZ Keynote: Ichiro Hasuo (part of FM Main Plenaries / Invited Talks) FM 2026 Opening
Volker StolzStolz, Volker Høgskulen på VestlandetNorway Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach
Terru StübingerStübinger, Terru Karlsruhe Institut für TechnologieGermany Slicing Models for Equiconsistency with Alloy
Han SuSu, Han National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Yulei SuiSui, Yulei University of New South WalesAustralia Mining Verdict Boundaries for Neural Network Verification
Jun SunSun, Jun Singapore Management UniversitySingapore Committee Member in Tutorial Track Committee within the FM Tutorials-track Selective Concolic Testing Committee Member in Program Committee within the FM Research Track-track
Zhihang SunSun, Zhihang Tsinghua UniversityChina A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning
Zhouyue SunSun, Zhouyue Shanghai Jiao Tong UniversityChina Array-Carrying Symbolic Execution for Function Contract Generation
Takashi SuwaSuwa, Takashi Kyoto University and ImironJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
César SánchezSánchez, César IMDEA Software InstituteSpain Maximum Realizability for LTL Modulo Theories
T Lenny TaelmanTaelman, Lenny University of AmsterdamNetherlands SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Alberto TagliaferroTagliaferro, Alberto Politecnico di Milano, ItalyItaly Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
Tsubasa TakagiTakagi, Tsubasa Japan Advanced Institute of Science and Technology Committee Member in Tutorial Track Committee within the FM Tutorials-track
Carolyn TalcottTalcott, Carolyn SRI International Committee Member in Tutorial Track Committee within the FM Tutorials-track
Chengsong TanTan, Chengsong KaihongChina Automated Sketching and Repairing of Large Mechanised Proofs
Silvia Lizeth Tapia TarifaTapia Tarifa, Silvia Lizeth University of Oslo, Norway Committee Member in Program Committee within the FM Research Track-track
Landon TaylorTaylor, Landon Utah State UniversityUnited States Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Maurice ter Beekter Beek, Maurice CNR-ISTI Pisa, ItalyItaly Committee Member in FME Board for FM 2026 Committee Member in Tutorial Track Committee within the FM Tutorials-track Session Chair of Session 11: Cyber-Physical & Robotics Systems (part of FM Research Track) Asynchronous Team Automata Committee Member in Program Committee within the FM Research Track-track Session Chair of ABZ Session 3: Methods (1) (part of FM ABZ)
Marc ThiemeThieme, Marc Karlsruhe Institute of TechnologyGermany Slicing Models for Equiconsistency with Alloy
Will ThomasThomas, Will University of Kansas Static Analysis and Synthesis of Layered Attestation Protocols
Cong TianTian, Cong Xidian UniversityChina Automated ITL Specification Generation from Industrial Aerospace Requirements
James ToblerTobler, James The University of QueenslandAustralia Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
Gianluca TortaTorta, Gianluca Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach
Patrick TotzkeTotzke, Patrick University of LiverpoolUnited Kingdom History-Constrained Systems
Beverley TownsendTownsend, Beverley University of YorkUnited Kingdom The SLEEC Framework for Normative Requirements Engineering
Jan TretmansTretmans, Jan Radboud University Nijmegen, TNO-ESINetherlands Committee Member in Program Committee within the FM Research Track-track
Stavros TripakisTripakis, Stavros Northeastern University Towards Language Model Guided TLA+ Proof Automation
Elena TroubitsynaTroubitsyna, Elena KTH Workshops Co-Chair in Organizing Committee for FM 2026 Engineering Resilient Autonomous Systems with Formal Methods Workshops Co-Chair in Workshop Committee within the FM Workshops Proposal-track
George TsoukalasTsoukalas, George The University of Texas at AustinUnited States SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Tatsuhiro TsuchiyaTsuchiya, Tatsuhiro Osaka UniversityJapan Committee Member in Tutorial Track Committee within the FM Tutorials-track
Xinyuan TuTu, Xinyuan University of CopenhagenDenmark From Behaviour-Driven Development Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs
Radu-Florin TulcanTulcan, Radu-Florin TU WienAustria Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
U Mattias UlbrichUlbrich, Mattias KITGermany A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures Committee Member in Program Committee within the FM Research Track-track Slicing Models for Equiconsistency with Alloy
Felix Ulrich-OlteanUlrich-Oltean, Felix University of YorkUnited Kingdom Verifying Properties of State-Based Models using Constraint Programming
V Frits VaandragerVaandrager, Frits Radboud UniversityNetherlands Committee Member in Program Committee within the FM Research Track-track
Simone ValentiniValentini, Simone University of MilanItaly Formal Verification of Decentralized Autonomous Organizations
Jaco van de Polvan de Pol, Jaco Aarhus UniversityDenmark Committee Member in Program Committee within the FM Research Track-track
Mark van Wijkvan Wijk, Mark University of TwenteNetherlands Session Chair of Session 2: Neural Networks Verification (part of FM Research Track) Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking
Laurent VoisinVoisin, Laurent Systerel Committee Member in Tutorial Track Committee within the FM Tutorials-track
Vesal VojdaniVojdani, Vesal University of TartuEstonia Mixed Flow-Sensitive Static Analysis: Engineering Modularity
Matthias VolkVolk, Matthias Eindhoven University of TechnologyNetherlands Probabilistic Model Checking Taken by Storm Session Chair of Session 10: Distributed Systems & Fault Tolerance (part of FM Research Track) Committee Member in Program Committee within the FM Research Track-track
Benjamin von Bergvon Berg, Benjamin Graz University of TechnologyAustria Active Automata Learning with Noisy Data: From Big to Small Data BDD-based Deadlock Prevention for Automated Guided Vehicles in Warehouse Logistics Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
W Masaki WagaWaga, Masaki Kyoto UniversityJapan Artifact Evaluation Co-Chair in Organizing Committee for FM 2026 Session Chair of Session 7: Programming Languages & Program Logic (part of FM Research Track) Committee Member in Program committee within the FM Doctoral Symposium-track Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Ryo WakizakaWakizaka, Ryo IBM Research - TokyoJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Felix WallnerWallner, Felix Institute for Formal Models and Verification, Johannes Kepler University LinzAustria Active Automata Learning with Noisy Data: From Big to Small Data
Michael WandWand, Michael Dalle Molle Institute for Artificial Intelligence USI-SUPSISwitzerland Formally Explaining Neural Network Classification
Edward WangWang, Edward Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Hao WangWang, Hao Shenzhen Kaihong Digital Industry Development Co., Ltd.China Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Ji WangWang, Ji National University of Defense TechnologyChina Selective Concolic Testing EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Peixin WangWang, Peixin East China Normal University A Formal Framework for Predicting Distributed System Performance under Faults A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Renxi WangWang, Renxi MBZUAIUnited Arab Emirates A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Xudong WangWang, Xudong College of Computer Science and Technology, NationalUniversity of Defense TechnologyChina EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore AIPV Keynote: Conrad Watt A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Fabian WedenikWedenik, Fabian KNAPP AGAustria BDD-based Deadlock Prevention for Automated Guided Vehicles in Warehouse Logistics
Heike WehrheimWehrheim, Heike Carl von Ossietzky Universität Oldenburg / University of OldenburgGermany Towards Proving Liveness on Weak Memory Committee Member in Program Committee within the FM Research Track-track
Cheng WenWen, Cheng Xidian UniversityChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Cheng-Hui WengWeng, Cheng-Hui Nagoya UniversityJapan Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent
Lukas WesthofenWesthofen, Lukas DLR e.V. Institute of Systems Engineering for Future MobilityGermany Test Coverage of Automated Robotic Systems in Open World Environments
Hunter WhitlockWhitlock, Hunter The University of QueenslandAustralia Autograding Weakest Precondition Proofs and Dafny Specifications
John WickersonWickerson, John Imperial College LondonUnited Kingdom Automated Sketching and Repairing of Large Mechanised Proofs
Jeannette WingWing, Jeannette Columbia UniversityUnited States Selection Commitee Member in Journal-First Track Selection Committee within the FM Journal First-track
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Verifying Sampling Algorithms via Distributional Invariants
Kirsten WinterWinter, Kirsten The University of Queensland Committee Member in Program Committee within the FM Research Track-track
Burkhart WolffWolff, Burkhart University Paris-SaclayFrance Committee Member in Program Committee within the FM Research Track-track
Leon WongWong, Leon Rakuten Mobile, IncJapan Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment
Jim WoodcockWoodcock, Jim University of York Committee Member in Program Committee within the FM Research Track-track Teaching Unifying Theories of Programming
bozhi wuwu, bozhi Singapore Management UniversitySingapore Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems
Zhilin WuWu, Zhilin Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Can LLM Aid in Solving Constraints with Inductive Definitions?
X Chang XuXu, Chang Nanjing UniversityChina ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
Fanjiang XuXu, Fanjiang Institute of Software at Chinese Academy of SciencesChina Exact Moment Estimation of Stochastic Differential Dynamics
Mengwei XuXu, Mengwei University of NewcastleUnited Kingdom A System-of-Systems Case Study for the Verification of Composed Digital Twins Encoding BDI Syntax with Theories in Event-B
Qiyuan XuXu, Qiyuan Nanyang Technological University A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Y Ryota YamamotoYamamoto, Ryota National Institute of Technology, Tomakomai CollegeJapan Seven-Year Activity to Introduce B-Method to Japanese Technical College Students
Songyang YanYan, Songyang Xi'an Jiaotong University and The University of TokyoChina Robustness Semantics based Configuration Bug Fixing for Automated Driving Systems
Banri YanahamaYanahama, Banri Nyx FoundationJapan Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
Mengfei YangYang, Mengfei China Academy of Space TechnologyChina Automated ITL Specification Generation from Industrial Aerospace Requirements
Seungil YangYang, Seungil Japan Advanced Institute of Science and Technology (JAIST)Japan Relational Verification of Identity Disclosure Using Alloy
Yilong YangYang, Yilong Beihang UniversityChina Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Zhengfeng YangYang, Zhengfeng East China Normal UniversityChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Zijiang YangYang, Zijiang University of Science and Technology of China and Synkrotron, Inc.China Robustness Semantics based Configuration Bug Fixing for Automated Driving Systems
Furong YeYe, Furong LIACS, Leiden UniversityNetherlands FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
Mingsheng YingYing, Mingsheng Tsinghua University QSeqSim: A Symbolic Simulator for Qiskit While Loops using Sequential Quantum Circuits
Tomoyuki YokogawaYokogawa, Tomoyuki Okayama Prefectural UniversityJapan Workshops Co-Chair in Organizing Committee for FM 2026 Workshops Co-Chair in Workshop Committee within the FM Workshops Proposal-track
Nobuko YoshidaYoshida, Nobuko University of Oxford, UKUnited Kingdom AIPV Keynote: Nobuko Yoshida, Resilient Distributed Intelligent Swarms and Safeguarded AI: Programming Models and Runtime Guarantees
Emily YuYu, Emily Leiden UniversityNetherlands Quantitative Monitoring of Signal First-Order Logic Certifying Constraints in Hardware Model Checking
Shenghao YuanYuan, Shenghao Zhejiang UniversityChina Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Z Xia ZengZeng, Xia Southwest UniversityChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Naijun ZhanZhan, Naijun Peking University; Zhongguancun LaboratoryChina Exact Moment Estimation of Stochastic Differential Dynamics
Naijun ZhanZhan, Naijun Institute of Software, Chinese Academy of Sciences Committee Member in Program Committee within the FM Research Track-track
Naijun ZhanZhan, Naijun Peking University; Zhongguancun LaboratoryChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Guanqin ZhangZhang, Guanqin University of New South Wales, SydneyAustralia Mining Verdict Boundaries for Neural Network Verification Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Guofeng ZhangZhang, Guofeng College of Computer, National University of Defense TechnologyChina Selective Concolic Testing EUF-based Solving Dyck-Reachability with Applications to Static Analysis
Jianyuan ZhangZhang, Jianyuan Xi'an Jiaotong UniversityChina Fast SMT-Based Fault Tolerance Verification for Wide Area Networks
Lei ZhangZhang, Lei University of Maryland Baltimore CountyUnited States Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Min ZhangZhang, Min East China Normal UniversityChina A Formal Framework for Predicting Distributed System Performance under Faults Committee Member in Program Committee within the FM Research Track-track
Peng ZhangZhang, Peng Xi'an Jiaotong UniversityChina Fast SMT-Based Fault Tolerance Verification for Wide Area Networks
Tianxiong ZhangZhang, Tianxiong Chair of Software Technology, Technische Universität DresdenGermany Towards a Bigraph-Based Digital Twin Framework for Multi-UAV Coordination in AAM
Xiaodong ZhangZhang, Xiaodong University of Chinese Academy of Science Robustness Semantics based Configuration Bug Fixing for Automated Driving Systems
Xindi ZhangZhang, Xindi Institute of Software / CAS ChinaChina FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
Yufeng ZhangZhang, Yufeng Hunan UniversityChina Selective Concolic Testing
Zhenya ZhangZhang, Zhenya Kyushu UniversityJapan Session Chair of Session 5: Logic and Semantics (part of FM Research Track) Mining Verdict Boundaries for Neural Network Verification Committee Member in Program Committee within the FM Research Track-track
Haiyan ZhaoZhao, Haiyan Peking UniversityChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Hanrui ZhaoZhao, Hanrui National University of Defense TechnologyChina Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification
Junfeng ZhaoZhao, Junfeng Inner Mongolia University Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Tianqi ZhaoZhao, Tianqi Zhongguancun LaboratoryChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Xiaofei ZhaoZhao, Xiaofei Lanzhou Petrochemical University of Vocational TechnologyChina Correct-by-Construction Dynamic Reachability: A Galois-Connected Approach to Bidirected Dyck Languages
Zicen ZhaoZhao, Zicen Kyushu UniversityJapan Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Kevin ZhouZhou, Kevin National Institute of InformaticsJapan Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking Committee Member in Artifact Evaluation Committee within the FM Artifact Evaluation-track
Minghui ZhouZhou, Minghui Peking UniversityChina Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Yi ZhouZhou, Yi Shanghai Jiao Tong UniversityChina Array-Carrying Symbolic Execution for Function Contract Generation
Yuhao ZhouZhou, Yuhao Towards Language Model Guided TLA+ Proof Automation
Zhou ZhouZhou, Zhou East China Normal UniversityChina A Formal Framework for Predicting Distributed System Performance under Faults
Ziwei ZhouZhou, Ziwei East China Normal UniversityChina A Formal Framework for Predicting Distributed System Performance under Faults
Daniel ZilkenZilken, Daniel RWTH Aachen UniversityGermany Verifying Sampling Algorithms via Distributional Invariants
Wolf ZimmermannZimmermann, Wolf Martin-Luther-University Halle-WittenbergGermany Automatic Assessment and Feedback on Undergraduates’ Structural Induction Proofs
Ö Peter ÖlveczkyÖlveczky, Peter University of OsloNorway Committee Member in Program committee within the FM Doctoral Symposium-track