blob: 51334da86bb96969227714e76082161a61c2fb2b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)
test0 Use Name resolution tests
test1 Use Typechecking tests
test2 Use VC generation
test7 Use Some tests for VCVariety.BlockNested
test20 Use Types introduced in Boogie2
test21 Use Verify Boogie 2 programs
aitest0 Use Constant propagation test
aitest1 Use Linear ineqality test
aitest9 Use Test for the abstract domain of intervals
lock Use SLAM example
test13 Use error messages for failing asserts vs. loop invariants
inline Use Procedure inlining
textbook Use Some textbook examples
test15 Use Benchmarks for error messages
bitvectors Use Smoke tests for bitvectors
smoke Use Soundness smoke testing
test16 Use Tests loop unrolling
codeexpr Use Tests code expressions
prover Use Tests checking various prover options
test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
houdini Use Test for Houdini decision procedure
datatypes Use Test for datatypes
generalizedarray Use Test for generalized array theory
livevars Use STORM benchmarks for testing correctness of live variable analysis
stratifiedinline Use Stratified inlining benchmarks
extractloops Use Extract loops benchmarks
havoc0 Use HAVOC-generated bpl files
dafny0 Dafny Dafny functionality tests
dafny1 Dafny Various Dafny examples
dafny2 Dafny More Dafny examples
VSI-Benchmarks Dafny Solutions to Verified Software Initiative verification challenges
vacid0 Dafny Dafny attempts to VACID Edition 0 benchmarks
vstte2012 Dafny Dafny solutions for the VSTTE 2012 program verification competition
VSComp2010 Dafny Dafny solutions to VSComp (verified software competition) problems
AbsHoudini Postponed Test for abstract houdini
|
