erniecohen

erniecohen/dafny

Dafny is a verification-aware programming language

4 good first / help-wanted issues · C# · last activity Oct 4, 2026

0 stars 0 forks 0 watchers C# Other
View on GitHub Website
4 Open Issues Need Help Last updated: Oct 4, 2026

Open Issues Need Help

View All on GitHub
Inconsistent treatment of allocated() 21 days ago
help wanted completeness upstream in-progress codex-false-positive
erniecohen/dafny
0

Dafny is a verification-aware programming language

C#
Failure to prove termination measure decreases on twostate lemmas when decreases clause has nonempty reads frame 21 days ago
help wanted soundness completeness upstream in-progress codex-false-positive
erniecohen/dafny
0

Dafny is a verification-aware programming language

C#
$HeapSucc should be axiomatized as reflexive 21 days ago
help wanted completeness upstream in-progress codex-false-positive
erniecohen/dafny
0

Dafny is a verification-aware programming language

C#
Soundness: heap-update successor contradicts extensional heap restoration 21 days ago
help wanted soundness upstream in-progress codex-false-positive
erniecohen/dafny
0

Dafny is a verification-aware programming language

C#