Pinned Repositories
2vyper
A static verifer for Ethereum Smart Contracts written in Vyper
axiom-profiler
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
bitbucket-issue-migration
Scripts for the migration from Bitbucket to GitHub.
carbon
Verification-condition-generation-based verifier for the Viper intermediate verification language.
gobra
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
prusti-assistant
VS Code extension to verify Rust programs with the Prusti verifier.
prusti-dev
A static verifier for Rust, based on the Viper verification infrastructure.
silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.
silver
Definition of the Viper intermediate verification language.
viperserver
HTTP server that manages verification requests to different tools from the Viper tool stack.
Viper Project's Repositories
viperproject/2vyper
A static verifer for Ethereum Smart Contracts written in Vyper
viperproject/bitbucket-issue-migration
Scripts for the migration from Bitbucket to GitHub.
viperproject/rust-contracts
viperproject/rust-life
Simple explanations for some complex Rust lifetime errors.
viperproject/check-license-header
GitHub action to check whether all files have a specified copyright license header
viperproject/prusti-action
GitHub Action to verify Rust code using the Prusti verifier.
viperproject/lizard
Lizard is the visual verification debugger for Viper IDE
viperproject/ouroboros
viperproject/reachability-verification
Heap reachability verification benchmarks (manually encoded in Viper) used in Modular Verification of Heap Reachability Properties in Separation Logic
viperproject/code-server-hub
Multi-user server for Code-Server
viperproject/dockerspawner
Spawns Code-Server single user servers in Docker containers
viperproject/gorac
viperproject/silver-multisets
An alternative encoding of multisets based on Dafny's encoding in Boogie.
viperproject/voila
Voila is proof outline checker for fine-grained concurrency verification
viperproject/sample
viperproject/.github
viperproject/arp-plugin
Plugin for Silver implementing Abstract Read Permissions.
viperproject/arp-plugin-test
viperproject/boogie-builder
A GitHub action that builds Boogie.
viperproject/chalice2silver
viperproject/commutativity-plugin-test
viperproject/documentation
viperproject/examples-verification
This repository contains the structure required for the Jenkins jobs "Examples Verification" to work.
viperproject/hyperviper
viperproject/prusti-perf
Website for graphing performance of rustc
viperproject/rust-pcs
viperproject/rustc-plugin
A framework for writing plugins that integrate with the Rust compiler
viperproject/silicon-sif-extension
Extension of Silicon for product programs, in particular product program counterexample transformation
viperproject/viper-ide-deps
This is the template repository for binary dependencies for Viper IDE. Created for automating the ViperTools package creation via Jenkins. Related: https://github.com/viperproject/viper-ide
viperproject/vs-verification-toolbox-release-testing
Repository with some releases to test vs-verification-toolbox