Recent advances in SMT (abstract)

Recent advances in SMT (cont'd) (abstract)

Symbolic Execution and Probabilistic Reasoning (abstract)

Symbolic Execution and Probabilistic Reasoning (cont'd) (abstract)

Formal Methods, Machine Learning, and Cyber-Physical Systems (abstract)

Formal Methods, Machine Learning, and Cyber-Physical Systems (contd) (abstract)

Towards Verified Artificial Intelligence (abstract)

A Formally Verified Motion Planners for Autonomous Vehicles (abstract)

Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems (abstract)

Neural State Classification for Hybrid Systems (abstract)

What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction (abstract)

A Symbolic Algorithm for Lazy Synthesis of Eager Strategies (abstract)

Round-Bounded Control of Parameterized Systems (abstract)

Optimal Proofs for Linear Temporal Logic on Lasso Words (abstract)

A Fragment of Linear Temporal Logic for Universal Very Weak Automata (abstract)

EVE: A Tool for Temporal Equilibrium Analysis (abstract)

MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment (abstract)

Signal Convolution Logic (abstract)

DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks (abstract)

Bisimilarity Distances for Approximate Differential Privacy (abstract)

Synthesis in pMDPs: A Tale of 1001 Parameters (abstract)

PSense: Automatic Sensitivity Analysis for Probabilistic Programs (abstract)

Bounded Synthesis of Reactive Programs (abstract)

Reactive Synthesis of Register Transducers (abstract)

Maximum Realizability for Linear Temporal Logic Specifications (abstract)

Quantifiers on Demand (abstract)

Information Leakage in Arbiter Protocols (abstract)

Robustness Testing of Intermediate Verifiers (abstract)

Verifying Rust Programs with SMACK (abstract)

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode (abstract)

Z3 to the power of Azure and Azure to the power of Z3 (abstract)

Simulation Algorithms for Symbolic Automata (abstract)

Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces (abstract)

Ranking and Repulsing Supermartingales for Approximating Reachability (abstract)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility (abstract)

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets (abstract)

Modular Verification of Concurrent Programs via Sequential Model Checking (abstract)

Continuous-Time Markov Decisions based on Partial Exploration (abstract)

Temporal Logic Verification of Stochastic Systems Using Barrier Certificates (abstract)

Owl: A Library for \omega-Words, Automata, and LTL (abstract)

Accelerated Model Checking of Parametric Markov Chains (abstract)

SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems (abstract)