Automata and Timed Systems
Symbolic Register Automata
Abstraction Refinement Algorithms for Timed Automata
Fast Algorithms for Handling Diagonal Constraints in Timed Automata
Safety and co-safety comparator automata for discounted-sum inclusion
Clock Bound Repair for Timed Systems
Verifying Asynchronous Interactions via Communicating Session Automata
Security and Hyperproperties
Verifying Hyperliveness
Quantitative Mitigation of Timing Side Channels
Property Directed Self Composition
Security-Aware Synthesis Using Delayed-Action Games
Automated Hypersafety Verification
Automated Synthesis of Secure Platform Mappings
Synthesis
Synthesizing Approximate Implementations for Unrealizable Specifications
Quantified Invariants via Syntax-Guided Synthesis
Efficient Synthesis with Probabilistic Constraints
Membership-based Synthesis of Linear Hybrid Automata
Overfitting in Synthesis: Theory and Practice
Proving Unrealizability for Syntax-Guided Synthesis
Model Checking
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-Agent Protocol
Extending NUXMV with Timed Transition Systems and Timed Temporal Properties
Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Cyber-physical Systems and Machine Learning
Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
The Marabou Framework for Verification and Analysis of Deep Neural Networks
Probabilistic Systems, Runtime Techniques
Probabilistic Bisimulation for Parameterized Systems
Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Symbolic Monitoring against Specifications Parametric in Time and Data
STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Dynamical, Hybrid, and Reactive Systems
Local and Compositional Reasoning For Optimized Reactive Systems
Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
Temporal Stream Logic: Synthesis beyond the Bools
Run-Time Optimization for Learned Controllers through Quantitative Games
Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations.