Z3 site has got some very good examples to test concepts out, Usually we we wont write Z3 SMTLIB format directly but use some APIs/bindings available in scala, C++ or Python. Dafny uses Hoare Logic Structure. The "Loop Invariants" part has a nice explanation on what are the problems with loop unrolling. Dafny is based on Boogie which happens to be an IVL.
- Z3 : https://rise4fun.com/Z3/tutorial/guide
- Dafny : https://rise4fun.com/Dafny/tutorial
- Boogie : https://rise4fun.com/Boogie, https://github.com/boogie-org/boogie
- Fuzzing : https://www.carolemieux.com/fuzzfactory_oopsla19.pdf
- DART Testing : https://dl.acm.org/citation.cfm?id=1065036
- Dafny Tutorial Link PDF : https://arxiv.org/pdf/1701.04481.pdf
- Non-Interference : http://csl.sri.com/papers/csl-92-2/csl-92-2.pdf