blob: baffc2a11e5a16acd6cdc724303b1532fa107d56 (
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
|
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
dafny0 Use Dafny functionality tests
dafny1 Use Various Dafny examples
dafny2 Use More Dafny examples
havoc0 Use HAVOC-generated bpl files
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
livevars Use STORM benchmarks for testing correctness of live variable analysis
lazyinline Postponed Lazy inlining benchmarks
stratifiedinline Use Stratified inlining benchmarks
extractloops Use Extract loops benchmarks
VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
|
