PV1 Pastiscan compute and produce proofs for resource bounds of imperative programs

Tool that computes polynomial resource bounds for imperative integer programs.

Application domain/field

Type of tool

Resource bound analyzer

Expected input

Imperative integer program


Either written in a minimal (own) imperative language, or LLVM bitcode


AARA-based tool for generating polynomial bounds on low-level integer programs with recursive procedures AARA: automatic amortized resource analysis. A technique that statically derives concrete (non-asymptotic) resource bounds. The tool accepts a minimal imperative language and LLVM bitcode as input. It supports expressions that are additions, subtractions, and multiplications of constants and program variables. It uses a special random expression for all other operations (such as divisions). Pastis also automatically generates proof certificates of the validity of its bounds.


Repository: https://github.com/academic-archive/cav17-pastis

Related papers

Automated Resource Analysis with Coq Proof Objects (CAV '17)

Last publication date

13 July 2017

Related tools

Resource-bound analyses for integer programs: CAMPY, KoAT, Rank, CoFloCo, COSTA, Loopus

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.