Viper Project

Verification Infrastructure for Permission-based Reasoning

README.md

Viper (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly.

Official project webpage: viper.ethz.ch

Pinned Loading

silver silver Public

Definition of the Viper intermediate verification language.

Scala 76 39
silicon silicon Public

Symbolic-execution-based verifier for the Viper intermediate verification language.

Scala 78 31
carbon carbon Public

Verification-condition-generation-based verifier for the Viper intermediate verification language.

Scala 29 19
viperserver viperserver Public

HTTP server that manages verification requests to different tools from the Viper tool stack.

Scala 10 15
prusti-dev prusti-dev Public

A static verifier for Rust, based on the Viper verification infrastructure.

Rust 1.5k 104
gobra gobra Public

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

Scala 102 26

Repositories

VerifiedSCION Public
Verifying the SCION architecture using Gobra

viperproject/VerifiedSCION’s past year of commit activity

Go 7 Apache-2.0 2 12 6 Updated Jul 19, 2024
axiom-profiler-2 Public
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).

viperproject/axiom-profiler-2’s past year of commit activity

Rust 8 3 4 5 Updated Jul 19, 2024
silver-oxide Public
A Rust parser for Viper

viperproject/silver-oxide’s past year of commit activity

Rust 0 MPL-2.0 0 0 0 Updated Jul 19, 2024
gobra-ide Public
VSCode Plugin for Gobra

viperproject/gobra-ide’s past year of commit activity

TypeScript 8 1 2 1 Updated Jul 19, 2024
mendel-verifier Public
Capability-based verifier for safe Rust clients of interior mutability

viperproject/mendel-verifier’s past year of commit activity

Rust 6 1 0 0 Updated Jul 18, 2024
gobra Public
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

viperproject/gobra’s past year of commit activity

Scala 102 26 79 10 Updated Jul 17, 2024
vs-verification-toolbox Public
Useful component to build VS Code extensions for verifiers.

viperproject/vs-verification-toolbox’s past year of commit activity

TypeScript 5 MPL-2.0 2 0 1 Updated Jul 15, 2024
silver Public
Definition of the Viper intermediate verification language.

viperproject/silver’s past year of commit activity

Scala 76 MPL-2.0 39 99 11 Updated Jul 15, 2024
viper-ide Public
This is the main repository for the Viper IDE extension for VS Code.

viperproject/viper-ide’s past year of commit activity

TypeScript 10 MPL-2.0 8 14 7 Updated Jul 15, 2024
silicon Public
Symbolic-execution-based verifier for the Viper intermediate verification language.

viperproject/silicon’s past year of commit activity

Scala 78 MPL-2.0 31 113 9 Updated Jul 12, 2024