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 SoonToBeIncluded 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 Use Dafny functionality tests dafny1 Use Various Dafny examples dafny2 Use More Dafny examples 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 VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems