オーナー

viperproject

索引済みのリポジトリ 13 件 · GitHub で見る

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

Scala · スター 189 個
silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.

Scala · スター 145 個
silver
Definition of the Viper intermediate verification language.

Scala · スター 100 個
carbon
Verification-condition-generation-based verifier for the Viper intermediate verification language.

Scala · スター 38 個
viperserver
HTTP server that manages verification requests to different tools from the Viper tool stack.

Scala · スター 16 個
viper-ide
This is the main repository for the Viper IDE extension for VS Code.

TypeScript · スター 14 個
VerifiedSCION
Verifying the SCION architecture using Gobra

Go · スター 12 個
gobra-ide
VSCode Plugin for Gobra

TypeScript · スター 11 個
vs-verification-toolbox
Useful component to build VS Code extensions for verifiers.

TypeScript · スター 6 個
gobra-book

JavaScript · スター 4 個
gobra-action
Github Action to verify Go code with Gobra directly in a CI workflow

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

Python · スター 2 個
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 個

初心者向けすべて

オープンすべて

quantifiedExp does not apply its `ignore` parameter, unlike `quantified` オープン

難易度 3/5 1〜2日初心者へのやさしさ 68/100

viperproject/silicon#1006 · 2026年9月9日に作成
Termination measures are not checked for closure spec calls オープン

soundness termination-checking

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/gobra#1106 · 2026年9月4日に作成
Termination measures of interface methods are not checked across package boundaries オープン

soundness termination-checking

難易度 5/5 1週間以上初心者へのやさしさ 30/100

viperproject/gobra#1105 · 2026年9月4日に作成
Recursive function plus quantifier that triggers on the function results in matching loop オープン

難易度 5/5 1週間以上初心者へのやさしさ 35/100

viperproject/silicon#1004 · 2026年8月25日に作成
Carbon can prove false オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/carbon#591 · 2026年8月18日に作成
Type checker crashes on addressing an element of a slice obtained from a map lookup オープン

難易度 2/5 1〜3時間初心者へのやさしさ 78/100

viperproject/gobra#1097 · 2026年8月17日に作成
Confusing reason/offending position ID with sequencing operation オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silver#928 · 2026年8月15日に作成
Tutorial.md is severely limited compared to actual *.g4 files オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1093 · 2026年8月15日に作成
Termination plugin fails with unclear error オープン

bug termination plugin

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silver#925 · コメント 1 件 · 2026年8月10日に作成
Unclear error message when injectivity check fails in a subexpression オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silicon#997 · 2026年8月10日に作成
Quantified predicate permission over freshly-allocated pointers fails injectivity check, even for provably-fresh allocations オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1060 · 2026年7月31日に作成
Pure interface method's definitional axiom does not fire through interface dispatch when the method recurses through another interface-typed call オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/gobra#1059 · 2026年7月30日に作成
Cannot prove non-nil after make オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1052 · コメント 2 件 · 2026年7月19日に作成
It is unnecessarily hard to prove injectivity of slices of struct pointers オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1051 · 2026年7月18日に作成
Anonymous methods オープン

enhancement

難易度 5/5 1週間以上初心者へのやさしさ 35/100

viperproject/silver#922 · 2026年7月13日に作成
Forward goto after variable declaration causes crash オープン

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/silicon#991 · 2026年7月10日に作成
Doing bitvector work in cvc5 puts the solver in a broken state オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silicon#990 · 2026年7月10日に作成
Conjunction of abstract functions is not able to be asserted オープン

難易度 4/5 3〜5日初心者へのやさしさ 52/100

viperproject/carbon#588 · 2026年7月10日に作成
Conjunction of abstract functions is not able to be asserted オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/silicon#989 · コメント 1 件 · 2026年7月10日に作成
Irreducible CFG error reporting is not useful オープン

難易度 5/5 1週間以上初心者へのやさしさ 35/100

viperproject/silver#918 · 2026年6月23日に作成
Proposed annotation: verified — heap-free function postconditions as domain axioms オープン

encoding enhancement syntax

難易度 5/5 1週間以上初心者へのやさしさ 35/100

viperproject/gobra#1037 · コメント 9 件 · 2026年6月14日に作成
Inconsistent treatment of recursive function postconditions オープン

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silver#913 · 2026年5月21日に作成
Invalid Triggers via Subslicing オープン

bug encoding invalid triggers

難易度 4/5 3〜5日初心者へのやさしさ 42/100

viperproject/gobra#1030 · コメント 1 件 · 2026年5月13日に作成
Wands are not checked for self-framingness オープン

magic-wands

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silicon#974 · 2026年5月7日に作成
Gobra does not immediately realize semantics of copying arrays by assignment オープン

bug encoding incompleteness

難易度 3/5 1〜2日初心者へのやさしさ 48/100

viperproject/gobra#1027 · コメント 6 件 · 2026年5月6日に作成
Can prove nil-ness and non-nilness from struct predicate オープン

documentation

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1025 · コメント 5 件 · 2026年5月4日に作成
Question on Injectivity オープン

難易度 3/5 1〜2日初心者へのやさしさ 52/100

viperproject/gobra-book#50 · 2026年4月30日に作成
Wildcard permissions don't work inside predicate bodies オープン

難易度 4/5 3〜5日初心者へのやさしさ 38/100

viperproject/carbon#584 · 2026年4月23日に作成
Carbon does not "frame" trigger-matching heap-dependent functions which depend on QPs (without help) オープン

難易度 5/5 1週間以上初心者へのやさしさ 35/100

viperproject/carbon#583 · コメント 1 件 · 2026年4月17日に作成
Diagnostics count on errors is global オープン

viperproject/viper-ide#566 · リアクション 1 件 · 担当者 2 名 · 2026年3月26日に作成
Incorrect encoding of relational predicates オープン

SIF

難易度 4/5 3〜5日初心者へのやさしさ 48/100

viperproject/silver#907 · コメント 1 件 · 2026年3月24日に作成
Clean up createRequire workarounds once VS Code ESM support is fixed オープン

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/vs-verification-toolbox#227 · 2026年3月5日に作成
Incomplete Slice Allocation Spec オープン

encoding enhancement

難易度 3/5 1〜2日初心者へのやさしさ 52/100

viperproject/gobra#1007 · 2026年3月4日に作成
Parser Error for Reserved Keywords オープン

enhancement parsing

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#1005 · 2026年3月2日に作成
Allow impure assertions for `assert by` オープン

feature-request

難易度 3/5 1〜2日初心者へのやさしさ 38/100

viperproject/gobra#999 · 2026年2月24日に作成
Invalid SMT Encoding オープン

bug encoding

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/gobra#997 · 2026年2月20日に作成
Unintuitive semantics for mixed non-hyper-predicates and hyper-predicates オープン

documentation SIF

難易度 5/5 1週間以上初心者へのやさしさ 30/100

viperproject/gobra#996 · コメント 10 件 · 2026年2月17日に作成
Using `rel(t,0) < rel(t,1)` with implication in SIF mode causes an error. オープン

SIF

難易度 4/5 3〜5日初心者へのやさしさ 32/100

viperproject/gobra#994 · コメント 2 件 · 2026年2月11日に作成
Assert might fail even defined before the `ghost if ` block in hypermode using `rel()` オープン

SIF

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#993 · コメント 3 件 · 2026年2月6日に作成
Cross execution access bug in `rel()` and `ghost if` blocks オープン

SIF

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/gobra#992 · コメント 2 件 · 2026年2月4日に作成
Incompleteness: Asserting a syntactically identical assertion fails オープン

enhancement

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/silver#902 · コメント 2 件 · 2026年1月28日に作成
`rel` Expressions in Triggers オープン

bug SIF

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/silver#901 · コメント 1 件 · 2026年1月28日に作成
Encoding bug when using `rel()` and a wrapper オープン

SIF

難易度 4/5 3〜5日初心者へのやさしさ 35/100

viperproject/gobra#987 · コメント 1 件 · 2026年1月27日に作成
Asserting after assuming quantifier with heap-dependent trigger fails オープン

bug incompleteness quantified-permissions

難易度 4/5 3〜5日初心者へのやさしさ 38/100

viperproject/silicon#959 · コメント 2 件 · 2026年1月15日に作成
Floating Point Literals オープン

encoding enhancement

難易度 5/5 1週間以上初心者へのやさしさ 30/100

viperproject/gobra#980 · コメント 1 件 · 2025年12月10日に作成
A potential bug in how Silicon handles loop invariant オープン

難易度 4/5 3〜5日初心者へのやさしさ 38/100

viperproject/silicon#957 · コメント 2 件 · 2025年12月9日に作成
Crash when using a compound data structure in a closure encoding オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#978 · 2025年12月3日に作成
Confusing error message if ADT type and constructor named alike オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

viperproject/gobra#977 · 2025年12月3日に作成
Dollars in argument identifiers confuse tab completion オープン

難易度 3/5 1〜2日初心者へのやさしさ 45/100

viperproject/viper-ide#533 · 2025年11月27日に作成
Internal function preconditions not assumed in wand-related scenario オープン

incompleteness

viperproject/silicon#951 · 担当者 1 名 · 2025年11月24日に作成

viperproject

最新の 100 件のみ表示しています

新しい issue をメールで受け取る