PV2 Samplegenerates permission pre- and postconditions for Viper programs

Infers permission pre- and postconditions for array programs

Application domain/field

Type of tool

Specification generator/annotation generator

Expected input

Program

Format:

Viper program

Expected output

Program annotated with permission pre- and postconditions

Internals

Sample infers permission pre- and postconditions for Viper programs. The tool first performs a forward numerical analysis to infer over-approximate loop invariants. Then, the tool performs inference and maximum elimination. Finally, it adds the annotations to the input program. Uses APRON for numerical analysis.

Links

Repository: https://github.com/viperproject/sample

Last commit date

5 June 2020

Related papers

https://doi.org/10.1007/978-3-319-96142-2_7 (CAV 2018)

Last publication date

18 July 2018

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.