Invited Paper
Linear Temporal Logic From Infinite to Finite Horizon
Automata Theory
Determinization and Limit-determinization of Emerson-Lei automata
Automatic discovery of fair paths in infinite-state transition systems
Certifying DFA Bounds for Recognition and Separation
Machine Learning for Formal Methods
AALpy: An Active Automata Learning Library
Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach
Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems
Theorem Proving and Tools
A Formal Semantics of the GraalVM Intermediate Representation
A Verified Decision Procedure for Orders in Isabelle/HOL
PJBDD: A BDD Library for Java and Multi-Threading
Model Checking
Live Synthesis
Faster Pushdown Reachability Analysis with Applications in Network Verification
Verifying Verified Code
Probabilistic Analysis
Probabilistic causes in Markov Chains
TEMPEST
Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
AQUA: Automated Quantized Inference for Probabilistic Programs
Software and Hardware Verification
Proving SIFA Protection of Masked Redundant Circuits
Verification by Gambling on Program Slices
Runtime Enforcement of Hyperproperties
System Synthesis and Approximation
Compositional Synthesis of Modular Systems
Event-B Refinement for Continuous Behaviours Approximation
Incorporating Monitors in Reactive Synthesis without Paying the Price
Verification of Machine Learning
pyNever: a Framework for Learning and Verification of Neural Networks
Property-Directed Verification and Robustness Certification of Recurrent Neural Networks.