1 files changed, 48 insertions, 0 deletions
diff --git a/Docs/DafnyRef/DafnyRef.bib b/Docs/DafnyRef/DafnyRef.bib
new file mode 100644
index 00000000..9a2a5a5b
--- /dev/null
+++ b/Docs/DafnyRef/DafnyRef.bib
@@ -0,0 +1,48 @@
+@Misc{Rise4fun:dafny,
+  author = {K. Rustan  M. Leino},
+  title = {Try Dafny In Your Browser},
+  note = "Available at \url{http://rise4fun.com/Dafny}"
+}
+@Misc{MSR:dafny:main,
+  author = {K. Rustan  M. Leino},
+  title = {Main Microsoft Research Dafny Web page},
+  note = "Available at \url{http://research.microsoft.com/en-us/projects/dafny}"
+}
+@Misc{MSR:dafny:source,
+  author = {K. Rustan  M. Leino et al},
+  title = {Dafny Source Code},
+  note = "Available at \url{http://dafny.codeplex.com}"
+}
+@Misc{MSR:dafny:quickref,
+  author = {K. Rustan  M. Leino},
+  title = {Dafny Quick Reference},
+  note = "Available at \url{http://research.microsoft.com/en-us/projects/dafny/reference.aspx}"
+}
+@Misc{Linz:Coco,
+  author = {Hanspeter M{\"{o}}ssenb{\"{o}}ck and Markus L{\"{o}}berbauer and Albrecht W{\"{o}}{\ss}},
+  title = {The Compiler Generator Coco/R},
+  howpublished = {Open source from University of Linz},
+  year = 2013,
+  note = "Available at \url{http://www.ssw.uni-linz.ac.at/Research/Projects/Coco/}"
+}
+@Misc{LEINO:Dafny:Calc,
+  author = {K. Rustan M. Leino and Nadia Polikarpova},
+  title = {Verified Calculations},
+  howpublished = {Manuscript KRML 231},
+  year = 2013,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/krml231.pdf}"
+}
+@Misc{LEINO:Dafny:Coinduction,
+  author = {K. Rustan M. Leino and Michal Moskal},
+  title = {Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier},
+  howpublished = {Manuscript KRML 230},
+  year = 2014,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/krml230.pdf}" 
+}
+@Misc{LEINO:Dafny:DynamicFrames,
+  author = {K. Rustan M. Leino},
+  title = {Dynamic-frame specifications in Dafny},
+  howpublished = {JML seminar, Dagstuhl, Germany},
+  year = 2009,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/dafny-jml-dagstuhl-2009.pptx}"
+}