29 citations · 37 across the 8 of their papers we have counts for
9 papers
Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Anne Schreuder, Lorenz Winkler, Laura Kovács +1
We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials…
From Polynomial Invariants to Linear Loops
George Kenison, Laura Kovács, Anton Varonka
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 verific…
Solving Invariant Generation for Unsolvable Loops
Daneshvar Amrollahi, Ezio Bartocci, George Kenison +3
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the…
Distribution Estimation for Probabilistic Loops
Ahmad Karimi, Marcel Moosbrugger, Miroslav Stankovič +3
We present an algorithmic approach to estimate the value distributions of random variables of probabilistic loops whose statistical moments are (partially) known. Based on these mo…
This Is the Moment for Probabilistic Loops
Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci +1
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…
Towards a Game-Theoretic Security Analysis of Off-Chain Protocols
Sophie Rain, Georgia Avarikioti, Laura Kovács +1
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-…
The Probabilistic Termination Tool Amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen +1
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 combin…
Trace Logic for Inductive Loop Reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovács
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 semanti…
Algebra-based Loop Synthesis
Andreas Humenberger, Laura Kovács
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 recurren…