1,553 papers · page 2 of 78
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata ( $$1$$ -DTA). Although there is only one clock, distinct automata may reset it differently along the same word. This adds a significant challenge in the search fo…
SMTScope: Automated and Efficient Analysis of SMT Traces
SMT solvers enable the automated verification of complex software, but they frequently also cause performance problems, proof brittleness, and spurious errors. Debugging such issues is challenging because it is difficult to understand and predict how the solver’s complex algorith…
On Deciding Constant Runtime of Linear Loops
Incremental Forward Reasoning for White-Box Proof Search
Several proof assistants provide automation tactics based on tableau-style tree search, such as Isabelle’s and Rocq’s auto and Lean’s Aesop. In this setting we consider forward rules, which apply a given theorem, say, $$A \rightarrow B \rightarrow C$$ , to any goal containing hyp…
Verifying Floating-Point Programs in Stainless
ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics
Robust Verification of Concurrent Stochastic Games
Autonomous systems often operate in multi-agent settings and need to make concurrent, strategic decisions, typically in uncertain environments. Verification and control problems for these systems can be tackled with concurrent stochastic games (CSGs), but this model requires tran…
Modular Attractor Acceleration in Infinite-State Games
Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent accel…
Revisiting Stateful Partial-Order Reduction
MightyPPL: Model Checking MITL with Past and Pnueli Modalities
Metric Interval Temporal Logic ( $$\textsf {MITL} $$ ) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using $$\textsf {MITL} $$ in verification tasks, however, have notable drawbacks: they either support only l…
Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses - (Competition Contribution)
BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
We propose a technique that combines a bdd -based solver for quantified bit-vector formulas with an arbitrary other solver. The main idea is to employ the bdd -based solver on subformulas of the problem and then add the obtained information back to the original formula. The techn…
EvolveGen : Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a co…
Multiple Long-Run and ømega-Regular Objectives in MDPs
We consider Markov decision processes (MDPs) with three types of objectives: (1) the probability of satisfying an $$\omega $$ -regular objective, (2) the expected long-run average (LRA) reward, and (3) the probability that the long-run average reward exceeds a given threshold. Al…
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees
Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities
Parallel SMT Solving via Iterative Tree Partitioning
We present a novel algorithm for parallel solving of SMT problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in pri…
Enumerating Choice Terms in Model-Based Quantifier Instantiation
Satisfiability modulo theories (SMT) solvers are widely used for determining the satisfiability of logical formulas with respect to background theories. SMT solvers are traditionally based on first-order logic, but some also support higher-order logic. Recently, Kondylidou et al.…