PV3 ⊧ Viperdetects inconsistencies between the code and spec with symbolic execution

Verification infrastructure for permission-based reasoning

Application domain/field

• Verification architecture
• Symbolic execution
• Separation logic
• Verification condition generation
• Deductive verification

Type of tool

Deductive verifier/verification architecture

Internals

Given a program and its specification in Viper's intermediate language, it can either generate verification conditions, which are then passed to Boogie, or it can use symbolic execution to try and detect inconsistencies between the code and the specifications. Uses Z3.

Comments

• If it would only generate verification conditions for Boogie, it would have ended up on PV2.
• There is a VS Code extension for Viper.