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

• Resource-bound analysis
• Resource bounds
• Resource consumption
• Automatic amortized resource analysis (AARA)

Type of tool

Resource bound analyzer

Expected input

Imperative integer program

Format:

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

Internals

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.