viperproject/silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.
ScalaMPL-2.0
Issues
- 0
- 3
Avoiding double QI across (pop)
#702 opened - 1
- 2
- 13
Unknown QP unsoundness
#695 opened - 1
Exhaling an empty QP allows asserting false
#688 opened - 0
- 2
Assertion mode option is broken
#676 opened - 3
--help fails with an exception
#665 opened - 2
Z3 regression in 4.8.10
#664 opened - 8
Triggers silently ignored/replaced
#661 opened - 5
External parallelization of Silicon
#660 opened - 4
Limited functions
#658 opened - 5
- 2
Potential unsoundness
#652 opened - 1
- 0
Strange filename ending `.silver`
#647 opened - 2
- 8
- 2
Unsoundness with quantified permissions
#636 opened - 0
Silicon verifies example that should fail.
#630 opened - 2
Problem with inequality of sequences
#629 opened - 2
- 2
- 1
NoPosition causes spaces in z3 log
#621 opened - 0
z3 trace-file-name
#618 opened - 0
Silicon cannot find z3 in PATH
#617 opened - 0
- 1
- 0
- 6
Error deduplication + NoPosition
#613 opened - 2
- 2
- 1
- 3
- 1
- 2
Old on a local variable affects triggering
#603 opened - 1
- 1
Difficulty proving sequence inequality
#601 opened - 6
- 1
- 2
- 3
- 3
Proving forall with only 1 wildcard
#591 opened - 3
Report inferred triggers
#586 opened - 1
- 3
- 3
Memory leaks in Silicon
#579 opened - 0
Data race while loading builtin domains
#578 opened - 1
Predicate-Related Incompleteness
#577 opened