Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
Abstract elided by the publisher.
1,553 papers · page 3 of 78
SMT(LIA) Sampling with High Diversity
SMT sampling refers to the task of generating a set of satisfying assignments (samples) for a given SMT formula. An effective SMT sampler should be capable of producing samples with high diversity to maximize coverage of the solution space. However, most SMT samplers struggle to …
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques, which are not expressible in first-order logic. Among others, these include liveness verification a…
SWAT: Improvements to the Symbolic Executor (Competition Contribution)
Abstract elided by the publisher.
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
Abstract elided by the publisher.
Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, an important issue is the detection of attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the …
Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis
We develop error-tolerant quantum state discrimination(QSD) strategies that maintain reliable performance under moderate noise. Two complementary approaches are proposed: CrossQSD, which generalizes unambiguous discrimination with tunable confidence bounds to balance accuracy and…
DASA: Fully Gradient-Based Program Analysis (Competition Contribution)
Abstract elided by the publisher.
Faster Signature Refinement for Branching Bisimilarity Minimization
We present a new algorithm to efficiently minimize state spaces with respect to branching bisimilarity. Our approach combines signature-based refinement with Hopcroft’s “process-the-smaller-half” optimization to avoid unnecessary computation. This combination results in a concept…
Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution)
. We present advances we brought to Mopsa for SV-COMP 2026. Mopsa now supports a backward analysis mode which computes an under-approximation of the weakest liberal precondition for the alarms found during a verification pass, which generates an input harness to re-produce the in…
Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring
Abstract elided by the publisher.
Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
Abstract elided by the publisher.
EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution)
Abstract elided by the publisher.
Deconstructing Subset Construction - Reducing While Determinizing
Abstract elided by the publisher.
Bit-Precise Interpolation in Bitwuzla
Bitwuzla is a state-of-the-art SMT solver specialized in theories relevant to bit-precise reasoning. The main bit-vector solving procedure of Bitwuzla is based on bit-blasting, a reduction of bit-vector constraints to propositional logic (SAT). Until now, Bitwuzla did not support…
Efficient Verification of Lingua Franca Programs
Abstract elided by the publisher.
jMT: Testing Correctness of Java Memory Models
Folklore is often saying"The Java memory model is broken."Therefore, several approaches have proposed repairs, only to find new programs exhibiting unexpected, unintuitive behavior or the model forbidding standard compiler optimizations. The complexity of defining a memory model …
Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
SMT solvers are essential for applications in artificial intelligence, software verification, and optimisation. However, no single solver excels across all formula types, and different applications may require the use of different solvers. While the SMT-LIB language enables multi…
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems
Abstract elided by the publisher.
QSOLE: Automatic QBF Equivalence Checking
Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains su…