@misc(eclipse,
 title        = "Eclipse Integrated Development Environment",
 url          = "http://www.eclipse.org",
)
@techreport(Back78:situation,
 author       = "Ralph-Johan Back",
 year         = "1978",
 title        = "Program Construction by Situation Analysis",
 type         = "Research Report",
 number       = "6",
 institution  = "Computing Centre, University of Helsinki",
 address      = "Finland",
 url          = "http://crest.abo.fi/publications/public/1978/ProgramConstructionBySituationAnalysisTR.pdf",
)
@article(jBack08b,
 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(inpBaErMa07,
 author       = "Ralph-Johan Back and Johannes Eriksson and Linda Mannila",
 year         = "2007",
 title        = "Teaching the Construction of Correct Programs Using Invariant Based Programming",
 booktitle    = "Proc. of SEEFM 2007",
 publisher    = "South-East European Research Centre",
 pages        = "171--187",
)
@inproceedings(inpBaErMy07,
 author       = "Ralph-Johan Back and Johannes Eriksson and Magnus Myreen",
 year         = "2007",
 title        = "Testing and Verifying Invariant Based Programs in the {SOCOS} Environment",
 booktitle    = "Proc. of Tests and Proofs (TAP) 2007",
 series       = "LNCS",
 volume       = "4454",
 publisher    = "Springer",
 pages        = "61--78",
 doi          = "10.1007/978-3-540-73770-4\_4",
)
@inproceedings(inpBaMy05a,
 author       = "Ralph-Johan Back and Magnus Myreen",
 year         = "2005",
 title        = "Tool Support for Invariant Based Programming",
 booktitle    = "Proc. of APSEC 2005",
 publisher    = "IEEE Computer Society",
 pages        = "711--718",
 doi          = "10.1109/APSEC.2005.104",
)
@inproceedings(back_preoteasa11proofrules,
 author       = "Ralph-Johan Back and Viorel Preoteasa",
 year         = "2011",
 title        = "Semantics and Proof Rules of Invariant Based Programs",
 booktitle    = "26th Symposium On Applied Computing",
 pages        = "1658--1665",
 doi          = "10.1145/1982185.1982532",
)
@inproceedings(barnett_boogie:modular_2006,
 author       = "Mike Barnett and Bor-Yuh~Evan Chang and Robert DeLine and Bart Jacobs and K.~Rustan~M. Leino",
 year         = "2006",
 title        = "Boogie: A modular reusable verifier for object-oriented programs",
 booktitle    = "Proc. of FMCO 2005",
 series       = "LNCS",
 volume       = "4111",
 publisher    = "Springer",
 pages        = "364--387",
 doi          = "10.1007/11804192\_17",
)
@inproceedings(specSharpOverview,
 author       = "Mike Barnett and K.~Rustan~M. Leino and Wolfram Schulte",
 year         = "2004",
 title        = "{The Spec\# programming system: An overview}",
 booktitle    = "CASSIS 2004",
 series       = "LNCS",
 volume       = "3362",
 publisher    = "Springer",
 pages        = "49--69",
 doi          = "10.1007/978-3-540-30569-9\_3",
)
@inproceedings(vandenberg01loop,
 author       = "Joachim van~den Berg and Bart Jacobs",
 year         = "2001",
 title        = "The {LOOP} Compiler for {Java} and {JML}",
 booktitle    = "Proc. of TACAS 2001",
 series       = "LNCS",
 volume       = "2031",
 publisher    = "Springer",
 pages        = "299--312",
 doi          = "10.1007/3-540-45319-9\_21",
)
@book(580470,
 author       = "Thomas~H. Cormen and Clifford Stein and Ronald~L. Rivest and Charles~E. Leiserson",
 year         = "2001",
 title        = "Introduction to Algorithms",
 publisher    = "MIT Press",
)
@article(1066102,
 author       = "David Detlefs and Greg Nelson and James~B. Saxe",
 year         = "2005",
 title        = "Simplify: a theorem prover for program checking",
 journal      = "Journal of the ACM",
 volume       = "52",
 number       = "3",
 pages        = "365--473",
 doi          = "10.1145/1066100.1066102",
)
@techreport(yices,
 author       = "Bruno Dutertre and Leonardo de~Moura",
 year         = "2006",
 title        = "The {Yices} {SMT} solver",
 type         = "Technical Report",
 institution  = "Computer Science Laboratory, SRI International",
 address      = "Menlo Park, CA",
 url          = "http://yices.csl.sri.com/tool-paper.pdf",
)
@article(vEmden79,
 author       = "M.~H. van Emden",
 year         = "1979",
 title        = "Programming with Verification Conditions",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "5",
 number       = "2",
 pages        = "148--159",
 doi          = "10.1109/TSE.1979.234171",
)
@inproceedings(inpErBa10,
 author       = "Johannes Eriksson and Ralph-Johan Back",
 year         = "2010",
 title        = "Applying {PVS} Background Theories and Proof Strategies in Invariant Based Programming",
 booktitle    = "Proc. of ICFEM 2010",
 pages        = "24--39",
 doi          = "10.1007/978-3-642-16901-4\_4",
)
@incollection(citeulike:2868751,
 author       = "Jean-Christophe Filli\^{a}tre and Claude March\'{e}",
 year         = "2007",
 title        = "The {Why}/{Krakatoa}/{Caduceus} Platform for Deductive Program Verification",
 booktitle    = "Proc. of CAV 2007",
 series       = "LNCS",
 volume       = "4590",
 publisher    = "Springer",
 pages        = "173--177",
 doi          = "10.1007/978-3-540-73368-3\_21",
)
@misc(NASALIBS,
 author       = "{NASA Langley Research Center}",
 title        = "{NASA Langley PVS Libraries}",
 url          = "http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html",
)
@inproceedings(owre96pvs,
 author       = "Sam Owre and S.~Rajan and John Rushby and Natarajan Shankar and Mandayam~K. Srivas",
 year         = "1996",
 title        = "{PVS}: Combining specification, proof checking, and model checking",
 booktitle    = "Proc. of {CAV'96}",
 series       = "LNCS",
 volume       = "1102",
 publisher    = "Springer",
 pages        = "411--414",
 doi          = "10.1007/3-540-61474-5\_91",
)
@techreport(PVS-Semantics:TR,
 author       = "Sam Owre and Natarajan Shankar",
 year         = "1997",
 title        = "The Formal Semantics of {PVS}",
 type         = "Technical Report",
 number       = "SRI-CSL-97-2",
 institution  = "Computer Science Laboratory, SRI International",
 address      = "Menlo Park, CA",
 url          = "http://www.csl.sri.com/papers/csl-97-2",
)
@inproceedings(Reynolds78,
 author       = "John~C. Reynolds",
 year         = "1978",
 title        = "Programming with transition diagrams",
 editor       = "D.~Gries",
 booktitle    = "Programming Methodology",
 publisher    = "Springer-Verlag",
 pages        = "153--165",
)
@article(Rushby98:TSE,
 author       = "John Rushby and Sam Owre and {N.} Shankar",
 year         = "1998",
 title        = "Subtypes for Specifications: Predicate Subtyping in {PVS}",
 journal      = "{IEEE} Transactions on Software Engineering",
 volume       = "24",
 number       = "9",
 pages        = "709--720",
 doi          = "10.1109/32.713327",
)