• Stars
    star
    34
  • Rank 743,971 (Top 16 %)
  • Language
    Scala
  • License
    Other
  • Updated about 2 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

More Repositories

1

prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
Rust
1,478
star
2

silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.
Scala
74
star
3

silver

Definition of the Viper intermediate verification language.
Scala
74
star
4

2vyper

A static verifer for Ethereum Smart Contracts written in Vyper
Python
50
star
5

carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Scala
29
star
6

axiom-profiler

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
C#
27
star
7

prusti-assistant

VS Code extension to verify Rust programs with the Prusti verifier.
TypeScript
22
star
8

bitbucket-issue-migration

Scripts for the migration from Bitbucket to GitHub.
Python
21
star
9

viperserver

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

create-nightly-release

GitHub action to create a new pre-release and delete old pre-releases created by this action
TypeScript
10
star
11

viper-ide

This is the main repository for the Viper IDE extension for VS Code.
TypeScript
9
star
12

gobra-ide

VSCode Plugin for Gobra
TypeScript
8
star
13

rust-contracts

Rust
7
star
14

rust-life

Simple explanations for some complex Rust lifetime errors.
Rust
7
star
15

VerifiedSCION

Verifying the SCION architecture using Gobra
Go
6
star
16

check-license-header

GitHub action to check whether all files have a specified copyright license header
TypeScript
6
star
17

vs-verification-toolbox

Useful component to build VS Code extensions for verifiers.
TypeScript
5
star
18

jni-gen

Generate Rust wrappers for Java/Scala
Rust
4
star
19

program-proofs-gobra

Examples and exercises from the book Program Proofs translated to Gobra
4
star
20

viper_client

Python
3
star
21

prusti-action

GitHub Action to verify Rust code using the Prusti verifier.
JavaScript
3
star
22

mendel-verifier

Capability-based verifier for safe Rust clients of interior mutability
Rust
3
star
23

termination-plugin

A Viper plugin for proving termination.
Scala
2
star
24

gobra-libs

Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.
Python
2
star
25

gobra-action

Github Action to verify Go code with Gobra directly in a CI workflow
Shell
2
star
26

ouroboros

Scala
2
star
27

lizard

Lizard is the visual verification debugger for Viper IDE
TypeScript
2
star
28

reachability-verification

Heap reachability verification benchmarks (manually encoded in Viper) used in Modular Verification of Heap Reachability Properties in Separation Logic
2
star
29

axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
Rust
2
star
30

viper-runner

Python
1
star
31

silver-multisets

An alternative encoding of multisets based on Dafny's encoding in Boogie.
1
star
32

voila

Voila is proof outline checker for fine-grained concurrency verification
Scala
1
star
33

viper-linux-dev-docker

Docker image for developing Viper https://github.com/viperproject/ See also https://github.com/viperproject/viper-linux-dev
Dockerfile
1
star
34

viper-linux-dev

Environment for developing Viper under Linux.
Python
1
star
35

gobra-mode

Support for Gobra in emacs
Emacs Lisp
1
star
36

gorac

Go
1
star
37

vpr-mode

Viper mode for emacs
Emacs Lisp
1
star