Propietario

viperproject

13 repositorios indexados · Ver en GitHub

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

Scala · 189 estrellas
silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.

Scala · 145 estrellas
silver
Definition of the Viper intermediate verification language.

Scala · 100 estrellas
carbon
Verification-condition-generation-based verifier for the Viper intermediate verification language.

Scala · 38 estrellas
viperserver
HTTP server that manages verification requests to different tools from the Viper tool stack.

Scala · 16 estrellas
viper-ide
This is the main repository for the Viper IDE extension for VS Code.

TypeScript · 14 estrellas
VerifiedSCION
Verifying the SCION architecture using Gobra

Go · 12 estrellas
gobra-ide
VSCode Plugin for Gobra

TypeScript · 11 estrellas
vs-verification-toolbox
Useful component to build VS Code extensions for verifiers.

TypeScript · 6 estrellas
gobra-book

JavaScript · 4 estrellas
gobra-action
Github Action to verify Go code with Gobra directly in a CI workflow

Shell · 2 estrellas
gobra-libs
Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.

Python · 2 estrellas
tutorial
This repo contains the sources of the official Viper tutorial. Feel free to submit your fixes and additions via pull requests. Please rep...

JavaScript · 0 estrellas

Para principiantes Todo

Abierto Todos

quantifiedExp does not apply its `ignore` parameter, unlike `quantified` Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 68/100

viperproject/silicon#1006 · Abierto el 9/9/2026
Termination measures are not checked for closure spec calls Abierto

soundness termination-checking

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/gobra#1106 · Abierto el 4/9/2026
Termination measures of interface methods are not checked across package boundaries Abierto

soundness termination-checking

Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

viperproject/gobra#1105 · Abierto el 4/9/2026
Recursive function plus quantifier that triggers on the function results in matching loop Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

viperproject/silicon#1004 · Abierto el 25/8/2026
Carbon can prove false Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/carbon#591 · Abierto el 18/8/2026
Type checker crashes on addressing an element of a slice obtained from a map lookup Abierto

Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100

viperproject/gobra#1097 · Abierto el 17/8/2026
Confusing reason/offending position ID with sequencing operation Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silver#928 · Abierto el 15/8/2026
Tutorial.md is severely limited compared to actual *.g4 files Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1093 · Abierto el 15/8/2026
Termination plugin fails with unclear error Abierto

bug termination plugin

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silver#925 · 1 comentario · Abierto el 10/8/2026
Unclear error message when injectivity check fails in a subexpression Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silicon#997 · Abierto el 10/8/2026
Quantified predicate permission over freshly-allocated pointers fails injectivity check, even for provably-fresh allocations Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1060 · Abierto el 31/7/2026
Pure interface method's definitional axiom does not fire through interface dispatch when the method recurses through another interface-typed call Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/gobra#1059 · Abierto el 30/7/2026
Cannot prove non-nil after make Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1052 · 2 comentarios · Abierto el 19/7/2026
It is unnecessarily hard to prove injectivity of slices of struct pointers Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1051 · Abierto el 18/7/2026
Anonymous methods Abierto

enhancement

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

viperproject/silver#922 · Abierto el 13/7/2026
Forward goto after variable declaration causes crash Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/silicon#991 · Abierto el 10/7/2026
Doing bitvector work in cvc5 puts the solver in a broken state Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silicon#990 · Abierto el 10/7/2026
Conjunction of abstract functions is not able to be asserted Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

viperproject/carbon#588 · Abierto el 10/7/2026
Conjunction of abstract functions is not able to be asserted Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/silicon#989 · 1 comentario · Abierto el 10/7/2026
Irreducible CFG error reporting is not useful Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

viperproject/silver#918 · Abierto el 23/6/2026
Proposed annotation: verified — heap-free function postconditions as domain axioms Abierto

encoding enhancement syntax

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

viperproject/gobra#1037 · 9 comentarios · Abierto el 14/6/2026
Inconsistent treatment of recursive function postconditions Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silver#913 · Abierto el 21/5/2026
Invalid Triggers via Subslicing Abierto

bug encoding invalid triggers

Dificultad 4/5 3-5 días Aptitud para principiantes 42/100

viperproject/gobra#1030 · 1 comentario · Abierto el 13/5/2026
Wands are not checked for self-framingness Abierto

magic-wands

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silicon#974 · Abierto el 7/5/2026
Gobra does not immediately realize semantics of copying arrays by assignment Abierto

bug encoding incompleteness

Dificultad 3/5 1-2 días Aptitud para principiantes 48/100

viperproject/gobra#1027 · 6 comentarios · Abierto el 6/5/2026
Can prove nil-ness and non-nilness from struct predicate Abierto

documentation

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1025 · 5 comentarios · Abierto el 4/5/2026
Question on Injectivity Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 52/100

viperproject/gobra-book#50 · Abierto el 30/4/2026
Wildcard permissions don't work inside predicate bodies Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 38/100

viperproject/carbon#584 · Abierto el 23/4/2026
Carbon does not "frame" trigger-matching heap-dependent functions which depend on QPs (without help) Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

viperproject/carbon#583 · 1 comentario · Abierto el 17/4/2026
Diagnostics count on errors is global Abierto

viperproject/viper-ide#566 · 1 reacción · 2 asignados · Abierto el 26/3/2026
Incorrect encoding of relational predicates Abierto

SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

viperproject/silver#907 · 1 comentario · Abierto el 24/3/2026
Clean up createRequire workarounds once VS Code ESM support is fixed Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/vs-verification-toolbox#227 · Abierto el 5/3/2026
Incomplete Slice Allocation Spec Abierto

encoding enhancement

Dificultad 3/5 1-2 días Aptitud para principiantes 52/100

viperproject/gobra#1007 · Abierto el 4/3/2026
Parser Error for Reserved Keywords Abierto

enhancement parsing

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#1005 · Abierto el 2/3/2026
Allow impure assertions for `assert by` Abierto

feature-request

Dificultad 3/5 1-2 días Aptitud para principiantes 38/100

viperproject/gobra#999 · Abierto el 24/2/2026
Invalid SMT Encoding Abierto

bug encoding

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/gobra#997 · Abierto el 20/2/2026
Unintuitive semantics for mixed non-hyper-predicates and hyper-predicates Abierto

documentation SIF

Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

viperproject/gobra#996 · 10 comentarios · Abierto el 17/2/2026
Using `rel(t,0) < rel(t,1)` with implication in SIF mode causes an error. Abierto

SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 32/100

viperproject/gobra#994 · 2 comentarios · Abierto el 11/2/2026
Assert might fail even defined before the `ghost if ` block in hypermode using `rel()` Abierto

SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#993 · 3 comentarios · Abierto el 6/2/2026
Cross execution access bug in `rel()` and `ghost if` blocks Abierto

SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/gobra#992 · 2 comentarios · Abierto el 4/2/2026
Incompleteness: Asserting a syntactically identical assertion fails Abierto

enhancement

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/silver#902 · 2 comentarios · Abierto el 28/1/2026
`rel` Expressions in Triggers Abierto

bug SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/silver#901 · 1 comentario · Abierto el 28/1/2026
Encoding bug when using `rel()` and a wrapper Abierto

SIF

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

viperproject/gobra#987 · 1 comentario · Abierto el 27/1/2026
Asserting after assuming quantifier with heap-dependent trigger fails Abierto

bug incompleteness quantified-permissions

Dificultad 4/5 3-5 días Aptitud para principiantes 38/100

viperproject/silicon#959 · 2 comentarios · Abierto el 15/1/2026
Floating Point Literals Abierto

encoding enhancement

Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

viperproject/gobra#980 · 1 comentario · Abierto el 10/12/2025
A potential bug in how Silicon handles loop invariant Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 38/100

viperproject/silicon#957 · 2 comentarios · Abierto el 9/12/2025
Crash when using a compound data structure in a closure encoding Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#978 · Abierto el 3/12/2025
Confusing error message if ADT type and constructor named alike Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

viperproject/gobra#977 · Abierto el 3/12/2025
Dollars in argument identifiers confuse tab completion Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 45/100

viperproject/viper-ide#533 · Abierto el 27/11/2025
Internal function preconditions not assumed in wand-related scenario Abierto

incompleteness

viperproject/silicon#951 · 1 asignado · Abierto el 24/11/2025

Mostrando los 100 más recientes

Esta página solo lista lo indexado más recientemente. El filtro avanzado tiene el inventario completo, acotado por lenguaje, dificultad y duración.

Abrir el filtro avanzado

viperproject

Mostrando los 100 más recientes

Recibe los nuevos issues en tu correo