arXiv subjects

Laura Kovács

Publications and source records attributed to Laura Kovács.

At least 37 records · Page 2Linked to original sources

arXiv2024

Saturating Sorting without Sorts

We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort.

cs.LO↗

arXiv2024

Rewriting and Inductive Reasoning

Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

cs.LO↗

arXiv2024

Getting Saturated with Induction

Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire. This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors.

cs.LO↗

arXiv2024

Program Synthesis in Saturation

We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors.

cs.LO↗

arXiv2024

Spanning Matrices via Satisfiability Solving

We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour of matrices, as we show that tree-like calculi have a number of drawbacks in the context of satisfiability solving. The matrix setting permits numerous global refinements of the basic connection calculus. We also show that a suitably-refined calculus is a decision procedure for the Bernays-Schönfinkel class.

cs.LO↗

arXiv2024

Linear Loop Synthesis for Quadratic Invariants

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

cs.LO↗

arXiv2024

SAT-Based Subsumption Resolution

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover Vampire, and show that it is noticeably faster than the state of the art.

cs.LO↗

arXiv2023

Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs

We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century. While the strongest polynomial invariants are computable for affine loops, for polynomial loops the problem remained wide open. As an intermediate result of independent interest, we prove that reachability for discrete polynomial dynamical systems is Skolem-hard as well. Furthermore, we generalize the notion of invariant ideals and introduce moment invariant ideals for probabilistic programs. With this tool, we further show that the strongest polynomial moment invariant is (i) uncomputable, for probabilistic loops with branching statements, and (ii) Skolem-hard to compute for polynomial probabilistic loops without branching statements. Finally, we identify a class of probabilistic loops for which the strongest polynomial moment invariant is computable and provide an algorithm for it.

cs.PL↗

arXiv2023

Automated Sensitivity Analysis for Probabilistic Loops

We present an exact approach to analyze and quantify the sensitivity of higher moments of probabilistic loops with symbolic parameters, polynomial arithmetic and potentially uncountable state spaces. Our approach integrates methods from symbolic computation, probability theory, and static analysis in order to automatically capture sensitivity information about probabilistic loops. Sensitivity information allows us to formally establish how value distributions of probabilistic loop variables influence the functional behavior of loops, which can in particular be helpful when choosing values of loop variables in order to ensure efficient/expected computations. Our work uses algebraic techniques to model higher moments of loop variables via linear recurrence equations and introduce the notion of sensitivity recurrences. We show that sensitivity recurrences precisely model loop sensitivities, even in cases where the moments of loop variables do not satisfy a system of linear recurrences. As such, we enlarge the class of probabilistic loops for which sensitivity analysis was so far feasible. We demonstrate the success of our approach while analyzing the sensitivities of probabilistic loops.

cs.PL↗

arXiv2023

From Polynomial Invariants to Linear Loops

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verification of program loops. The problem of generating loop invariants; in particular, invariants described by polynomial relations (so called polynomial invariants), is therefore one of the hardest problems in software verification. In this paper we advocate an alternative solution to invariant generation. Rather than inferring invariants from loops, we synthesise loops from invariants. As such, we generate loops that satisfy a given set of polynomials; in other words, our synthesised loops are correct by construction. Our work turns the problem of loop synthesis into a symbolic computation challenge. We employ techniques from algebraic geometry to synthesise loops whose polynomial invariants are described by pure difference binomials. We show that such complex polynomial invariants need ``only'' linear loops, opening up new venues in program optimisation. We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials. Importantly, we introduce an algorithmic approach that constructs linear loops from such polynomial invariants, by generating linear recurrence sequences that have specified algebraic relations among their terms.

cs.LO↗

arXiv2023

SMT Solving over Finite Field Arithmetic

Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post-quantum cryptography. Solving polynomial systems is also one of the most difficult problems in mathematics. In this paper, we propose an automated reasoning procedure for deciding the satisfiability of a system of non-linear equations over finite fields. We introduce zero decomposition techniques to prove that polynomial constraints over finite fields yield finite basis explanation functions. We use these explanation functions in model constructing satisfiability solving, allowing us to equip a CDCL-style search procedure with tailored theory reasoning in SMT solving over finite fields. We implemented our approach and provide a novel and effective reasoning prototype for non-linear arithmetic over finite fields.

cs.LO↗

arXiv2022

This Is the Moment for Probabilistic Loops

We present a novel static analysis technique to derive higher moments for program variables for a large class of probabilistic loops with potentially uncountable state spaces. Our approach is fully automatic, meaning it does not rely on externally provided invariants or templates. We employ algebraic techniques based on linear recurrences and introduce program transformations to simplify probabilistic programs while preserving their statistical properties. We develop power reduction techniques to further simplify the polynomial arithmetic of probabilistic programs and define the theory of moment-computable probabilistic loops for which higher moments can precisely be computed. Our work has applications towards recovering probability distributions of random variables and computing tail probabilities. The empirical evaluation of our results demonstrates the applicability of our work on many challenging examples.

cs.PL↗

arXiv2022

Towards a Game-Theoretic Security Analysis of Off-Chain Protocols

Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.

cs.CR↗

arXiv2022

Algebra-Based Reasoning for Loop Synthesis

Provably correct software is one of the key challenges of our software-driven society. Program synthesis -- the task of constructing a program satisfying a given specification -- is one strategy for achieving this. The result of this task is then a program which is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure. We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, encoding thus program loops with affine operations among program variables. We turn the task of loop synthesis into a polynomial constraint problem, by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.

cs.LO↗

arXiv2022

Solving Invariant Generation for Unsolvable Loops

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. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

cs.PL↗

arXiv2022

Distribution Estimation for Probabilistic Loops

We present an algorithmic approach to estimate the value distributions of random variables of probabilistic loops whose statistical moments are (partially) known. Based on these moments, we apply two statistical methods, Maximum Entropy and Gram-Charlier series, to estimate the distributions of the loop's random variables. We measure the accuracy of our distribution estimation by comparing the resulting distributions using exact and estimated moments of the probabilistic loop, and performing statistical tests. We evaluate our method on several probabilistic loops with polynomial updates over random variables drawing from common probability distributions, including examples implementing financial and biological models. For this, we leverage symbolic approaches to compute exact higher-order moments of loops as well as use sampling-based techniques to estimate moments from loop executions. Our experimental results provide practical evidence of the accuracy of our method for estimating distributions of probabilistic loop outputs.

stat.CO↗

arXiv2021

The Probabilistic Termination Tool Amber

We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber combines martingale theory with properties of asymptotic bounding functions and implements relaxed versions of existing probabilistic termination proof rules to prove/disprove (positive) almost sure termination of probabilistic loops. Amber supports programs parameterized by symbolic constants and drawing from common probability distributions. Our experimental comparisons give practical evidence of Amber outperforming existing state-of-the-art tools.

cs.PL↗

arXiv2021

Automating Induction by Reflection

Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires an infinite number of axioms, which is not a feasible input to a computer-aided theorem prover requiring a finite input. Mathematical practice is to specify these infinite sets of axioms as axiom schemes. Unfortunately these schematic definitions cannot be formalized in first-order logic, and therefore not supported as inputs for first-order theorem provers. In this work we introduce a new method, inspired by the field of axiomatic theories of truth, that allows to express schematic inductive definitions, in the standard syntax of multi-sorted first-order logic. Further we test the practical feasibility of the method with state-of-the-art theorem provers, comparing it to solvers' native techniques for handling induction.

cs.LO↗