Author name cluster

Laura Kovács

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

19 papers

2 author rows

FormaliSE Conference 2025 Conference Paper

Llm-Based Generation of Weakest Preconditions and Precise Array Invariants

Daragh King
Vasileios Koutavas
Laura Kovács

The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas such as software verification and runtime error-checking. For programs containing loops, WP generation critically depends upon synthesizing loop invariants that are inductive in nature; these WPs then essentially embed the inductive properties required for program verification. This paper investigates the use of Large Language Models (LLMs) to generate WPs (and accompanying loop invariants) in order to prove the correctness of nondeterministic programs containing arrays, loops, and arithmetic. Specifically, we employ several models of ChatGPT to derive the WPs and invariants for the aforementioned programs. We then compare these LLM-derived WPs and invariants to their provable counterparts obtained by the MaxPrANQ tool. We find that the quality of the LLM-derived results can vary greatly and is highly dependent on the underlying model used by ChatGPT. This variance in performance propels us to outline directions for future work and discuss how LLMs and formal-tools can complement one another in generating valid WPs and strong invariants.

SAT Conference 2024 Conference Paper

Lazy Reimplication in Chronological Backtracking

Robin Coutelier
Mathias Fleury
Laura Kovács

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.

LPAR Conference 2024 Conference Paper

Rewriting and Inductive Reasoning

Márton Hajdú
Laura Kovács
Michael Rawson 0001

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 miss- ing crucial consequences. We therefore extend the superposition calculus with rewriting- based techniques to generate sufficient consequences for automating induction in satura- tion. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

LPAR Conference 2024 Conference Paper

Saturating Sorting without Sorts

Pamina Georgiou
Márton Hajdú
Laura Kovács

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 focus- ing 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 induction in saturation. We advocate a compositional approach for automating proofs by induction re- quired 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 satu- ration. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort.

LPAR Conference 2024 Conference Paper

Scaling CheckMate for Game-Theoretic Security

Sophie Rain
Lea Salome Brugger
Anja Petkovic Komel
Laura Kovács
Michael Rawson 0001

We present the CheckMate tool for automated verification of game-theoretic secu- rity properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game- theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate’s input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

LPAR Conference 2024 Conference Paper

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

Johannes Schoisswohl
Laura Kovács
Konstantin Korovin

We introduce Virtual Integer-Real Arithmetic Substitution (Viras), a quantifier elim- ination procedure for deciding quantified linear mixed integer-real arithmetic problems. Viras combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that Viras gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

MFCS Conference 2023 Conference Paper

Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Laura Kovács

Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al. , 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al. , 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al. , 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al. , 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].

LPAR Conference 2023 Conference Paper

Refining Unification with Abstraction

Ahmed Bhayat
Konstantin Korovin
Laura Kovács
Johannes Schoisswohl

Automated reasoning with theories and quantifiers is a common demand in formal methods. A major challenge that arises in this respect comes with rewriting/simplifying terms that are equal with respect to a background first-order theory T, as equality reasoning in this context requires unification modulo T. We introduce a refined algorithm for unification with abstraction in T, allowing for a fine-grained control of equality constraints and substitutions introduced by standard unification with abstraction approaches. We experimentally show the benefit of our approach within first-order linear rational arithmetic.

LPAR Conference 2023 Conference Paper

SMT Solving over Finite Field Arithmetic

Thomas Hader
Daniela Kaufmann
Laura Kovács

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.

TCS Journal 2022 Journal Article

Moment-based analysis of Bayesian network properties

Miroslav Stankovič
Ezio Bartocci
Laura Kovács

We use algebraic reasoning to translate Bayesian network (BN) properties into linear recurrence equations over statistical moments of BN variables. We show that this translation can always be done for various BNs, such as discrete, Gaussian, conditional linear Gaussian, and dynamic BNs. An important part of our work comes with representing BNs as while loops in probabilistic programs with polynomial assignments over random variables and parametrised distributions. We prove that closed-form summaries of probabilistic loops precisely characterize higher-order moments of BN variables. As such, we automatically solve several BN-related problems, including exact inference, sensitivity analysis, filtering, and computing the expected number of rejecting samples in sampling-based procedures. We evaluate our work on a number of BN benchmarks, using automated invariant generation within Prob-solvable loop analysis. This paper is an extended version of the “Analysis of Bayesian Networks via Prob-Solvable Loops” manuscript published at ICTAC 2020 [1].

LFMTP Workshop 2021 Workshop Paper

Automating Induction by Reflection

Johannes Schoisswohl
Laura Kovács

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.

LPAR Conference 2018 Conference Paper

Loop Analysis by Quantification over Iterations

Bernhard Gleiss
Laura Kovács
Simon Robillard

We present a framework to analyze and verify programs containing loops by using a first-order language of so-called extended expressions. This language can express both functional and temporal properties of loops. We prove soundness and completeness of our framework and use our approach to automate the tasks of partial correctness verification, termination analysis and invariant generation. For doing so, we express the loop semantics as a set of first-order properties over extended expressions and use theorem provers and/or SMT solvers to reason about these properties. Our approach supports full first-order reasoning, including proving program properties with alternation of quantifiers. Our work is implemented in the tool QuIt and successfully evaluated on benchmarks coming from software verification.

Highlights Conference 2018 Conference Abstract

Symbol Elimination for Program Analysis

Laura Kovács

ABSTRACT. In this talk I describe how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. I will first present how computer algebra methods, such as Groebner basis computation and symbolic summation help us in inferring properties of program loops with non-trivial arithmetic. I will then further extend our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, I will use saturation-based first-order theorem proving and extend first-order provers with support for program analysis. I will review some of our recent results on Craig interpolation and proving properties in the full first-order theories of data structures. Our work is implemented in the Vampire theorem prover and successfully applied on benchmarks from the software verification and automated reasoning communities.

CSL Conference 2017 Conference Paper

First-Order Interpolation and Grey Areas of Proofs (Invited Talk)

Laura Kovács

Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity.

LPAR Conference 2017 Conference Paper

First-Order Interpolation and Interpolating Proof Systems

Laura Kovács
Andrei Voronkov

It is known that one can extract Craig interpolants from so-called local proofs. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. However, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs: there are formulas having non-local proofs but no local proof. In this paper we investigate interpolant extraction from non-local refutations (proofs of contradiction) in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems: any such proof system should deal with formulas of arbitrary quantifier complexity. To search for alternatives for interpolating proof systems, we consider several variations on interpolation and local proofs. Namely, we give an algorithm for building interpolants from resolution refutations in logic without equality and discuss additional constraints when this approach can be also used for logic with equality. We finally propose a new direction related to interpolation via local proofs in first-order theories.

LPAR Conference 2015 Conference Paper

Reasoning About Loops Using Vampire in KeY

Wolfgang Ahrendt
Laura Kovács
Simon Robillard

Abstract We describe symbol elimination and consequence finding in the first-order theorem prover Vampire for automatic generation of quantified invariants, possibly with quantifier alternations, of loops with arrays. Unlike the previous implementation of symbol elimination in Vampire, our work is not limited to a specific programming language but provides a generic framework by relying on a simple guarded command representation of the input loop. We also improve the loop analysis part in Vampire by generating loop properties more easily handled by the saturation engine of Vampire. Our experiments show that, with our changes, the number of generated invariants is decreased, in some cases, by a factor of 20. We also provide a framework to use our approach to invariant generation in conjunction with pre- and post-conditions of program loops. We use the program specification to find relevant invariants as well as to verify the partial correctness of the loop. As a case study, we demonstrate how symbol elimination in Vampire can be used as an interface for realistic imperative languages, by integrating our tool in the KeY verification system, thus allowing reasoning about loops in Java programs in a fully automated way, without any user guidance.

LPAR Conference 2013 Conference Paper

Tree Interpolation in Vampire

Régis Blanc
Ashutosh Gupta
Laura Kovács
Bernhard Kragl

Abstract We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.

LPAR Conference 2012 Conference Paper

r-TuBound: Loop Bounds for WCET Analysis (Tool Paper)

Jens Knoop
Laura Kovács
Jakob Zwirchmayr

Abstract We describe the structure and the usage of a new software tool, called r-TuBound, for deriving symbolic loop iteration bounds in the worst-case execution time (WCET) analysis of programs. r-TuBound implements algorithms for pattern-based recurrence solving and program flow refinement, and it was successfully tested on a wide range of examples. The purpose of this article is to illustrate what r-TuBound can do and how it can be used to derive the WCET of programs.

LPAR Conference 2008 Conference Paper

Valigator: A Verification Tool with Bound and Invariant Generation

Thomas A. Henzinger
Thibaud Hottelier
Laura Kovács

Abstract We describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gröbner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.