137 citations · 525 across the 67 of their papers we have counts for
7 papers · 1 filter
Polar: An Algebraic Analyzer for (Probabilistic) Loops
Marcel Moosbrugger, Julian Müllner, Ezio Bartocci +1
We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling alge…
(Un)Solvable Loop Analysis
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…
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…
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…
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…
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…