43 citations · 170 across the 19 of their papers we have counts for
24 papers
Algebra-Based Reasoning for Loop Synthesis
Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner +1
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 -- i…
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 rea…
Automating Induction by Reflection
Johannes Schoisswohl, Laura Kovacs
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 rea…
Summing Up Smart Transitions
Neta Elad, Sophie Rain, Neil Immerman +2
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 transa…
MORA -- Automatic Generation of Moment-Based Invariants
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic
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 poly…
Formalizing Graph Trail Properties in Isabelle/HOL
Laura Kovacs, Hanna Lachnitt, Stefan Szeider
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 weigh…
Algebra-based Synthesis of Loops and their Invariants (Invited Paper)
Andreas Humenberger, Laura Kovacs
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 progra…
Automated Termination Analysis of Polynomial Probabilistic Programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen +1
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 ter…
Analysis of Bayesian Networks via Prob-Solvable Loops
Ezio Bartocci, Laura Kovács, Miroslav Stankovič
Prob-solvable loops are probabilistic programs with polynomial assignments over random variables and parametrised distributions, for which the full automation of moment-based invar…
Subsumption Demodulation in First-Order Theorem Proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath
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…
Interactive Visualization of Saturation Attempts in Vampire
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz
Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engin…
Verifying Relational Properties using Trace Logic
Gilles Barthe, Renate Eilers, Pamina Georgiou +3
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 applica…
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Ezio Bartocci, Laura Kovács, Miroslav Stankovič
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…
Lonely Points in Simplices
Maximilian Jaroschek, Manuel Kauers, Laura Kovacs
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 p…
Aligator.jl - A Julia Package for Loop Invariant Generation
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
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. Aligato…
Invariant Generation for Multi-Path Loops with Polynomial Assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properti…
A Supervisory Control Algorithm Based on Property-Directed Reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovács +1
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…
Splitting Proofs for Interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda
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 s…
Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
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 recursio…
Symbolic Computation and Automated Reasoning for Program Analysis
Laura Kovacs
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…
Coming to Terms with Quantified Reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov
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 essentia…
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger +1
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 arr…
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
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 prope…
Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems
Laura Kovacs, Rosario Pugliese, Francesco Tiezzi
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).…