Integrating KoAT’s push-button probabilistic cost analysis into Caesar

RWTH Publications (RWTH Aachen)

Abstract

Probabilistic programs model randomized algorithms and stochastic processes, but verifying their correctness and runtime behavior remains challenging. Caesar is a deductive verification infrastructure for probabilistic programs that requires users to provide pre-expectations as annotations. Finding these manually can be complex and error-prone. KoAT is a tool for automated cost complexity analysis of probabilistic integer programs that can automatically infer upper bounds on expected runtimes. In this thesis, we develop and implement a fully automatic translation from Caesar’s input language HeyVL into KoAT’s input format, enabling users to invoke KoAT at the push of a button to obtain runtime bounds. We formally prove the correctness of our translation, showing that KoAT’s result constitutes a valid upper bound on the original program’s expected runtime. We empirically evaluated our implementation and showed that our translation produces consistent results compared to KoAT’s native analysis.

Authors 1

1. Mats Eblenkamp corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen