PV2 ⊧ Samplegenerates permission pre- and postconditions for Viper programs

Infers permission pre- and postconditions for array programs

Application domain/field

• Separation logic
• Program verification
• Array programs
• Permissions
• Pre- and postconditions

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.