b'Laura Kov\xc3\xa1cs'

research

∙ 07/20/2023

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

We show that computing the strongest polynomial invariant for single-pat...

0 Julian Müllner, et al. ∙

research

∙ 06/02/2023

(Un)Solvable Loop Analysis

Automatically generating invariants, key to computer-aided analysis of p...

0 Daneshvar Amrollahi, et al. ∙

research

∙ 05/24/2023

Automated Sensitivity Analysis for Probabilistic Loops

We present an exact approach to analyze and quantify the sensitivity of ...

0 Marcel Moosbrugger, et al. ∙

research

∙ 05/20/2023

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Cryptographic protocols are extremely hard to design and prove correct, ...

0 Simon Jeanteur, et al. ∙

research

∙ 04/24/2023

SMT Solving over Finite Field Arithmetic

Non-linear polynomial systems over finite fields are used to model funct...

0 Thomas Hader, et al. ∙

research

∙ 02/13/2023

From Polynomial Invariants to Linear Loops

Loop invariants are software properties that hold before and after every...

0 George Kenison, et al. ∙

research

∙ 06/23/2022

Algebra-Based Reasoning for Loop Synthesis

Provably correct software is one of the key challenges of our software-d...

0 Andreas Humenberger, et al. ∙

research

∙ 06/14/2022

Solving Invariant Generation for Unsolvable Loops

Automatically generating invariants, key to computer-aided analysis of p...

0 Daneshvar Amrollahi, et al. ∙

research

∙ 05/13/2022

Distribution Estimation for Probabilistic Loops

We present an algorithmic approach to estimate the value distributions o...

0 Ahmad Karimi, et al. ∙

research

∙ 04/14/2022

This is the Moment for Probabilistic Loops

We present a novel static analysis technique to derive higher moments fo...

0 Marcel Moosbrugger, et al. ∙

research

∙ 09/15/2021

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

Off-chain protocols constitute one of the most promising approaches to s...

0 Sophie Rain, et al. ∙

research

∙ 07/27/2021

The Probabilistic Termination Tool Amber

We describe the Amber tool for proving and refuting the termination of a...

0 Marcel Moosbrugger, et al. ∙

research

∙ 06/09/2021

Automating Induction by Reflection

Despite recent advances in automating theorem proving in full first-orde...

0 Johannes Schoisswohl, et al. ∙

research

∙ 05/17/2021

Summing Up Smart Transitions

Some of the most significant high-level properties of currencies are the...

0 Neta Elad, et al. ∙

research

∙ 03/05/2021

MORA – Automatic Generation of Moment-Based Invariants

We introduce MORA, an automated tool for generating invariants of probab...

0 Ezio Bartocci, et al. ∙

research

∙ 03/05/2021

Formalizing Graph Trail Properties in Isabelle/HOL

We describe a dataset expressing and proving properties of graph trails,...

0 Laura Kovács, et al. ∙

research

∙ 03/05/2021

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

Provably correct software is one of the key challenges in our softwaredr...

0 Andreas Humenberger, et al. ∙

research

∙ 10/07/2020

Automated Termination Analysis of Polynomial Probabilistic Programs

The termination behavior of probabilistic programs depends on the outcom...

0 Marcel Moosbrugger, et al. ∙

research

∙ 08/04/2020

Trace Logic for Inductive Loop Reasoning

We propose trace logic, an instance of many-sorted first-order logic, to...

0 Pamina Georgiou, et al. ∙

research

∙ 07/18/2020

Analysis of Bayesian Networks via Prob-Solvable Loops

Prob-solvable loops are probabilistic programs with polynomial assignmen...

0 Ezio Bartocci, et al. ∙

research

∙ 04/24/2020

Algebra-based Loop Synthesis

We present an algorithm for synthesizing program loops satisfying a give...

0 Andreas Humenberger, et al. ∙

research

∙ 01/28/2020

Subsumption Demodulation in First-Order Theorem Proving

Motivated by applications of first-order theorem proving to software ana...

0 Bernhard Gleiss, et al. ∙

research

∙ 01/13/2020

Interactive Visualization of Saturation Attempts in Vampire

Many applications of formal methods require automated reasoning about sy...

0 Bernhard Gleiss, et al. ∙

research

∙ 06/24/2019

Verifying Relational Properties using Trace Logic

We present a logical framework for the verification of relational proper...

0 Gilles Barthe, et al. ∙

research

∙ 05/21/2019

Lonely Points in Simplices

Given a lattice L in Z^m and a subset A of R^m, we say that a point in A...

0 Maximilian Jaroschek, et al. ∙

research

∙ 05/07/2019

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

One of the main challenges in the analysis of probabilistic programs is ...

0 Ezio Bartocci, et al. ∙

research

∙ 08/16/2018

Aligator.jl - A Julia Package for Loop Invariant Generation

We describe the Aligator.jl software package for automatically generatin...

0 Andreas Humenberger, et al. ∙

research

∙ 01/11/2018

Invariant Generation for Multi-Path Loops with Polynomial Assignments

Program analysis requires the generation of program properties expressin...

0 Andreas Humenberger, et al. ∙

research

∙ 11/17/2017

A Supervisory Control Algorithm Based on Property-Directed Reachability

We present an algorithm for synthesising a controller (supervisor) for a...

0 Koen Claessen, et al. ∙

research

∙ 11/07/2017

Splitting Proofs for Interpolation

We study interpolant extraction from local first-order refutations. We p...

0 Bernhard Gleiss, et al. ∙

research

∙ 05/08/2017

Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

Analyzing and reasoning about safety properties of software systems beco...

0 Andreas Humenberger, et al. ∙

Laura Kovács

Featured Co-authors