21,147 papers · page 19 of 1,058
Kyveli Doveri, Pierre Ganty, B. Srivathsan
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…
Jonás Fiala, Peter Müller
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…
Florian Frohn, Jürgen Giesl, Peter Giesl, Nils Lommen
Abstract elided by the publisher.
Xavier Généreux, Jannis Limperg
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…
Andrea Gilot, Axel Bergström, Eva Darulova
Abstract elided by the publisher.
Makoto Hamana, Kento Emoto
Abstract elided by the publisher.
Angel Y. He, David Parker
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…
Philippe Heim, Rayna Dimitrova
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…
Frédéric Herbreteau, Gérald Point, Gautham Viswanathan, Igor Walukiewicz
Abstract elided by the publisher.
Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya
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…
Karoliine Holter, Paulína Ayaziová, Simmo Saan, Jan Strejcek, Vesal Vojdani
Abstract elided by the publisher.
Jakub Horák, Martin Jonás
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…
Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang
Abstract elided by the publisher.
Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Alfons Laarman, Jingyi Mei
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…
Julius Ide, Joost-Pieter Katoen, Hannah Mertens, Tim Quatmann
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…
Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner
Abstract elided by the publisher.
Ali Rasim Kocal, Michael Schwarz, Simmo Saan, Helmut Seidl
Abstract elided by the publisher.
Tomás Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh, Natasha Sharygina
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…
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli
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.…
Lukas König, Christian Schildwächter, Michaela Klauck, Christian Heinzemann
Abstract elided by the publisher.