Quantifying Information Leakage Using Model Counting (abstract)

Probabilistic Programming: A Guide for Verificationists (abstract)

Working as Intended: Surveillance Capitalism is not a Rogue Capitalism (abstract)

Improved Geometric Path Enumeration for Verifying ReLU Neural Networks (abstract)

An Abstraction-Based Framework for Neural Network Verification (abstract)

Verification of Deep Convolutional Neural Networks Using ImageStars (abstract)

Systematic Generation of Diverse Benchmarks for DNN Verifiers (abstract)

NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems (abstract)

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems (abstract)

Refinement for Structured Concurrent Programs (abstract)

Parameterized Verification of Systems with Global Synchronization and Guards (abstract)

Solver-aided Recency-Aware Replicated Objects (abstract)

Ivy: a Multi-Modal Verification Tool for Distributed Algorithms (abstract)

Automated and Scalable Verification of Integer Multipliers (abstract)

fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components (abstract)

Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing (abstract)

Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling (abstract)

SAW: A Tool for Safety Analysis of Weakly-hard Systems (abstract)

SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks (abstract)

Formal Verification of Libra Blockchain Smart Contracts (abstract)

The Move Prover (abstract)

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract (abstract)

Synthesis of Super-Optimized Smart Contracts using Max-SMT (abstract)

Stratified Abstraction of Access Control Policies (abstract)

Verification of Quantitative Hyperproperties Using Trace Enumeration Relations (abstract)

Validation of Abstract Side-Channel Models for Computer Architectures (abstract)

Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models (abstract)

Reachability Analysis using Message Passing over Tree Decompositions. (abstract)

A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation (abstract)

PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems (abstract)

Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI (abstract)

AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks (abstract)

Global Guidance for Local Generalization in Model Checking (abstract)

Towards Model Checking Real-World Software-Defined Networks (abstract)

Action-Based Model Checking: Logic, Automata, and Reduction (abstract)

Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata (abstract)

RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft (abstract)

AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (abstract)

Towards Robust Artificial Intelligence via Spec-consistent Machine Learning (abstract)

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic (abstract)

Reasoning over Permissions Regions in Concurrent Separation Logic (abstract)

Approximate Counting of Minimal Unsatisfiable Subsets (abstract)

Nonlinear Craig Interpolant Generation (abstract)

Recursive Data Structures in SPARK (abstract)

Unbounded-Time Safety Verification of Stochastic Differential Dynamics (abstract)

Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games (abstract)

Global PAC Bounds for Learning Discrete Time Markov Chains (abstract)

STMC: Statistical Model Checker with Stratified and Antithetic Sampling (abstract)

Certifying Certainty and Uncertainty in Approximate Membership Query Structures (abstract)

Realizing Omega-regular Hyperproperties (abstract)

AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems (abstract)

Code2Inv: A Deep Learning Framework for Program Verification (abstract)

Maximum Causal Entropy Specification Inference from Demonstrations (abstract)

Automata Tutor v3 (abstract)

Manthan: A Data-Driven Approach for Boolean Function Synthesis (abstract)

The Reactive Synthesis Competition (SYNTCOMP 2020) (abstract)

Good Enough Synthesis (abstract)

TarTar: A Timed Automata Repair Tool (abstract)

Synthesizing JIT Compilers for In-Kernel DSLs (abstract)

Program Synthesis using Deduction-Guided Reinforcement Learning (abstract)

Decidable Synthesis of Programs with Uninterpreted Functions (abstract)

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling (abstract)

Symbolic Partial-Order Execution for Testing Multi-Threaded Programs (abstract)

Root Causing Linearizability Violations (abstract)

Must Fault Localization For Program Repair (abstract)

MetaVal: Witness Validation via Verification (abstract)

Qualitative Controller Synthesis for Consumption Markov Decision Processes (abstract)

Stochastic Games with Lexicographic Reachability-Safety Objectives (abstract)

Optimistic Value Iteration (abstract)

PrIC3: Property Directed Reachability for MDPs (abstract)

PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time (abstract)