viperproject/silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.
ScalaMPL-2.0
Issues
- 2
- 0
- 3
- 0
- 0
- 0
Weird behavior if WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException
#850 opened - 3
`FuncApp` in axioms
#847 opened - 2
- 2
- 2
- 0
Unsound behavior with QPs without condition
#833 opened - 4
- 4
- 3
- 1
- 0
Using --help crashes Silicon (again)
#819 opened - 1
- 0
Potential unsoundness
#810 opened - 2
Function body needs to be asserted manually
#803 opened - 0
Tests non-deterministically time out
#801 opened - 0
- 1
- 3
- 2
- 1
- 0
Unexpected assertion failure when using --setAxiomatizationFile without axioms and variables
#779 opened - 0
- 2
- 0
Map-related unsoundness
#769 opened - 1
- 2
- 3
- 1
- 1
Crash with "unknown function/constant"
#749 opened - 1
Recommended stack size
#748 opened - 6
Unrolling loops blows up verification time
#747 opened - 1
- 2
- 2
Unsoundness due to loop invariant
#740 opened - 0
- 5
Reporting multiple errors
#735 opened - 6
- 10
Efficient solver initialization by cloning
#731 opened - 1
--numberOfParallelVerifiers 0 causes NPE
#726 opened - 2
Missing hashCode definitions
#723 opened - 0
- 0
Crash due to "unknown constant"
#715 opened - 3
State merging failed due to inequal `quantifiedVariables` with `--conditionalizePermissions`
#713 opened - 1
Crash on example with "unknown symbol"
#711 opened - 1
Support for SMT literals
#707 opened