19. References#
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: a modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, volume 4111 of lncs, 364–387. Springer, September 2006.
Leonardo de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS 2008, volume 4963 of lncs, 337–340. Springer, mar–apr 2008.
K. Rustan M. Leino. Main microsoft research dafny web page. 2008. Available at http://research.microsoft.com/en-us/projects/dafny.
K. Rustan M. Leino. This is Boogie 2. Manuscript KRML 178, 2008. Available at http://research.microsoft.com/ leino/papers.html.
K. Rustan M. Leino. Dafny: an automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, LPAR-16, volume 6355 of lncs, 348–370. Springer, April 2010.
K. Rustan M. Leino and Michal Moskal. Co-induction simply: automatic co-inductive proofs in a program verifier. Manuscript KRML 230, 2014. Available at http://research.microsoft.com/en-us/um/people/leino/papers/krml230.pdf.
K. Rustan M. Leino and Nadia Polikarpova. Verified calculations. Manuscript KRML 231, 2013. Available at http://research.microsoft.com/en-us/um/people/leino/papers/krml231.pdf.
Hanspeter Mössenböck, Markus Löberbauer, and Albrecht Wöß. The compiler generator coco/r. Open source from University of Linz, 2013. Available at http://www.ssw.uni-linz.ac.at/Research/Projects/Coco/.