arXiv subjects

Laura Kovács

Publications and source records attributed to Laura Kovács.

At least 19 recordsLinked to original sources

arXiv2026

Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support

We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping Theorem (OST) in the form of a specific precondition. This precondition requires the existence of an integrable dominating function for the martingale expression, which implies uniform integrability; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the runtime of a linear loop, then we can automatically synthesise polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to have unbounded support, which is a novel contribution to the field.

cs.LO↗

arXiv2026

Generalizing CDCL with Graph Backtracking

We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound and complete. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.

cs.LO↗

arXiv2026

Completeness of Synthesis under Realizability Assumptions using Superposition

Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one.

cs.LO↗

arXiv2026

Lean on Vampire Proofs (Short Paper)

Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampires output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean

cs.LO↗

arXiv2026

On Solving String Equations via Powers and Parikh Images

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

cs.LO↗

arXiv2026

Constraint Learning for Non-confluent Proof Search

Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.

cs.LO↗

arXiv2026

Polar: An Algebraic Analyzer for (Probabilistic) Loops

We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling algebraic recurrences that precisely capture the loop semantics. To this end, our work implements a variety of techniques to compute exact closed-forms of recurrences over higher-order moments of variables, infer invariants, and derive loop sensitivities with respect to unknown parameters. Polar can analyze probabilistic loops containing if-statements, polynomial arithmetic, and common probability distributions. By translating loop analysis into linear recurrence solving, Polar uses the derived closed-forms of recurrences to compute the strongest polynomial invariant or to infer parameter sensitivity. Polar is both sound and complete within well-defined programming model restrictions. Lifting any of these restrictions results in significant hardness limits of computation. To overcome computational burdens for the sake of efficiency, Polar also provides incomplete but sound techniques to compute moments of combinations of variables.

cs.PL↗

arXiv2025

The Vampire Diary

During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling Vampire to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use Vampire in practice and review the main changes Vampire has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.

cs.LO↗

arXiv2025

Synthesis Benchmarks for Automated Reasoning

Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $\forall\exists$-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis.

cs.LO↗

arXiv2025

Positive Almost-Sure Termination of Polynomial Random Walks

The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure termination (AST), while also providing quantitative answers via positive almost-sure termination (PAST) on the expected number of steps until termination. While every program which is PAST is AST, the converse is not true. The symmetric random walk with constant step size is a prominent example of a program that is AST but not PAST. In this paper we show that a more general class of polynomial random walks is PAST. Our random walks implement a step size that is polynomially increasing in the number of loop iterations and have a constant probability $p$ of choosing either branch. We decide that such programs are PAST when the degree of the polynomial is higher than both the degree of the drift and a threshold $d_\text{min}(p)$. Our approach does not use proof rules, nor auxiliary arithmetic expressions, such as martingales or invariants. Rather, we establish an inductive bound for the cumulative distribution function of the loop guard, based on which PAST is proven. We implemented the approximation of this threshold, by combining genetic programming, algebraic reasoning and linear programming.

cs.LO↗

arXiv2025

Term Ordering Diagrams

The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) for discovering redundant clauses and inferences. Implementing term orderings is however challenging. While KBO comparisons can be performed in linear time and LPO checks in quadratic time, using the best known algorithms for these orders is not enough. Indeed, our experiments show that for some examples term ordering checks may use about 98% of the overall proving time. The reason for this is that some equalities that cannot be ordered can become ordered after applying a substitution (post-ordered), and we have to check for post-ordering repeatedly for the same equalities. In this paper, we show how to improve post-ordering checks by introducing a new data structure called term ordering diagrams, in short TODs, which creates an index for these checks. We achieve efficiency by lazy modifications of the index and by storing and reusing information from previously performed checks to speed up subsequent checks. Our experiments demonstrate efficiency of TODs.

cs.LO↗

arXiv2025

Partial Redundancy in Saturation

Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We improve redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas, which is more powerful than the standard notion: there are both clauses and inferences that are redundant when we use our notions and not redundant when we use standard notions. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses. Our calculus is refutationally complete and is strong enough to capture some standard restrictions of the superposition calculus. We discuss the implementation of the calculus in the theorem prover Vampire. Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire.

cs.LO↗

arXiv2025

Lazy Reimplication in Chronological Backtracking

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.

cs.LO↗

arXiv2024

SAT Solving for Variants of First-Order Subsumption

Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system verification, program synthesis, and cybersecurity. Automation in these domains crucially depends on the efficiency of the underlying reasoners towards finding proofs and/or counterexamples of the task to be enforced. In order to gain efficiency, automated reasoners use dedicated proof rules to keep proof search tractable. To this end, (variants of) subsumption is one of the most important proof rules used by automated reasoners, ranging from SAT solvers to first-order theorem provers and beyond. It is common that millions of subsumption checks are performed during proof search, necessitating efficient implementations. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem provers involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden. In this paper we argue that the integration of a dedicated SAT solver opens up new venues for efficient implementations of first-order subsumption and related rules. We show that, by using a flexible learning approach to choose between various SAT encodings of subsumption variants, we greatly improve the scalability of first-order theorem proving. Our experimental results demonstrate that, by using a tailored SAT solver within first-order reasoning, we gain a large speedup in solving state-of-the-art benchmarks.

cs.LO↗

arXiv2024

(Un)Solvable Loop Analysis

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

cs.PL↗

arXiv2024

PolySAT: Word-level Bit-vector Reasoning in Z3

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.

cs.LO↗

arXiv2024

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver

This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2's frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.

cs.LO↗

arXiv2024

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.

cs.CR↗