Proprietario

viperproject

13 repository indicizzati · Vedi su GitHub

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

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

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

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

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

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

TypeScript · 14 stelle
VerifiedSCION
Verifying the SCION architecture using Gobra

Go · 12 stelle
gobra-ide
VSCode Plugin for Gobra

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

TypeScript · 6 stelle
gobra-book

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

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

Python · 2 stelle
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 stelle

Adatte ai principianti Tutto

Aperta Tutte

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 68/100

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

soundness termination-checking

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

soundness termination-checking

Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100

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

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

viperproject/silicon#1004 · Aperta il 25/8/2026
Carbon can prove false Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/gobra#1093 · Aperta il 15/8/2026
Termination plugin fails with unclear error Aperta

bug termination plugin

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

viperproject/silver#925 · 1 commento · Aperta il 10/8/2026
Unclear error message when injectivity check fails in a subexpression Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/gobra#1052 · 2 commenti · Aperta il 19/7/2026
It is unnecessarily hard to prove injectivity of slices of struct pointers Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/gobra#1051 · Aperta il 18/7/2026
Anonymous methods Aperta

enhancement

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/silicon#989 · 1 commento · Aperta il 10/7/2026
Irreducible CFG error reporting is not useful Aperta

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

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

encoding enhancement syntax

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

viperproject/gobra#1037 · 9 commenti · Aperta il 14/6/2026
Inconsistent treatment of recursive function postconditions Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

viperproject/silver#913 · Aperta il 21/5/2026
Invalid Triggers via Subslicing Aperta

bug encoding invalid triggers

Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100

viperproject/gobra#1030 · 1 commento · Aperta il 13/5/2026
Wands are not checked for self-framingness Aperta

magic-wands

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

bug encoding incompleteness

Difficoltà 3/5 1-2 giorni Idoneità per principianti 48/100

viperproject/gobra#1027 · 6 commenti · Aperta il 6/5/2026
Can prove nil-ness and non-nilness from struct predicate Aperta

documentation

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/gobra#1025 · 5 commenti · Aperta il 4/5/2026
Question on Injectivity Aperta

Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

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

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

viperproject/carbon#583 · 1 commento · Aperta il 17/4/2026
Diagnostics count on errors is global Aperta

viperproject/viper-ide#566 · 1 reazione · 2 assegnatari · Aperta il 26/3/2026
Incorrect encoding of relational predicates Aperta

SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

viperproject/silver#907 · 1 commento · Aperta il 24/3/2026
Clean up createRequire workarounds once VS Code ESM support is fixed Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

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

encoding enhancement

Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100

viperproject/gobra#1007 · Aperta il 4/3/2026
Parser Error for Reserved Keywords Aperta

enhancement parsing

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

feature-request

Difficoltà 3/5 1-2 giorni Idoneità per principianti 38/100

viperproject/gobra#999 · Aperta il 24/2/2026
Invalid SMT Encoding Aperta

bug encoding

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

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

documentation SIF

Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100

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

SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 32/100

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

SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

viperproject/gobra#993 · 3 commenti · Aperta il 6/2/2026
Cross execution access bug in `rel()` and `ghost if` blocks Aperta

SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

viperproject/gobra#992 · 2 commenti · Aperta il 4/2/2026
Incompleteness: Asserting a syntactically identical assertion fails Aperta

enhancement

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

viperproject/silver#902 · 2 commenti · Aperta il 28/1/2026
`rel` Expressions in Triggers Aperta

bug SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

viperproject/silver#901 · 1 commento · Aperta il 28/1/2026
Encoding bug when using `rel()` and a wrapper Aperta

SIF

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

viperproject/gobra#987 · 1 commento · Aperta il 27/1/2026
Asserting after assuming quantifier with heap-dependent trigger fails Aperta

bug incompleteness quantified-permissions

Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

viperproject/silicon#959 · 2 commenti · Aperta il 15/1/2026
Floating Point Literals Aperta

encoding enhancement

Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100

viperproject/gobra#980 · 1 commento · Aperta il 10/12/2025
A potential bug in how Silicon handles loop invariant Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

viperproject/silicon#957 · 2 commenti · Aperta il 9/12/2025
Crash when using a compound data structure in a closure encoding Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 45/100

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

incompleteness

viperproject/silicon#951 · 1 assegnatario · Aperta il 24/11/2025

Vengono mostrati i 100 più recenti

Questa pagina elenca solo ciò che è stato indicizzato di recente. Il filtro avanzato contiene l'inventario completo, ristretto per linguaggio, difficoltà e durata.

Apri il filtro avanzato

viperproject

Vengono mostrati i 100 più recenti

Ricevi le nuove issue nella tua casella