PV3 ⊧ Viperdetects inconsistencies between the code and spec with symbolic executionVerification infrastructure for permission-based reasoning
- Verification architecture
- Symbolic execution
- Separation logic
- Verification condition generation
- Deductive verification
Type of toolDeductive verifier/verification architecture
InternalsGiven 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.
- If it would only generate verification conditions for Boogie, it would have ended up on PV2.
- There is a VS Code extension for Viper.