A polytime complexity analyser for Probabilistic Polynomial Time over imperative stack programs

TL;DR

This paper introduces iSAPP, a static analysis tool that verifies whether imperative stack programs run within the Probabilistic Polynomial Time complexity class, providing a sound and complete method for complexity analysis.

Contribution

The paper presents iSAPP, a novel static analyser for imperative stack programs that is sound and extensionally complete for PP, with polynomial-time certificate generation.

Findings

iSAPP can verify PP complexity for stack programs.

Certificate of polynomiality can be generated in polynomial time.

The tool is sound and extensionally complete for PP.

Abstract

We present iSAPP (Imperative Static Analyser for Probabilistic Polynomial Time), a complexity verifier tool that is sound and extensionally complete for the Probabilistic Polynomial Time (PP) complexity class. iSAPP works on an imperative programming language for stack machines. The certificate of polynomiality can be built in polytime, with respect to the number of stacks used.