FM24: 26TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

This page contains an index consisting of author-provided keywords.

A
abstract interpretation	The Pyramid Of (Formal) Software Verification
Abstract State Machines	ASMETA tool set for rigorous system design
Acceleration	Integrating Loop Acceleration into Bounded Model Checking
Active Automata Learning	State Matching and Multiple References in Adaptive Active Automata Learning
Adaptive cruise control	Code-level Safety Verification for Automated Driving: A Case Study
Adaptive Learning	State Matching and Multiple References in Adaptive Active Automata Learning
Alloy	Alloy repair hint generation based on historical data
Android App Security	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
ASMETA	ASMETA tool set for rigorous system design
Attack graphs	Fast Attack Graph Defense Localization via Bisimulation
Automata learning	Stochastic Games for User Journeys
Automated driving	Code-level Safety Verification for Automated Driving: A Case Study
automated hints	Alloy repair hint generation based on historical data
Automated reasoning	The Business of Proof Satisfiability Modulo Theories: A Beginner's Tutorial
automated verification	Staged Specification Logic for Verifying Higher-Order Imperative Programs
Award	FME Fellowship Award
AWS Cloud	Automated Static Analysis of Quality of Service Properties of Communicating Systems
B
B method	B+ or how to model system properties in a formal software model
B-Method	B2SAT: A Bare-Metal Reduction of B to SAT
Backdoor-freeness	Certified Quantization Strategy Synthesis for Neural Networks
barrier certificates	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
BERT	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
binary decision diagrams	Understanding Synthesized Reactive Systems Through Invariants
Bisimulation	Fast Attack Graph Defense Localization via Bisimulation
bounded model checking	Automated Static Analysis of Quality of Service Properties of Communicating Systems Accurate Static Data Race Detection for C Integrating Loop Acceleration into Bounded Model Checking UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking The Pyramid Of (Formal) Software Verification
C
C/C++ versus RTL	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Cameleer	Practical Deductive Verification of OCaml Programs
Certified Quantization	Certified Quantization Strategy Synthesis for Neural Networks
Chairs	FM24 Opening
choreographies	Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last
Choreography	Automated Static Analysis of Quality of Service Properties of Communicating Systems
Clojure	Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last
Code generation	Extending Isabelle/HOL’s Code Generator with support for the Go programming language
Code generation from models	ASMETA tool set for rigorous system design
concurrency	Accurate Static Data Race Detection for C
Concurrent programs	Unifying Weak Memory Verification using Potentials
Configurable Program Analysis	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Conformal prediction	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Constrained Horn Clauses	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Constraint Solving	B2SAT: A Bare-Metal Reduction of B to SAT Learning Branching-Time Properties in CTL and ATL via Constraint Solving
container	fm-weck: Containerized Execution of Formal Methods Tools
context-bounded analysis	Accurate Static Data Race Detection for C
Continuous-state spaces	Partially Observable Stochastic Games with Neural Perception Mechanisms
CPAchecker	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Craig interpolation	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Cryptographic circuits	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
CSP	Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testin
Cutpoint graph	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
cvc5	Satisfiability Modulo Theories: A Beginner's Tutorial
Cyber-physical system	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Cyber-physical systems	A Tutorial on Stream-based Monitoring Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
D
Dafny	Free Facts: An Alternative to Inefficient Axioms in Dafny
data race detection	Accurate Static Data Race Detection for C
Data-driven model construction	Stochastic Games for User Journeys
Debugging	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
decision diagrams	Advancing Quantum Computing with Formal Methods
Deductive Software Verification	Practical Deductive Verification of OCaml Programs
Deductive verification	The Java Verification Tool KeY: A Tutorial Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems The Pyramid Of (Formal) Software Verification
Deep neural network verification	Code-level Safety Verification for Automated Driving: A Case Study
Delta-debugging	Chamelon : a delta-debugger for OCaml
Dempster-Shafer structures	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Directed Acyclic Graph	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Distributed Redundant Controllers	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Distributed Systems	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First)
Doctoral Symposium	On Time and Space (Of Humans) Thoughts on the interplay between corporate, government, and university R&D
Dynamic Logic	The Java Verification Tool KeY: A Tutorial
dynamic programming	CauMon: An Informative Online Monitor for Signal Temporal Logic
Dynamic temporal logic	Automated Static Analysis of Quality of Service Properties of Communicating Systems
E
Embedded systems	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
explainability	Understanding Synthesized Reactive Systems Through Invariants
F
Falsification	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Fault injection attacks	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
Fault Localization	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
Fault Tolerance	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Fellowship	FME Fellowship Award
floating-point	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
FM24	FM24 Opening
FME	FME Fellowship Award
Formal datapath verification	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Formal Equivalence Verification	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
formal methods	No risk, no fun: a tutorial on risk management Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems The Pyramid Of (Formal) Software Verification
formal methods in industry	B+ or how to model system properties in a formal software model
Formal Requirement Elicitation Tool	Formalising Requirements for Systems Verification
Formal safety verification	Code-level Safety Verification for Automated Driving: A Case Study
formal semantics	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
formal specification	Alloy repair hint generation based on historical data
Formal Verification	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms Free Facts: An Alternative to Inefficient Axioms in Dafny Software Verification with CPAchecker 3.0: Tutorial and User Guide Compositional Verification of Cryptographic Circuits against Fault Injection Attacks Formalising Requirements for Systems Verification
Formula-based Fault Localization	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
Functional languages	Chamelon : a delta-debugger for OCaml
Functional Programming	Practical Deductive Verification of OCaml Programs
Functional programs	Proving Functional Program Equivalence via Directed Lemma Synthesis
functional verification	The Pyramid Of (Formal) Software Verification
G
Game-Based Verification	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
generalized reactivity(1) synthesis	Understanding Synthesized Reactive Systems Through Invariants
Go programming language	Extending Isabelle/HOL’s Code Generator with support for the Go programming language
Gospel	Practical Deductive Verification of OCaml Programs
H
High-Concurrency systems	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
higher-order functions	Staged Specification Logic for Verifying Higher-Order Imperative Programs
homogenization	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Human-robot interaction	Formal Methods for Robotics and Human-Robot Interaction
Humans	On Time and Space (Of Humans)
Hybrid Systems	Switching Controller Synthesis for Hybrid Systems Against STL Formulas Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
hybrid workflows	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Hyperliveness	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
HyperLTL	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
I
Industrial applications	Thoughts on the interplay between corporate, government, and university R&D
Industry application	The Business of Proof
Industry day	Industry partner pitches
Information flow security	Detecting speculative execution vulnerabilities on weak memory models
intelligent tutoring system	Alloy repair hint generation based on historical data
Interactive Theorem Proving	Efficient Formally Verified Maximal End Component Decomposition for MDPs
interoperability	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
ISO standards	No risk, no fun: a tutorial on risk management
J
JasperTM C2RTL	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Java Modeling Language	The Java Verification Tool KeY: A Tutorial
Journal first	Extending rely-guarantee thinking to handle real-time scheduling (Journal first) RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first) FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First) Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems (Journal first)
L
L# algorithm	State Matching and Multiple References in Adaptive Active Automata Learning
learning from samples	DFAMiner: Mining minimal separating DFAs from labelled samples
Lemma synthesis	Proving Functional Program Equivalence via Directed Lemma Synthesis
Linear Arithmetic	A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
Linear Integer Arithmetics	A Local Search Algorithm for MaxSMT(LIA)
Linear Temporal Logic	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Local Search	A Local Search Algorithm for MaxSMT(LIA)
LTL	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
LTLf	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Löwenheim–Skolem theorem	The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
M
many-sorted logic	The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
Markov Decision Process	Efficient Formally Verified Maximal End Component Decomposition for MDPs
Mathematical Logic	The Business of Proof
Maximal End Components	Efficient Formally Verified Maximal End Component Decomposition for MDPs
Maximum Satisfiability	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
MaxSMT	A Local Search Algorithm for MaxSMT(LIA)
Mealy Machines	State Matching and Multiple References in Adaptive Active Automata Learning
Memory Safety	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Message-passing systems	Automated Static Analysis of Quality of Service Properties of Communicating Systems
minimal separating DFA	DFAMiner: Mining minimal separating DFAs from labelled samples
misconceptions	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Model Checking	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT) Learning Branching-Time Properties in CTL and ATL via Constraint Solving Software Verification with CPAchecker 3.0: Tutorial and User Guide Stochastic Games for User Journeys
Model validation	ASMETA tool set for rigorous system design
Model verification	ASMETA tool set for rigorous system design
Model-Based Diagnosis	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
Model-based testing	Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testin
Model-based verification	Code-level Safety Verification for Automated Driving: A Case Study
Multi-agent autonomous systems	Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems (Journal first)
multi-threaded programs	Accurate Static Data Race Detection for C
multiparty session typing	Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last
multitask PLC	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
N
neural networks	Certified Quantization Strategy Synthesis for Neural Networks A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Neural-network control	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Neuro-symbolic systems	Partially Observable Stochastic Games with Neural Perception Mechanisms
nuXmv	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
O
Oblivious Algorithms	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
OCaml	Practical Deductive Verification of OCaml Programs Chamelon : a delta-debugger for OCaml Safe and Easy Compile-Time Generative Programming
One-sided zero-sum games	Partially Observable Stochastic Games with Neural Perception Mechanisms
online monitoring	CauMon: An Informative Online Monitor for Signal Temporal Logic
Opacity	The Opacity of Timed Automata
Opening	FM24 Opening
over-approximation algorithms	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Owicki-Gries reasoning	Unifying Weak Memory Verification using Potentials
P
p-boxes	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Parameterized Systems	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Parameterized Verification	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Partially observable stochastic games	Partially Observable Stochastic Games with Neural Perception Mechanisms
Passive Learning	DFAMiner: Mining minimal separating DFAs from labelled samples Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Pattern-based Language	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Performance optimization	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
pitches	Industry partner pitches
PLC	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
PLC ST	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
Point-based value iteration	Partially Observable Stochastic Games with Neural Perception Mechanisms
Polynomial Programs	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
POSIX threads	Accurate Static Data Race Detection for C
Preimages	Certified Quantization Strategy Synthesis for Neural Networks
PRISM	Stochastic Games for User Journeys
Probabilistic Algorithms	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
Probabilistic Model Checking	Efficient Formally Verified Maximal End Component Decomposition for MDPs
probabilistic verification	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
probability bounds	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Program Analysis	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Program equivalence verification	Proving Functional Program Equivalence via Directed Lemma Synthesis
Program generation	Safe and Easy Compile-Time Generative Programming
program logic	Staged Specification Logic for Verifying Higher-Order Imperative Programs
Program performance	Safe and Easy Compile-Time Generative Programming
Program verification	The Java Verification Tool KeY: A Tutorial
Projection	A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
proof brittleness	Free Facts: An Alternative to Inefficient Axioms in Dafny
Proof calculus	Unifying Weak Memory Verification using Potentials
Prophecies	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
Python	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Q
Quality of Service (QoS)	Automated Static Analysis of Quality of Service Properties of Communicating Systems
quantifier elimination over reals	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Quantitative Attributes	Automated Static Analysis of Quality of Service Properties of Communicating Systems
Quantum Classifiers	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
quantum computing	Advancing Quantum Computing with Formal Methods
Quantum Machine Learning	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Quantum Noise	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
R
R&D	Thoughts on the interplay between corporate, government, and university R&D
Reach-Avoid	Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Reachability	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers Accurate Static Data Race Detection for C
Reachability Analysis	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
reactive synthesis	Understanding Synthesized Reactive Systems Through Invariants
really-guarantee	Extending rely-guarantee thinking to handle real-time scheduling (Journal first)
realt-time	Extending rely-guarantee thinking to handle real-time scheduling (Journal first)
realtime	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Reinforcement Learning	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
Requirements engineering	Formalising Requirements for Systems Verification
Resilience	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
Reusability	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
risk assessment	No risk, no fun: a tutorial on risk management
risk management	No risk, no fun: a tutorial on risk management
Robostar	Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testin
Robotic systems	RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first)
Robotics	Formal Methods for Robotics and Human-Robot Interaction
Robustness	Certified Quantization Strategy Synthesis for Neural Networks
Robustness Verification	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
round-off errors	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
runtime monitoring	A Tutorial on Stream-based Monitoring Runtime Verification in Real-Time with the Copilot Language: A Tutorial
runtime verification	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
S
Safety	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains B+ or how to model system properties in a formal software model
safety-critical systems	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
SAT Solving	B2SAT: A Bare-Metal Reduction of B to SAT
satisfiability modulo theories	Satisfiability Modulo Theories: A Beginner's Tutorial The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
SCADE	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Security analysis	Fast Attack Graph Defense Localization via Bisimulation
Security and Privacy	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
semidefinite programming	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Separability	Learning Branching-Time Properties in CTL and ATL via Constraint Solving
separating semialgebraic sets	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
sequentialisation	Accurate Static Data Race Detection for C
Service Level Agreement (SLA)	Automated Static Analysis of Quality of Service Properties of Communicating Systems
Set Propagation	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Set-Reprensentations	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Signal Temporal Logic	CauMon: An Informative Online Monitor for Signal Temporal Logic Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems Switching Controller Synthesis for Hybrid Systems Against STL Formulas
simulation	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
SMT solvers	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
SMT-based reasoning	Free Facts: An Alternative to Inefficient Axioms in Dafny
Software robustness	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Software testing	The Pyramid Of (Formal) Software Verification
Software tolerance	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Software verification	Efficient Formally Verified Maximal End Component Decomposition for MDPs Software Verification with CPAchecker 3.0: Tutorial and User Guide The Pyramid Of (Formal) Software Verification
Specification Mining	Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Speculative execution	Detecting speculative execution vulnerabilities on weak memory models
Spinlock backoff	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
sponsors	Industry partner pitches
State-based formal models	ASMETA tool set for rigorous system design
static analysis	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0 The Pyramid Of (Formal) Software Verification
Static program analysis	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
Stochastic games	Stochastic Games for User Journeys
Stream-based Specifications	A Tutorial on Stream-based Monitoring
Strongly Connected Components	Efficient Formally Verified Maximal End Component Decomposition for MDPs
sum-of-squares	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Switching Controller Synthesis	Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Symbolic Verification	B2SAT: A Bare-Metal Reduction of B to SAT
Synthesis	Formal Methods for Robotics and Human-Robot Interaction
T
Temporal Formalisms	On Time and Space (Of Humans)
temporal logic	Learning Branching-Time Properties in CTL and ATL via Constraint Solving Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Temporal Specification	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Test Case Generation	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Testing	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Theorem provers	Extending Isabelle/HOL’s Code Generator with support for the Go programming language
theorem proving	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
theory combination	The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
three-valued finite automata	DFAMiner: Mining minimal separating DFAs from labelled samples
Threshold Automata	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Timed automata	The Opacity of Timed Automata
Timed games	Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems (Journal first)
Timed opacity	The Opacity of Timed Automata
Tools	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python fm-weck: Containerized Execution of Formal Methods Tools
Transition Power Abstraction	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Tutorial	Satisfiability Modulo Theories: A Beginner's Tutorial Software Verification with CPAchecker 3.0: Tutorial and User Guide
U
uncertainty	No risk, no fun: a tutorial on risk management
understandability	Understanding Synthesized Reactive Systems Through Invariants
Unsafe Rust	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Unsafety	Integrating Loop Acceleration into Bounded Model Checking
usability	fm-weck: Containerized Execution of Formal Methods Tools
User journeys	Stochastic Games for User Journeys
user studies	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
V
Variable Elimination	A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
verification	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first) FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First)
Verified Verifiers	Efficient Formally Verified Maximal End Component Decomposition for MDPs
W
Weak memory models	Detecting speculative execution vulnerabilities on weak memory models Unifying Weak Memory Verification using Potentials
weighted model counting	Advancing Quantum Computing with Formal Methods
Z
zonotopes	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks

Disclaimer | Powered by EasyChair Smart Program