21,147 papers · page 19 of 1,058
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…
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…
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
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…
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
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…
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…
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
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.…
Abstract elided by the publisher.