Anytime Algorithms for MaxSAT and Beyond (abstract)

Formal Verification for Natural and Engineered Biological Systems (abstract)

Tutorial on Word-Level Model Checking (abstract)

Effective System Level Liveness Verification (abstract)

Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration (abstract)

A Theoretical Framework for Symbolic Quick Error Detection (abstract)

Runtime Verification on FPGAs with LTLf Specifications (abstract)

Distributed Bounded Model Checking (abstract)

EUFicient Reachability for Software with Arrays (abstract)

Thread-modular Counter Abstraction for Parameterized Program Safety (abstract)

Incremental Verification by SMT-based Summary Repair (abstract)

How testable is business software? (abstract)

Reactive Synthesis from Extended Bounded Response LTL Specifications (abstract)

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces (abstract)

Learning Properties in LTL \cap ACTL from Positive Examples Only (abstract)

Automating Compositional Analysis of Authentication Protocols (abstract)

Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation (abstract)

Parallelization Techniques for Verifying Neural Networks (abstract)

Formal Methods with a Touch of Magic (abstract)

ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks (abstract)

Automating Modular Verification of Secure Information Flow (abstract)

Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost (abstract)

Model Checking Software-Defined Networks with Flow Entries that Time Out (abstract)

Using model checking tools to triage the severity of security bugs in the Xen hypervisor (abstract)

From Correctness to High Quality (abstract)

Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning (abstract)

On Optimizing a Generic Function in SAT (abstract)

Ternary Propagation-Based Local Search for More Bit-Precise Reasoning (abstract)

Reductions for Strings and Regular Expressions Revisited (abstract)

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

(Dual) Projected Propositional Model Counting and Enumeration without Repetition (abstract)

Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction (abstract)

Specification Synthesis using Constrained Horn Clauses (abstract)

Compositional Adviser-Strategy Synthesis for Multi-Agent Systems (abstract)

Modular Synthesis of Reactive Systems (abstract)

Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease (abstract)

Formal Threat Modeling in the Cloud (abstract)

SWITSS: Computing Small Witnessing Subsystems (abstract)

Smart Induction for Isabelle/HOL (Tool Paper) (abstract)

Trace Logic for Inductive Loop Reasoning (abstract)

The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus (abstract)