@misc(altergo-web,
 note         = "Alt-ergo: \url {http://alt-ergo.lri.fr/}",
)
@inproceedings(Barnett-Leino05,
 author       = "Mike Barnett and K. Rustan M. Leino",
 year         = "2005",
 title        = "Weakest-precondition of unstructured programs",
 editor       = "Michael D. Ernst and Thomas P. Jensen",
 booktitle    = "Program Analysis For Software Tools and Engineering (PASTE)",
 publisher    = "ACM",
 doi          = "10.1145/1108792.1108813",
)
@incollection(SpecSharp2005,
 author       = "Mike Barnett and K. Rustan M. Leino and Wolfram Schulte",
 year         = "2005",
 title        = "The Spec\# Programming System: An Overview",
 editor       = "Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet and Traian Muntean",
 booktitle    = "Construction and Analysis of Safe, Secure, and Interoperable Smart Devices",
 series       = "Lecture Notes in Computer Science",
 volume       = "3362",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "49--69",
 doi          = "10.1007/978-3-540-30569-9\_3",
)
@techreport(BarST-RR-10,
 author       = "Clark Barrett and Aaron Stump and Cesare Tinelli",
 year         = "2010",
 title        = "{The SMT-LIB Standard: Version 2.0}",
 type         = "Technical Report",
 institution  = "Department of Computer Science, The University of Iowa",
 url          = "http://www.SMT-LIB.org",
)
@inproceedings(BarST-SMT-10,
 author       = "Clark Barrett and Aaron Stump and Cesare Tinelli",
 year         = "2010",
 title        = "{The SMT-LIB Standard: Version 2.0}",
 editor       = "A. Gupta and D. Kroening",
 booktitle    = "Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England)",
 url          = "http://www.smt-lib.org",
)
@misc(ACSL,
 author       = "P. Baudin",
 title        = "{ACSL}: {ANSI C Specification Language}",
 note         = "\url {http://frama-c.com/download/acsl_1.4.pdf}",
)
@book(beckert2007verification,
 author       = "Bernhard Beckert and Reiner H\"{a}hnle and Peter H. Schmitt",
 year         = "2007",
 title        = "Verification of object-oriented software : {The KeY Approach}",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-69061-0",
)
@book(opac-b1101046,
 author       = "Yves Bertot and Pierre Castéran",
 year         = "2004",
 title        = "Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions",
 series       = "Texts in theoretical computer science",
 publisher    = "Springer",
 address      = "Berlin, New York",
 doi          = "10.1007/978-3-662-07964-5",
 url          = "http://opac.inria.fr/record=b1101046",
)
@inproceedings(Blanc:2013:OLV:2489837.2489838,
 author       = "R{\'e}gis Blanc and Viktor Kuncak and Etienne Kneuss and Philippe Suter",
 year         = "2013",
 title        = "An Overview of the Leon Verification System: Verification by Translation to Recursive Functions",
 booktitle    = "Proceedings of the 4th Workshop on Scala",
 series       = "SCALA '13",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "1:1--1:10",
 doi          = "10.1145/2489837.2489838",
)
@inproceedings(Burdy-etal03,
 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         = "2003",
 title        = "An overview of {JML} tools and applications",
 editor       = "Thomas Arts and Wan Fokkink",
 booktitle    = "Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03)",
 series       = "Electronic Notes in Theoretical Computer Science (ENTCS)",
 volume       = "80",
 publisher    = "Elsevier",
 pages        = "73--89",
 doi          = "10.1016/S1571-0661(04)80810-7",
)
@misc(Clang,
 note         = "Clang: \url {http://clang.llvm.org/}",
)
@misc(CodeSurfer,
 note         = "CodeSurfer: \url {http://www.grammatech.com/research/technologies/codesurfer}",
)
@incollection(VCC,
 author       = "Ernie Cohen and Markus Dahlweid and Mark Hillebrand and Dirk Leinenbach and Michał Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies",
 year         = "2009",
 title        = "VCC: A Practical System for Verifying Concurrent C",
 editor       = "Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel",
 booktitle    = "Theorem Proving in Higher Order Logics",
 series       = "Lecture Notes in Computer Science",
 volume       = "5674",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "23--42",
 doi          = "10.1007/978-3-642-03359-9\_2",
)
@incollection(Cok-2011-jSMTLIB,
 author       = "David R. Cok",
 year         = "2011",
 title        = "{jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2}",
 editor       = "Mihaela Bobaru and Klaus Havelund and GerardJ. Holzmann and Rajeev Joshi",
 booktitle    = "NASA Formal Methods",
 series       = "Lecture Notes in Computer Science",
 volume       = "6617",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "480--486",
 doi          = "10.1007/978-3-642-20398-5\_36",
)
@incollection(Cok-2011-OpenJML,
 author       = "David R. Cok",
 year         = "2011",
 title        = "OpenJML: JML for Java 7 by Extending OpenJDK",
 editor       = "Mihaela Bobaru and Klaus Havelund and GerardJ. Holzmann and Rajeev Joshi",
 booktitle    = "NASA Formal Methods",
 series       = "Lecture Notes in Computer Science",
 volume       = "6617",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "472--479",
 doi          = "10.1007/978-3-642-20398-5\_35",
)
@article(Cok-2014-OpenJML,
 author       = "David R. Cok",
 year         = "2014",
 title        = "{OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse}",
 journal      = "{Electronic Proceedings in Theoretical Computer Science (EPTCS)}",
 note         = "To appear.",
)
@inproceedings(Kiniry-Cok05,
 author       = "David R. Cok and Joseph R. Kiniry",
 year         = "2005",
 title        = "{ESC/Java2}: Uniting {ESC/Java} and {JML}: Progress and issues in building and using {ESC/Java2}, including a case study involving the use of the tool to verify portions of an {Internet} voting tally system",
 editor       = "Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet and Traian Muntean",
 booktitle    = "Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004)",
 series       = "Lecture Notes in Computer Science",
 volume       = "3362",
 publisher    = "Springer-Verlag",
 pages        = "108--128",
 doi          = "10.1007/b105030",
)
@misc(webcvc4,
 note         = "CVC4: \url {http://cvc4.cs.nyu.edu}",
)
@inproceedings(DeMoura:2008:ZES:1792734.1792766,
 author       = "Leonardo De Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "{Z3: An Efficient SMT Solver}",
 booktitle    = "Proceedings of the Theory and Practice of Software",
 series       = "TACAS'08/ETAPS'08",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "337--340",
 url          = "http://portal.acm.org/citation.cfm?id=1792734.1792766",
)
@techreport(Detlefs-Nelson-Saxe03,
 author       = "David Detlefs and Greg Nelson and James B. Saxe",
 year         = "2003",
 title        = "{Simplify: A Theorem Prover for Program Checking}",
 type         = "Technical Report",
 number       = "HPL-2003-148",
 institution  = "HP Labs",
 url          = "http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf",
)
@article(ErnstPGMPTX2007,
 author       = "Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and Chen Xiao",
 year         = "2007",
 title        = "The {Daikon} system for dynamic detection of likely invariants",
 journal      = "Science of Computer Programming",
 volume       = "69",
 number       = "1--3",
 pages        = "35--45",
 doi          = "10.1016/j.scico.2007.01.015",
)
@incollection(Why3,
 author       = "Jean-Christophe Filliâtre and Andrei Paskevich",
 year         = "2013",
 title        = "Why3 --- Where Programs Meet Provers",
 editor       = "Matthias Felleisen and Philippa Gardner",
 booktitle    = "Programming Languages and Systems",
 series       = "Lecture Notes in Computer Science",
 volume       = "7792",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "125--128",
 doi          = "10.1007/978-3-642-37036-6\_8",
)
@article(FlanaganSaxe01,
 author       = "Cormac Flanagan and James B. Saxe",
 year         = "2001",
 title        = "Avoiding exponential explosion: generating compact verification conditions",
 journal      = "SIGPLAN Not.",
 volume       = "36",
 number       = "3",
 pages        = "193--205",
 doi          = "10.1145/373243.360220",
)
@misc(webframac,
 note         = "Frama-C: \url {http://frama-c.com/}",
)
@book(Paul94,
 author       = "{L. Paulson}",
 year         = "1994",
 title        = "{I}sabelle: {A} {G}eneric {T}heorem {P}rover",
 series       = "Lecture Notes in Computer Science",
 volume       = "828",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/BFb0030541",
)
@article(Leino05,
 author       = "K. Rustan M. Leino",
 year         = "2005",
 title        = "Efficient weakest preconditions",
 journal      = "Inf. Process. Lett.",
 volume       = "93",
 number       = "6",
 pages        = "281--288",
 doi          = "10.1016/j.ipl.2004.10.015",
)
@inproceedings(Leino:Dafny:LPAR16,
 author       = "K. Rustan M. Leino",
 year         = "2010",
 title        = "Dafny: An Automatic Program Verifier for Functional Correctness",
 editor       = "Edmund M. Clarke and Andrei Voronkov",
 booktitle    = "LPAR-16",
 series       = "Lecture Notes in Computer Science",
 volume       = "6355",
 publisher    = "Springer",
 pages        = "348--370",
 doi          = "10.1007/978-3-642-17511-4\_20",
 url          = "http://dl.acm.org/citation.cfm?id=1939141.1939161",
)
@techreport(Leino-Nelson-Saxe00,
 author       = "K. Rustan M. Leino and Greg Nelson and James B. Saxe",
 year         = "2000",
 title        = "{ESC/Java} User's Manual",
 type         = "Technical Note",
 institution  = "Compaq Systems Research Center",
 url          = "http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-2000-002.pdf?jumpid=reg_R1002_USEN",
)
@article(Dafny2014,
 author       = "K. Rustan M. Leino and Valentin W\"ustholz",
 year         = "2014",
 title        = "{The Dafny Integrated Development Environment}",
 journal      = "{Electronic Proceedings in Theoretical Computer Science (EPTCS)}",
 note         = "To appear.",
)
@inproceedings(cade92-pvs,
 author       = "{S.} Owre and {J.} {M.} Rushby and  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-Verlag",
 address      = "Saratoga, {NY}",
 pages        = "748--752",
 doi          = "10.1007/3-540-55602-8\_217",
 url          = "http://www.csl.sri.com/papers/cade92-pvs/",
)
@manual(OwrShaRusStr01b,
 author       = "Sam Owre and Natarajan Shankar and John M. Rushby and David W. J. Stringer-Calvert",
 year         = "2001",
 title        = "{PVS} Language Reference",
 organization = "SRI International",
 url          = "http://pvs.csl.sri.com/doc/pvs-language-reference.pdf",
 note         = "Version 2.4",
)
@inproceedings(SchillerE2012,
 author       = "Todd W. Schiller and Michael D. Ernst",
 year         = "2012",
 title        = "Reducing the barriers to writing verified specifications",
 booktitle    = "Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2012)",
 address      = "Tucson, AZ, USA",
 pages        = "95--112",
 url          = "http://doi.acm.org/10.1145/2384616.2384624",
)
@misc(webSWIG,
 note         = "SWIG: \url {http://www.swig.org}",
)
@misc(CodeSonar,
 note         = "CodeSonar\textregistered ~web site. \url {http://www.grammatech.com/products/codesonar}",
)
@misc(JMLweb,
 note         = "JML web site. \url {http://www.jmlspecs.org}",
)