@book(Back,
 author       = "R.-J. Back and J. von Wright",
 year         = "1998",
 title        = "{Refinement Calculus: A Systematic Introduction}",
 publisher    = "Springer",
 address      = "New York",
)
@article(Back2009,
 author       = "Ralph-Johan Back",
 year         = "2009",
 title        = "{Invariant Based Programming: Basic Approach and Teaching Experiences}",
 journal      = "Formal Aspects of Computing",
 volume       = "21",
 number       = "3",
 pages        = "227--244",
 doi          = "10.1007/s00165-008-0070-y",
)
@inproceedings(CVCL,
 author       = "Clark Barrett and Sergey Berezin",
 year         = "2004",
 title        = "{CVC Lite: A New Implementation of the Cooperating Validity Checker}",
 booktitle    = "Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13--17, 2004",
 series       = "LNCS",
 volume       = "3114",
 publisher    = "Springer",
 pages        = "515--518",
 doi          = "10.1007/978-3-540-27813-9\_49",
)
@book(KeYBook2007,
 editor       = "Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt",
 year         = "2007",
 title        = "{Verification of Object-Oriented Software: The {KeY} Approach}",
 series       = "LNCS",
 volume       = "4334",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-69061-0",
)
@proceedings(TFM2006,
 editor       = "P. Boca and J. P. Bowen and D. A. Duce",
 year         = "2006",
 title        = "{Teaching Formal Methods: Practice and Experience}",
 series       = "Electronic Workshops in Computing (eWIC)",
 publisher    = "British Computer Society",
 address      = "London, UK, December 16",
 note         = "\url {http://www.bcs.org/category/8726}",
)
@article(Boute,
 author       = "Raymond T.\ Boute",
 year         = "2006",
 title        = "{Calculational Semantics: Deriving Programming Theories from Equations by Functional Predicate Calculus}",
 journal      = "ACM Transactions on Programming Languages and Systems",
 volume       = "28",
 number       = "4",
 pages        = "747--793",
 doi          = "10.1145/1146809.1146814",
)
@article(JML,
 author       = "Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll",
 year         = "2005",
 title        = "{An Overview of JML Tools and Applications}",
 journal      = "International Journal on Software Tools for Technology Transfer",
 volume       = "7",
 pages        = "212--232",
 doi          = "10.1007/s10009-004-0167-4",
)
@proceedings(TFM2004,
 editor       = "C. Neville Dean and Raymond T. Boute",
 year         = "2004",
 title        = "{Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18--19, 2004}",
 series       = "LNCS",
 volume       = "3294",
 publisher    = "Springer",
 doi          = "10.1007/b102075",
)
@article(Dijkstra1968,
 author       = "Edsger W. Dijkstra",
 year         = "1968",
 title        = "{A Constructive Approach to the Problem of Program Correctness}",
 journal      = "BIT Numerical Mathematics",
 volume       = "8",
 number       = "3",
 pages        = "174--186",
 doi          = "10.1007/BF01933419",
)
@article(Feinerer2009,
 author       = "Ingo Feinerer and Gernot Salzer",
 year         = "2009",
 title        = "{A Comparison of Tools for Teaching Formal Software Verification}",
 journal      = "Formal Aspects of Computing",
 volume       = "21",
 number       = "3",
 pages        = "293--301",
 doi          = "10.1007/s00165-008-0084-5",
)
@inproceedings(FilliatreM07,
 author       = "Jean-Christophe Filli{\^a}tre and Claude March{\'e}",
 year         = "2007",
 title        = "The Why/Krakatoa/Caduceus Platform for Deductive Program Verification",
 booktitle    = "Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007",
 series       = "LNCS",
 volume       = "4590",
 publisher    = "Springer",
 pages        = "173--177",
 doi          = "10.1007/978-3-540-73368-3\_21",
)
@proceedings(TFM2009,
 editor       = "Jeremy Gibbons and Jos{\'e} Nuno Oliveira",
 year         = "2009",
 title        = "{Teaching Formal Methods, Second International Conference, TFM 2009, Eindhoven, The Netherlands, November 2--6, 2009}",
 series       = "Lecture Notes in Computer Science",
 volume       = "5846",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-04912-5",
)
@misc(Gordon,
 author       = "Mike Gordon",
 year         = "2010",
 title        = "{Specification and Verification I}",
 note         = "University of Cambridge, UK, Lecture Notes, \url {http://www.cl.cam.ac.uk/~mjcg/Lectures/SpecVer1/SpecVer1.html}",
)
@book(Hehner,
 author       = "Eric C.R. Hehner",
 year         = "2006",
 title        = "A Practical Theory of Programming",
 publisher    = "Springer",
 address      = "New York",
 note         = "\url {http://www.cs.utoronto.ca/\~hehner/aPToP}",
)
@book(HoareJifeng,
 author       = "C.A.R. Hoare and He Jifeng",
 year         = "1998",
 title        = "{Unifying Theories of Programming}",
 publisher    = "Prentice Hall",
 address      = "London, UK",
 url          = "http://www.unifyingtheories.org",
)
@book(Lamport2002,
 author       = "Leslie Lamport",
 year         = "2002",
 title        = "{Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers}",
 publisher    = "Addison-Wesley",
 url          = "http://research.microsoft.com/users/lamport/tla/book.html",
)
@book(Morgan,
 author       = "Carroll Morgan",
 year         = "1998",
 title        = "{Programming from Specifications}",
 edition      = "2nd",
 publisher    = "Prentice Hall",
 address      = "London, UK",
 url          = "http://www.cs.ox.ac.uk/publications/books/PfS",
)
@article(Morris,
 author       = "J. M. Morris",
 year         = "1987",
 title        = "{A Theoretical Basis for Stepwise Refinement and the Programming Calculus}",
 journal      = "Science of Computer Programming",
 volume       = "9",
 number       = "3",
 pages        = "287--306",
 doi          = "10.1016/0167-6423(87)90011-6",
)
@inproceedings(Oliveira2004,
 author       = "Jos{\'e} Nuno Oliveira",
 year         = "2004",
 title        = "A Survey of Formal Methods Courses in European Higher Education",
 booktitle    = "\cite {TFM2004}",
 pages        = "235--248",
 doi          = "10.1007/978-3-540-30472-2\_16",
)
@inproceedings(PVS,
 author       = "S. Owre and J. M. Rushby and N. Shankar",
 year         = "1992",
 title        = "{PVS: A Prototype Verification System}",
 editor       = "Deepak Kapur",
 booktitle    = "11th International Conference on Automated Deduction (CADE)",
 series       = "Lecture Notes in Artificial Intelligence",
 volume       = "607",
 publisher    = "Springer",
 address      = "Saratoga, NY, June 14--18",
 pages        = "748--752",
 doi          = "10.1007/3-540-55602-8\_217",
)
@book(Schmidt1986,
 author       = "David A. Schmidt",
 year         = "1986",
 title        = "{Denotational Semantics -- A Methodology for Language Development}",
 publisher    = "Allyn and Bacon",
 address      = "Boston, MA",
 url          = "http://people.cis.ksu.edu/~schmidt/text/densem.html",
)
@techreport(Schreiner2008c,
 author       = "Wolfgang Schreiner",
 year         = "2008",
 title        = "{A Program Calculus}",
 type         = "Technical Report",
 institution  = "RISC",
 address      = "Johannes Kepler University, Linz, Austria",
 note         = "\url {http://www.risc.jku.at/people/schreine/papers/ProgramCalculus2008.pdf}",
)
@techreport(Schreiner2008b,
 author       = "Wolfgang Schreiner",
 year         = "2008",
 title        = "{Understanding Programs}",
 type         = "Technical Report",
 institution  = "Research Institute for Symbolic Computation (RISC)",
 address      = "Johannes Kepler University, Linz, Austria",
 note         = "\url {http://www.risc.uni-linz.ac.at/people/schreine/papers/Understanding2008.pdf}",
)
@article(Schreiner2008,
 author       = "Wolfgang Schreiner",
 year         = "2009",
 title        = "{The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom}",
 journal      = "Formal Aspects of Computing",
 volume       = "21",
 number       = "3",
 pages        = "277--291",
 doi          = "10.1007/s00165-008-0069-4",
)