Showing 1–50 of 52 results for author: Kovács, L

PolySAT: Word-level Bit-vector Reasoning in Z3

Authors: Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kovács

Abstract: 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 p… ▽ More 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. △ Less

Submitted 7 June, 2024; originally announced June 2024.

Comments: Submitted to FMCAD 2024, https://fmcad.org/FMCAD24/

Graphs Unveiled: Graph Neural Networks and Graph Generation

Authors: László Kovács, Ali Jlidi

Abstract: One of the hot topics in machine learning is the field of GNN. The complexity of graph data has imposed significant challenges on existing machine learning algorithms. Recently, many studies on extending deep learning approaches for graph data have emerged. This paper represents a survey, providing a comprehensive overview of Graph Neural Networks (GNNs). We discuss the applications of graph neura… ▽ More One of the hot topics in machine learning is the field of GNN. The complexity of graph data has imposed significant challenges on existing machine learning algorithms. Recently, many studies on extending deep learning approaches for graph data have emerged. This paper represents a survey, providing a comprehensive overview of Graph Neural Networks (GNNs). We discuss the applications of graph neural networks across various domains. Finally, we present an advanced field in GNNs: graph generation. △ Less

Submitted 18 March, 2024; originally announced March 2024.

Scaling CheckMate for Game-Theoretic Security

Authors: Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovacs, Michael Rawson

Abstract: We present the CheckMate tool for automated verification of game-theoretic security 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… ▽ More We present the CheckMate tool for automated verification of game-theoretic security 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. △ Less

Submitted 13 June, 2024; v1 submitted 15 March, 2024; originally announced March 2024.

Saturating Sorting without Sorts

Authors: Pamina Georgiou, Márton Hajdu, Laura Kovács

Abstract: 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 specif… ▽ More 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. △ Less

Submitted 6 March, 2024; originally announced March 2024.

Rewriting and Inductive Reasoning

Authors: Márton Hajdu, Laura Kovács, Michael Rawson

Abstract: 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 conseq… ▽ More 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. △ Less

Submitted 29 February, 2024; originally announced February 2024.

Program Synthesis in Saturation

Authors: Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov

Abstract: 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, w… ▽ More 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. △ Less

Submitted 29 February, 2024; originally announced February 2024.

Comments: 23 pages; this is an extended version of the published paper

Journal ref: Automated Deduction - CADE 29. CADE 2023. Lecture Notes in Computer Science, vol 14132. Springer, Cham

Getting Saturated with Induction

Authors: Márton Hajdu, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov

Abstract: 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 presen… ▽ More 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. △ Less

Submitted 29 February, 2024; originally announced February 2024.

Comments: 26 pages; this is an extended version of the published paper

Journal ref: Principles of Systems Design 2022, Lecture Notes in Computer Science, vol 13660. Springer, Cham

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver

Authors: Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács

Abstract: 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… ▽ More 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. △ Less

Submitted 29 April, 2024; v1 submitted 27 February, 2024; originally announced February 2024.

Spanning Matrices via Satisfiability Solving

Authors: Clemens Eisenhofer, Michael Rawson, Laura Kovács

Abstract: 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 th… ▽ More 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. △ Less

Submitted 16 February, 2024; originally announced February 2024.

SAT-Based Subsumption Resolution

Authors: Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath

Abstract: 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. 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. △ Less

Submitted 31 January, 2024; originally announced January 2024.

Journal ref: Automated Deduction -- CADE 29 (2023). Lecture Notes in Computer Science vol 14132. Springer

Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, Anton Varonka

Abstract: 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 o… ▽ More 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. △ Less

Submitted 15 February, 2024; v1 submitted 8 October, 2023; originally announced October 2023.

Comments: Extended version of our conference paper accepted to STACS 2024

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

Authors: Julian Müllner, Marcel Moosbrugger, Laura Kovács

Abstract: 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… ▽ More 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. △ Less

Submitted 14 November, 2023; v1 submitted 20 July, 2023; originally announced July 2023.

Comments: Published at POPL 2024

(Un)Solvable Loop Analysis

Authors: Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič

Abstract: 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… ▽ More 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. △ Less

Submitted 4 March, 2024; v1 submitted 2 June, 2023; originally announced June 2023.

Comments: Extended version of the conference paper `Solving Invariant Generation for Unsolvable Loops' published at SAS 2022 (see also the preprint arXiv:2206.06943). We extended both the text and results. 36 pages

Automated Sensitivity Analysis for Probabilistic Loops

Authors: Marcel Moosbrugger, Julian Müllner, Laura Kovács

Abstract: 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 info… ▽ More 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. △ Less

Submitted 4 September, 2023; v1 submitted 24 May, 2023; originally announced May 2023.

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson

Abstract: 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 guaran… ▽ More 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. △ Less

Submitted 5 April, 2024; v1 submitted 20 May, 2023; originally announced May 2023.

SMT Solving over Finite Field Arithmetic

Authors: Thomas Hader, Daniela Kaufmann, Laura Kovács

Abstract: 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… ▽ More 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. △ Less

Submitted 15 May, 2023; v1 submitted 24 April, 2023; originally announced May 2023.

From Polynomial Invariants to Linear Loops

Authors: George Kenison, Laura Kovács, Anton Varonka

Abstract: 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 verif… ▽ More 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. △ Less

Submitted 24 May, 2023; v1 submitted 13 February, 2023; originally announced February 2023.

Comments: 18 pages. To Appear at ISSAC 2023

Algebra-Based Reasoning for Loop Synthesis

Authors: Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner, Laura Kovács

Abstract: 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 p… ▽ More 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. △ Less

Submitted 23 June, 2022; originally announced June 2022.

Comments: This paper is an extended version of the "Algebra-Based Loop Synthesis'' manuscript published at iFM 2020. arXiv admin note: substantial text overlap with arXiv:2004.11787

Solving Invariant Generation for Unsolvable Loops

Authors: Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič

Abstract: 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… ▽ More 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. △ Less

Submitted 14 June, 2022; originally announced June 2022.

This Is the Moment for Probabilistic Loops

Authors: Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci, Laura Kovács

Abstract: 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 probabili… ▽ More 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. △ Less

Submitted 20 December, 2022; v1 submitted 14 April, 2022; originally announced April 2022.

Comments: Published at OOPSLA 2022

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

Authors: Sophie Rain, Georgia Avarikioti, Laura Kovács, Matteo Maffei

Abstract: 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 p… ▽ More 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. △ Less

Submitted 24 October, 2022; v1 submitted 15 September, 2021; originally announced September 2021.

Comments: This submission is the extended version of our CSF 2023 paper "Towards a Game-Theoretic Security Analysis of Off-Chain Protocols"

The Probabilistic Termination Tool Amber

Authors: Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács

Abstract: 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 probabilisti… ▽ More 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. △ Less

Submitted 27 July, 2021; originally announced July 2021.

Comments: Accepted to FM 2021

Automating Induction by Reflection

Authors: Johannes Schoisswohl, Laura Kovács

Abstract: 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 th… ▽ More 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. △ Less

Submitted 15 July, 2021; originally announced July 2021.

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376. A full version of this paper appears at arXiv:2106.05066

Journal ref: EPTCS 337, 2021, pp. 39-54

Automating Induction by Reflection

Authors: Johannes Schoisswohl, Laura Kovacs

Abstract: 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 th… ▽ More 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. This paper is an extended version of the LFMTP 21 submission with the same title. △ Less

Submitted 9 June, 2021; originally announced June 2021.

Comments: LFMTP

Summing Up Smart Transitions

Authors: Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv

Abstract: Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer… ▽ More Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances. Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length. In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts. △ Less

Submitted 17 May, 2021; originally announced May 2021.

Comments: This submission is an extended version of the CAV 2021 paper "Summing Up Smart Transitions", by N. Elad, S. Rain, N. Immerman, L. Kovács and M. Sagiv

ACM Class: F.3.1; F.4.1

MORA -- Automatic Generation of Moment-Based Invariants

Authors: Ezio Bartocci, Laura Kovacs, Miroslav Stankovic

Abstract: We introduce MORA, an automated tool for generating invariants of probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, MORA computes invariant properties over higher-order moments of loop variables, express… ▽ More We introduce MORA, an automated tool for generating invariants of probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, MORA computes invariant properties over higher-order moments of loop variables, expressing, for example, statistical properties, such as expected values and variances, over the value distribution of loop variables. △ Less

Submitted 5 March, 2021; originally announced March 2021.

Formalizing Graph Trail Properties in Isabelle/HOL

Authors: Laura Kovacs, Hanna Lachnitt, Stefan Szeider

Abstract: We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing g… ▽ More We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one. This preprint has been accepted for publication at CICM 2020. △ Less

Submitted 5 March, 2021; originally announced March 2021.

Algebra-based Synthesis of Loops and their Invariants (Invited Paper)

Authors: Andreas Humenberger, Laura Kovacs

Abstract: Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a… ▽ More Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations. This is a preprint that was invited for publication at VMCAI 2021. △ Less

Submitted 5 March, 2021; originally announced March 2021.

Automated Termination Analysis of Polynomial Probabilistic Programs

Authors: Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács

Abstract: The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination… ▽ More The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions - including the constraints on supermartingales - of a proof rule. Our software tool Amber can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools. △ Less

Submitted 28 January, 2021; v1 submitted 7 October, 2020; originally announced October 2020.

Trace Logic for Inductive Loop Reasoning

Authors: Pamina Georgiou, Bernhard Gleiss, Laura Kovács

Abstract: We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturin… ▽ More We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturing inductive loop invariants. Our work is implemented in the RAPID framework, by extending and integrating superposition-based first-order reasoning within RAPID. We successfully used RAPID to prove correctness of many programs whose functional behavior are best summarized in the first-order theories of linear integer arithmetic, arrays and inductive data types. △ Less

Submitted 6 August, 2020; v1 submitted 4 August, 2020; originally announced August 2020.

Comments: Related Version: A compact, peer-reviewed version of this paper will be available in the conference proceedings of Formal Methods of Computer-Aided Design (FMCAD) 2020

Analysis of Bayesian Networks via Prob-Solvable Loops

Authors: Ezio Bartocci, Laura Kovács, Miroslav Stankovič

Abstract: Prob-solvable loops are probabilistic programs with polynomial assignments over random variables and parametrised distributions, for which the full automation of moment-based invariant generation is decidable. In this paper we extend Prob-solvable loops with new features essential for encoding Bayesian networks (BNs). We show that various BNs, such as discrete, Gaussian, conditional linear Gaussia… ▽ More Prob-solvable loops are probabilistic programs with polynomial assignments over random variables and parametrised distributions, for which the full automation of moment-based invariant generation is decidable. In this paper we extend Prob-solvable loops with new features essential for encoding Bayesian networks (BNs). We show that various BNs, such as discrete, Gaussian, conditional linear Gaussian and dynamic BNs, can be naturally encoded as Prob-solvable loops. Thanks to these encodings, we can 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. △ Less

Submitted 26 July, 2020; v1 submitted 18 July, 2020; originally announced July 2020.

Algebra-based Loop Synthesis

Authors: Andreas Humenberger, Laura Kovács

Abstract: We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurrence equations with constant coefficients. 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… ▽ More We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurrence equations with constant coefficients. 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 program verification, as well as generating number sequences from algebraic relations. We implemented our work in the Absynth tool and report on our initial experiments with loop synthesis. △ Less

Submitted 28 April, 2020; v1 submitted 24 April, 2020; originally announced April 2020.

Subsumption Demodulation in First-Order Theorem Proving

Authors: Bernhard Gleiss, Laura Kovacs, Jakob Rath

Abstract: Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus. We implem… ▽ More Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus. We implemented subsumption demodulation in the theorem prover Vampire, by extending Vampire with a new clause index and adapting its multi-literal matching component. Our experiments, using the TPTP and SMT-LIB repositories, show that subsumption demodulation in Vampire can solve many new problems that could so far not be solved by state-of-the-art reasoners. △ Less

Submitted 28 January, 2020; originally announced January 2020.

Interactive Visualization of Saturation Attempts in Vampire

Authors: Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz

Abstract: Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or mod… ▽ More Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or models. Such an analysis is challenging due to the large number of logical formulas generated during proof/model search. In this paper we focus on saturation-based first-order theorem proving and introduce the SATVIS tool for interactively visualizing saturation-based proof attempts in first-order theorem proving. We build SATVIS on top of the world-leading theorem prover VAMPIRE, by interactively visualizing the saturation attempts of VAMPIRE in SATVIS. Our work combines the automatic layout and visualization of the derivation graph induced by the saturation attempt with interactive transformations and search functionality. As a result, we are able to analyze and debug (failed) proof attempts of VAMPIRE. Thanks to its interactive visualisation, we believe SATVIS helps both experts and non-experts in theorem proving to understand first-order proofs and analyze/refine failing proof attempts of first-order provers. △ Less

Submitted 13 January, 2020; originally announced January 2020.

Journal ref: Ahrendt W., Tapia Tarifa S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science, vol 11918. Springer, Cham

On the notion of number in humans and machines

Authors: Norbert Bátfai, Dávid Papp, Gergő Bogacsovics, Máté Szabó, Viktor Szilárd Simkó, Márió Bersenszki, Gergely Szabó, Lajos Kovács, Ferencz Kovács, Erik Szilveszter Varga

Abstract: In this paper, we performed two types of software experiments to study the numerosity classification (subitizing) in humans and machines. Experiments focus on a particular kind of task is referred to as Semantic MNIST or simply SMNIST where the numerosity of objects placed in an image must be determined. The experiments called SMNIST for Humans are intended to measure the capacity of the Object Fi… ▽ More In this paper, we performed two types of software experiments to study the numerosity classification (subitizing) in humans and machines. Experiments focus on a particular kind of task is referred to as Semantic MNIST or simply SMNIST where the numerosity of objects placed in an image must be determined. The experiments called SMNIST for Humans are intended to measure the capacity of the Object File System in humans. In this type of experiment the measurement result is in well agreement with the value known from the cognitive psychology literature. The experiments called SMNIST for Machines serve similar purposes but they investigate existing, well known (but originally developed for other purpose) and under development deep learning computer programs. These measurement results can be interpreted similar to the results from SMNIST for Humans. The main thesis of this paper can be formulated as follows: in machines the image classification artificial neural networks can learn to distinguish numerosities with better accuracy when these numerosities are smaller than the capacity of OFS in humans. Finally, we outline a conceptual framework to investigate the notion of number in humans and machines. △ Less

Submitted 27 June, 2019; originally announced June 2019.

Verifying Relational Properties using Trace Logic

Authors: Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei

Abstract: We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive inst… ▽ More We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive instance of first-order predicate logic. Trace logic draws its expressiveness from its syntax, which allows expressing properties over computation traces. Its axiomatization supports fine-grained reasoning about intermediate steps in program execution, notably loop iterations. We present an algorithm to encode the semantics of programs as well as their relational properties in trace logic, and then show how first-order theorem proving can be used to reason about the resulting trace logic formulas. Our work is implemented in the tool Rapid and evaluated with examples coming from the security field. △ Less

Submitted 12 August, 2019; v1 submitted 24 June, 2019; originally announced June 2019.

Lonely Points in Simplices

Authors: Maximilian Jaroschek, Manuel Kauers, Laura Kovacs

Abstract: Given a lattice L in Z^m and a subset A of R^m, we say that a point in A is lonely if it is not equivalent modulo L to another point of A. We are interested in identifying lonely points for specific choices of L when A is a dilated standard simplex, and in conditions on L which ensure that the number of lonely points is unbounded as the simplex dilation goes to infinity. Given a lattice L in Z^m and a subset A of R^m, we say that a point in A is lonely if it is not equivalent modulo L to another point of A. We are interested in identifying lonely points for specific choices of L when A is a dilated standard simplex, and in conditions on L which ensure that the number of lonely points is unbounded as the simplex dilation goes to infinity. △ Less

Submitted 21 May, 2019; originally announced May 2019.

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

Authors: Ezio Bartocci, Laura Kovács, Miroslav Stankovič

Abstract: One of the main challenges in the analysis of probabilistic programs is to compute invariant properties that summarise loop behaviours. Automation of invariant generation is still at its infancy and most of the times targets only expected values of the program variables, which is insufficient to recover the full probabilistic program behaviour. We present a method to automatically generate moment-… ▽ More One of the main challenges in the analysis of probabilistic programs is to compute invariant properties that summarise loop behaviours. Automation of invariant generation is still at its infancy and most of the times targets only expected values of the program variables, which is insufficient to recover the full probabilistic program behaviour. We present a method to automatically generate moment-based invariants of a subclass of probabilistic programs, called Prob-Solvable loops, with polynomial assignments over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values or variances, of program variables. We successfully evaluated our work on several examples where full automation for computing higher-order moments and invariants over program variables was not yet possible. △ Less

Submitted 29 May, 2019; v1 submitted 7 May, 2019; originally announced May 2019.

Defining rough sets using tolerances compatible with an equivalence

Authors: Jouni Järvinen, László Kovács, Sándor Radeleczki

Abstract: We consider tolerances $T$ compatible with an equivalence $E$ on $U$, meaning that the relational product $E \circ T$ is included in $T$. We present the essential properties of $E$-compatible tolerances and study rough approximations defined by such $E$ and $T$. We consider rough set pairs $(X_E,X^T)$, where the lower approximation $X_E$ is defined as is customary in rough set theory, but $X^T$ al… ▽ More We consider tolerances $T$ compatible with an equivalence $E$ on $U$, meaning that the relational product $E \circ T$ is included in $T$. We present the essential properties of $E$-compatible tolerances and study rough approximations defined by such $E$ and $T$. We consider rough set pairs $(X_E,X^T)$, where the lower approximation $X_E$ is defined as is customary in rough set theory, but $X^T$ allows more elements to be possibly in $X$ than $X^E$. Motivating examples of $E$-compatible tolerances are given, and the essential lattice-theoretical properties of the ordered set of rough sets $\{ (X_E,X^T) \mid X \subseteq U\}$ are established. △ Less

Submitted 14 May, 2019; v1 submitted 21 November, 2018; originally announced November 2018.

Comments: In press, accepted manuscript

MSC Class: 03E20 (Primary) 68T37; 06B23 (Secondary)

Journal ref: Information Sciences 496 (2019) 264-283

Aligator.jl - A Julia Package for Loop Invariant Generation

Authors: Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

Abstract: We describe the Aligator.jl software package for automatically generating all polynomial invariants of the rich class of extended P-solvable loops with nested conditionals. Aligator.jl is written in the programming language Julia and is open-source. Aligator.jl transforms program loops into a system of algebraic recurrences and implements techniques from symbolic computation to solve recurrences,… ▽ More We describe the Aligator.jl software package for automatically generating all polynomial invariants of the rich class of extended P-solvable loops with nested conditionals. Aligator.jl is written in the programming language Julia and is open-source. Aligator.jl transforms program loops into a system of algebraic recurrences and implements techniques from symbolic computation to solve recurrences, derive closed form solutions of loop variables and infer the ideal of polynomial invariants by variable elimination based on Gröbner basis computation. △ Less

Submitted 16 August, 2018; originally announced August 2018.

Invariant Generation for Multi-Path Loops with Polynomial Assignments

Authors: Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

Abstract: Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are p… ▽ More Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are polynomial expressions over program variables. We call this class of loops extended P-solvable and introduce an algorithm for generating all polynomial invariants of such loops. By an iterative procedure employing Gröbner basis computation, our approach computes the polynomial ideal of the polynomial invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given extended P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of inner loops. In particular, for a loop with m program variables and r conditional branches we prove an upper bound of m*r iterations. We implemented our approach in the Aligator software package. Furthermore, we evaluated it on 18 programs with polynomial arithmetic and compared it to existing methods in invariant generation. The results show the efficiency of our approach. △ Less

Submitted 11 January, 2018; originally announced January 2018.

A Supervisory Control Algorithm Based on Property-Directed Reachability

Authors: Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson

Abstract: We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also simi… ▽ More We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for computer science has developed techniques and tools. In this paper, we attempt to marry the two by adapting PDR to the problem of controller synthesis. The resulting algorithm takes as input a transition system with forbidden states and uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution to the greater effort of formal supervisory controller synthesis and verification. △ Less

Submitted 17 November, 2017; originally announced November 2017.

Comments: 16 pages; presented at Haifa Verification Conference 2017, the final publication is available at Springer via https://doi.org/10.1007/978-3-319-70389-3_8

MSC Class: 68-02

Journal ref: Strichman O., Tzoref-Brill R. (eds) Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science, vol 10629. Springer, Cham

Splitting Proofs for Interpolation

Authors: Bernhard Gleiss, Laura Kovacs, Martin Suda

Abstract: We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the com- mon signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the re… ▽ More We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the com- mon signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the refuta- tion into two parts. We use this new insight to develop an algorithm for extracting interpolants which are linear in the size of the input refutation and can be further optimized using metrics such as number of non-logical symbols or quantifiers. We implemented the new algorithm in first-order theorem prover VAMPIRE and evaluated it on a large number of examples coming from the first-order proving community. Our experiments give practical evidence that our work improves the state-of-the-art in first-order interpolation. △ Less

Submitted 7 November, 2017; originally announced November 2017.

Comments: 26th Conference on Automated Deduction, 2017

Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

Authors: Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

Abstract: Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursion. For such programs one needs additional information, for example in the form of loop invariants, expressing properties to hold at intermediate program points. In this paper we study program loops with non-trivial arith… ▽ More Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursion. For such programs one needs additional information, for example in the form of loop invariants, expressing properties to hold at intermediate program points. In this paper we study program loops with non-trivial arithmetic, implementing addition and multiplication among numeric program variables. We present a new approach for automatically generating all polynomial invariants of a class of such programs. Our approach turns programs into linear ordinary recurrence equations and computes closed form solutions of these equations. These closed forms express the most precise inductive property, and hence invariant. We apply Gröbner basis computation to obtain a basis of the polynomial invariant ideal, yielding thus a finite representation of all polynomial invariants. Our work significantly extends the class of so-called P-solvable loops by handling multiplication with the loop counter variable. We implemented our method in the Mathematica package Aligator and showcase the practical use of our approach. △ Less

Submitted 11 May, 2017; v1 submitted 8 May, 2017; originally announced May 2017.

Comments: A revised version of this paper is published in the proceedings of ISSAC 2017

Symbolic Computation and Automated Reasoning for Program Analysis

Authors: Laura Kovacs

Abstract: This talk describes 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. The talk will first present how computer algebra methods, such as Groebner basis computation, quantifier elimination and al… ▽ More This talk describes 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. The talk will first present how computer algebra methods, such as Groebner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops with non-trivial arithmetic. Typical properties inferred by our work are loop invariants and expressions bounding the number of loop iterations. The talk will then describe our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, we use saturation-based first-order theorem proving and extend first-order provers with support for program analysis. Since program analysis requires reasoning in the combination of first-order theories of data structures, the talk also discusses new features in firstorder theorem proving, such as inductive reasoning and built-in boolean sort. These extensions allow us to express program properties directly in first-order logic and hence use further first-order theorem provers to reason about program properties. △ Less

Submitted 11 April, 2017; originally announced April 2017.

Comments: Paper published at iFM 2016

Coming to Terms with Quantified Reasoning

Authors: Laura Kovacs, Simon Robillard, Andrei Voronkov

Abstract: The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over algebraic data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reaso… ▽ More The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over algebraic data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reasoning about quantified properties over term algebras is challenging. In this paper we address full first-order reasoning about properties of programs manipulating term algebras, and describe two approaches for doing so by using first-order theorem proving. Our first method is a conservative extension of the theory of term algebras using a finite number of statements, while our second method relies on extending the superposition calculus of first-order theorem provers with additional inference rules. We implemented our work in the first-order theorem prover Vampire and evaluated it on a large number of algebraic data type benchmarks, as well as game theory constraints. Our experimental results show that our methods are able to find proofs for many hard problems previously unsolved by state-of-the-art methods. We also show that Vampire implementing our methods outperforms existing SMT solvers able to deal with algebraic data types. △ Less

Submitted 9 November, 2016; originally announced November 2016.

ACM Class: D.2.4; F.3.1; F.3.2; F.4.1; I.2.3; I.2.4

The Vampire and the FOOL

Authors: Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov

Abstract: This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expres… ▽ More This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency. △ Less

Submitted 5 December, 2015; v1 submitted 16 October, 2015; originally announced October 2015.

ACM Class: D.2.4; F.3.1; F.4.1; I.2.3; I.2.5

A First Class Boolean Sort in First-Order Theorem Proving and TPTP

Authors: Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov

Abstract: To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program properties can be translated to first-order logic and theorem provers can be used to prove program properties efficiently. However, in the TPTP language, the input language of automated first-order theorem provers, the use of… ▽ More To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program properties can be translated to first-order logic and theorem provers can be used to prove program properties efficiently. However, in the TPTP language, the input language of automated first-order theorem provers, the use of the boolean sort is limited compared to other sorts, thus hindering the use of first-order theorem provers in program analysis and verification. In this paper, we present an extension FOOL of many-sorted first-order logic, in which the boolean sort is treated as a first-class sort. Boolean terms are indistinguishable from formulas and can appear as arguments to functions. In addition, FOOL contains if-then-else and let-in constructs. We define the syntax and semantics of FOOL and its model-preserving translation to first-order logic. We also introduce a new technique of dealing with boolean sorts in superposition-based theorem provers. Finally, we discuss how the TPTP language can be changed to support FOOL. △ Less

Submitted 7 May, 2015; originally announced May 2015.

Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems

Authors: Laura Kovacs, Rosario Pugliese, Francesco Tiezzi

Abstract: This volume contains the final and revised versions of the papers presented at the 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011). The workshop was held in Reykjavik, Iceland, on June 9, 2011, as part of DisCoTec 2011. The aim of the WWV workshop series is to provide an interdisciplinary forum to facilitate the cross-fertilization and the advanceme… ▽ More This volume contains the final and revised versions of the papers presented at the 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011). The workshop was held in Reykjavik, Iceland, on June 9, 2011, as part of DisCoTec 2011. The aim of the WWV workshop series is to provide an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools drawn from Rule-based programming, Software engineering, Formal methods and Web-oriented research. Nowadays, indeed, many companies and institutions have diverted their Web sites into interactive, completely-automated, Web-based applications for, e.g., e-business, e-learning, e-government, and e-health. The increased complexity and the explosive growth of Web systems have made their design and implementation a challenging task. Systematic, formal approaches to their specification and verification can permit to address the problems of this specific domain by means of automated and effective techniques and tools. In response to this year's call for papers, we received 9 paper submissions. The Program Committee of WWV 2011 collected three reviews for each paper and held an electronic discussion leading to the selection of 7 papers for presentation at the workshop. In addition to the selected papers, the scientific programme included an invited lecture by Elie Najm. △ Less

Submitted 9 August, 2011; originally announced August 2011.

Comments: EPTCS 61, 2011

Descriptive-complexity based distance for fuzzy sets

Authors: Laszlo Kovacs, Joel Ratsaby

Abstract: A new distance function dist(A,B) for fuzzy sets A and B is introduced. It is based on the descriptive complexity, i.e., the number of bits (on average) that are needed to describe an element in the symmetric difference of the two sets. The distance gives the amount of additional information needed to describe any one of the two sets given the other. We prove its mathematical properties and perfor… ▽ More A new distance function dist(A,B) for fuzzy sets A and B is introduced. It is based on the descriptive complexity, i.e., the number of bits (on average) that are needed to describe an element in the symmetric difference of the two sets. The distance gives the amount of additional information needed to describe any one of the two sets given the other. We prove its mathematical properties and perform pattern clustering on data based on this distance. △ Less

Submitted 15 December, 2010; originally announced December 2010.