@inproceedings(Barnett-Leino05-short,
 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",
)
@inproceedings(Barnett-Leino-Schulte04-short,
 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 (CASSIS 2004)",
 series       = "Lecture Notes in Computer Science",
 volume       = "3362",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/978-3-540-30569-9\_3",
)
@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 4334",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/978-3-540-69061-0",
)
@inproceedings(Blanc:2013:OLV:2489837.2489838-short,
 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",
 doi          = "10.1145/2489837.2489838",
)
@inproceedings(BML2007-short,
 author       = "Lilian Burdy and Marieke Huisman and Mariela Pavlova",
 year         = "2007",
 title        = "Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode",
 booktitle    = "Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering",
 series       = "FASE'07",
 doi          = "10.1007/978-3-540-71289-3\_18",
)
@article(chalin2004jml,
 author       = "Patrice Chalin",
 year         = "2004",
 title        = "JML support for primitive arbitrary precision numeric types: Definition and semantics",
 journal      = "Journal of Object Technology",
 volume       = "3",
 number       = "6",
 pages        = "57--79",
 doi          = "10.5381/jot.2004.3.6.a3",
)
@article(chalin2005reassessing,
 author       = "Patrice Chalin",
 year         = "2005",
 title        = "Reassessing JML's logical foundation",
 journal      = "Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP05), Glasgow, Scotland",
)
@incollection(chalin2007non,
 author       = "Patrice Chalin and Perry R James",
 year         = "2007",
 title        = "Non-null references by default in Java: Alleviating the nullity annotation burden",
 booktitle    = "ECOOP 2007",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-73589-2\_12",
)
@article(ChalinJR08,
 author       = "Patrice Chalin and Perry R. James and Frédéric Rioux",
 year         = "2008",
 title        = "Reducing the use of nullable types through non-null by default and monotonic non-null.",
 journal      = "IET Software",
 volume       = "2",
 number       = "6",
 pages        = "515--531",
 doi          = "10.1049/iet-sen:20080010",
)
@incollection(BML-2009,
 author       = "Jacek Chrzaszcz and Marieke Huisman and Aleksy Schubert",
 year         = "2009",
 title        = "BML and Related Tools",
 editor       = "FrankS. Boer and MarcelloM. Bonsangue and Eric Madelaine",
 booktitle    = "Formal Methods for Components and Objects",
 series       = "Lecture Notes in Computer Science",
 volume       = "5751",
 publisher    = "Springer",
 pages        = "278--297",
 doi          = "10.1007/978-3-642-04167-9\_14",
)
@article(Cok-2010-ImprovedUsability,
 author       = "David Cok",
 year         = "2010",
 title        = "Improved usability and performance of SMT solvers for debugging specifications",
 journal      = "International Journal on Software Tools for Technology Transfer (STTT)",
 volume       = "12",
 doi          = "10.1007/s10009-010-0138-x",
)
@inproceedings(Cok04,
 author       = "David R. Cok",
 year         = "2004",
 title        = "Reasoning with specifications containing method calls in {JML} and first-order provers",
 editor       = "Erik Poll",
 booktitle    = "ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs",
 pages        = "41--48",
)
@article(Cok-2008-SAVCBS,
 author       = "David R. Cok",
 year         = "2008",
 title        = "Adapting {JML} to generic types and {Java} 1.6",
 journal      = "SAVCBS'08",
)
@incollection(Cok-2011-jSMTLIB-short,
 author       = "David R. Cok",
 year         = "2011",
 title        = "{jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2}",
 editor       = "Mihaela Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi",
 booktitle    = "NASA Formal Methods",
 series       = "Lecture Notes in Computer Science",
 volume       = "6617",
 publisher    = "Springer Berlin Heidelberg",
 doi          = "10.1007/978-3-642-20398-5\_36",
)
@article(Cok-2014-SPEEDY,
 author       = "David R. Cok and Scott C. Johnson",
 year         = "2014",
 title        = "SPEEDY: An Eclipse-based IDE for invariant inference",
 journal      = "{Electronic Proceedings in Theoretical Computer Science (EPTCS)}",
 note         = "To appear.",
)
@inproceedings(Kiniry-Cok05-short,
 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",
 series       = "LNCS",
 volume       = "3362",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/b105030",
)
@misc(webcvc4,
 note         = "CVC4: \url {http://cvc4.cs.nyu.edu}",
)
@article(DarvasM06,
 author       = "{\'A}d{\'a}m Darvas and Peter M{\"u}ller",
 year         = "2006",
 title        = "Reasoning About Method Calls in Interface Specifications",
 journal      = "Journal of Object Technology",
 volume       = "5",
 number       = "5",
 pages        = "59--85",
 doi          = "10.5381/jot.2006.5.5.a3",
)
@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",
)
@inproceedings(DietlDM07,
 author       = "Werner Dietl and Sophia Drossopoulou and Peter M{\"u}ller",
 year         = "2007",
 title        = "Generic Universe Types",
 editor       = "Erik Ernst",
 booktitle    = "ECOOP",
 series       = "Lecture Notes in Computer Science",
 volume       = "4609",
 publisher    = "Springer",
 pages        = "28--53",
 doi          = "10.1007/978-3-540-73589-2\_3",
)
@misc(JSR308-webpage-201110,
 author       = "Michael D. Ernst",
 year         = "2011",
 title        = "{Type Annotations} specification ({JSR} 308)",
 howpublished = "\url {http://types.cs.washington.edu/jsr308/}",
)
@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",
)
@inproceedings(ESCJava2002,
 author       = "Cormac Flanagan and K. Rustan M. Leino and Mark Lillibridge and Greg Nelson and James B. Saxe and Raymie Stata",
 year         = "2002",
 title        = "Extended Static Checking for Java",
 booktitle    = "Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation",
 series       = "PLDI '02",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "234--245",
 doi          = "10.1145/512529.512558",
)
@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/}",
)
@inproceedings(LGLM:BVD,
 author       = "Claire Le Goues and K. Rustan M. Leino and Micha{\l } Moskal",
 year         = "2011",
 title        = "The {B}oogie {V}erification {D}ebugger (Tool Paper)",
 editor       = "Gilles Barthe and Alberto Pardo and Gerardo Schneider",
 booktitle    = "Software Engineering and Formal Methods --- 9th International Conference, SEFM 2011",
 series       = "Lecture Notes in Computer Science",
 volume       = "7041",
 publisher    = "Springer",
 pages        = "407--414",
 doi          = "10.1007/978-3-642-24690-6\_28",
)
@incollection(Leavens-Baker-Ruby99b,
 author       = "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
 year         = "1999",
 title        = "{JML}: A Notation for Detailed Design",
 editor       = "Haim Kilov and Bernhard Rumpe and Ian Simmonds",
 booktitle    = "Behavioral Specifications of Businesses and Systems",
 publisher    = "Kluwer Academic Publishers",
 address      = "Boston",
 pages        = "175--188",
 doi          = "10.1007/978-1-4615-5229-1\_12",
)
@unpublished(Leavens-Cok-05,
 author       = "Gary T. Leavens and David R. Cok",
 year         = "2005",
 title        = "Adapting Observational Purity to {JML}",
 note         = "Presented at IFIP WG 2.3",
)
@techreport(Leavens-Mueller06,
 author       = "Gary T. Leavens and Peter M{\"u}ller",
 year         = "2006",
 title        = "Information Hiding and Visibility in Interface Specifications",
 type         = "Technical Report",
 number       = "06-28",
 institution  = "Department of Computer Science, Iowa State University",
 address      = "Ames, Iowa",
 url          = "ftp://ftp.cs.iastate.edu/pub/techreports/TR06-28/TR.pdf",
 note         = "In ICSE 2007, pages 385-395.",
)
@unpublished(Leavens-etal08,
 author       = "Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David R. Cok and Peter M\"{u}ller and Joseph Kiniry and Patrice Chalin and Daniel M. Zimmerman",
 year         = "2008",
 title        = "{JML Reference Manual}",
 note         = "Available from \url {http://www.jmlspecs.org}",
)
@inproceedings(Leino:1998:DGS:286936.286953-short,
 author       = "K. Rustan M. Leino",
 year         = "1998",
 title        = "Data Groups: Specifying the Modification of Extended State",
 booktitle    = "Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications",
 series       = "OOPSLA '98",
 publisher    = "ACM",
 doi          = "10.1145/286942.286953",
)
@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-short,
 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",
 doi          = "10.1007/978-3-642-17511-4\_20",
)
@inproceedings(Leino-Mueller06,
 author       = "K. Rustan M. Leino and Peter M\"uller",
 year         = "2006",
 title        = "A verification methodology for model fields",
 editor       = "Peter Sestoft",
 booktitle    = "European Symposium on Programming (ESOP)",
 series       = "Lecture Notes in Computer Science",
 volume       = "3924",
 publisher    = "Springer-Verlag",
 pages        = "115--130",
 doi          = "10.1007/11693024\_9",
)
@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.",
)
@book(Meyer88,
 author       = "Bertrand Meyer",
 year         = "1988",
 title        = "Object-oriented Software Construction",
 publisher    = "Prentice Hall",
 address      = "New York, NY",
)
@misc(webmobius,
 note         = "Mobius. \url {http://software.imdea.org/~gbarthe/mobius/bin/view/Mobius/WebHome.html}",
)
@inproceedings(DBLP:conf/issta/PapiACPE08,
 author       = "Matthew M. Papi and Mahmood Ali and Telmo Luis Correa Jr. and Jeff H. Perkins and Michael D. Ernst",
 year         = "2008",
 title        = "{Practical pluggable types for Java}",
 booktitle    = "ISSTA",
 pages        = "201--212",
 doi          = "10.1145/1390630.1390656",
)
@inproceedings(ShanerLN07,
 author       = "Steve M. Shaner and Gary T. Leavens and David A. Naumann",
 year         = "2007",
 title        = "Modular verification of higher-order methods with mandatory calls specified by model programs",
 booktitle    = "OOPSLA",
 doi          = "10.1145/1297027.1297053",
)
@incollection(Zimmerman2010,
 author       = "Daniel M. Zimmerman and Rinkesh Nagmoti",
 year         = "2011",
 title        = "JMLUnit: The Next Generation",
 editor       = "Bernhard Beckert and Claude March\'e",
 booktitle    = "Formal Verification of Object-Oriented Software",
 series       = "Lecture Notes in Computer Science",
 volume       = "6528",
 publisher    = "Springer",
 pages        = "183--197",
 doi          = "10.1007/978-3-642-18070-5\_13",
)
@misc(ACSLweb,
 note         = "ACSL web site. \url {http://www.frama-c.cea.fr/acsl.html}",
)
@misc(JMLweb,
 note         = "JML web site. \url {http://www.jmlspecs.org}",
)
@misc(OPENJDKweb,
 note         = "OpenJDK web site. \url {http://openjdk.java.net}",
)