Viper verifier

Viper verifier
[Google Scholar] [Website]

Notes: intermediate verification language, Rust language, permission logic, Prusti verifier, verification condition generator

Viper is an intermediate verification language based on permission logic developed at ETH Zürich.

Frontends include Prusti verifier for the Rust language.

Intermediate verification language, Ownership types, Permission logic, Prusti verifier