Symbolic Register Automata (abstract)

Abstraction Refinement Algorithms for Timed Automata (abstract)

Fast algorithms for handling diagonal constraints in timed automata (abstract)

Safety and co-safety comparator automata for discounted-sum inclusion (abstract)

Clock Bound Repair for Timed Systems (abstract)

Automated Hypersafety Verification (abstract)

Verifying Hyperliveness (abstract)

Quantitative Mitigation of Timing Side Channels (abstract)

Property Directed Self Composition (abstract)

Security-Aware Synthesis Using Delayed-Action Games (abstract)

Automated Synthesis of Secure Platform Mappings (abstract)

Synthesizing Approximate Implementations for Unrealizable Specifications (abstract)

Quantified Invariants via Syntax-Guided-Synthesis (abstract)

Efficient Synthesis with Probabilistic Constraints (abstract)

Membership-based Synthesis of Linear Hybrid Automata (abstract)

Overfitting in Synthesis: Theory and Practice (abstract)

Proving Unrealizability for Syntax-Guided Synthesis (abstract)

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (abstract)

When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol (abstract)

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (abstract)

Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (abstract)

Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (abstract)

StreamLAB: Stream-based Monitoring of Cyber-Physical Systems (abstract)

Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (abstract)

The Marabou Framework for Verification and Analysis of Deep Neural Networks (abstract)

Probabilistic Bisimulation for Parameterized Systems (abstract)

Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks (abstract)

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games (abstract)

Symbolic Monitoring against Specifications Parametric in Time and Data (abstract)

STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis (abstract)

Local and Compositional Reasoning For Optimized Reactive Systems (abstract)

Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach (abstract)

Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis (abstract)

Temporal Stream Logic: Synthesis beyond the Bools (abstract)

Run-Time Optimization for Learned Controllers through Quantitative Games (abstract)

Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations (abstract)

Satisfiability Checking for Mission-Time LTL (abstract)

High-Level Abstractions for Simplifying Extended String Constraints in SMT (abstract)

Alternating Automata Modulo First Order Theories (abstract)

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (abstract)

CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (abstract)

Incremental Determinization for Quantifier Elimination and Functional Synthesis (abstract)

Loop Summarization with Rational Vector Addition Systems (abstract)

Invertibility Conditions for Floating-Point Formulas (abstract)

Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (abstract)

Icing: Supporting Fast-math Style Optimizations in a Verified Compiler (abstract)

Sound Approximation of Programs with Elementary Functions (abstract)

Formal verification of quantum algorithms using quantum Hoare logic (abstract)

SecCSL: Security Concurrent Separation Logic (abstract)

Reachability Analysis for AWS-based Networks (abstract)

Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics (abstract)

Gradual Consistency Checking (abstract)

Checking Robustness Against Snapshot Isolation (abstract)

Efficient verification of network fault tolerance via counterexample-guided refinement (abstract)

On the Complexity of Checking Consistency for Replicated Data Types (abstract)

Communication-closed asynchronous protocols (abstract)

Interpolating Strong Induction (abstract)

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (abstract)

Inferring Inductive Invariants from Phase Structures (abstract)

Termination of Triangular Integer Loops is Decidable (abstract)

AliveInLean: A Verified LLVM Peephole Optimization Verifier (abstract)

Automated Parameterized Verification of CRDTs (abstract)

What's wrong with on-the-fly partial order reduction (abstract)

Integrating Formal Schedulability Analysis into a Verifed OS Kernel (abstract)

Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS (abstract)

Violat: Generating Tests of Observational Refinement for Concurrent Objects (abstract)