@inproceedings(Boogie:Architecture, author = "Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and Bart Jacobs and K. Rustan M. Leino", year = "2006", title = "{B}oogie: A Modular Reusable Verifier for Object-Oriented Programs", editor = "Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem-Paul de Roever", booktitle = "Formal Methods for Components and Objects (FMCO)", series = "LNCS", volume = "4111", publisher = "Springer", pages = "364--387", url = "http://dx.doi.org/10.1007/11804192_17", ) @article(BarnettFaehndrichLeinoMuellerSchulteVenter2011, author = "Mike Barnett and Manuel F{\"a}hndrich and K. Rustan M. Leino and Peter M{\"u}ller and Wolfram Schulte and Herman Venter", year = "2011", title = "Specification and Verification: The {Spec\#} Experience", journal = "Communications of the ACM", volume = "54", number = "6", pages = "81--91", url = "http://dx.doi.org/10.1145/1953122.1953145", ) @inproceedings(Nitpick, author = "Jasmin Christian Blanchette and Tobias Nipkow", year = "2010", title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder", editor = "Matt Kaufmann and Lawrence C. Paulson", booktitle = "Interactive Theorem Proving (ITP)", series = "LNCS", volume = "6172", publisher = "Springer", pages = "131--146", url = "http://dx.doi.org/10.1007/978-3-642-14052-5_11", ) @inproceedings(BobotFilliatreMarcheMelquiondPaskevich2013, author = "Fran\c {c}ois Bobot and Jean-Christophe Filli{\^a}tre and Claude March{\'e} and Guillaume Melquiond and Andrei Paskevich", year = "2013", title = "Preserving User Proofs across Specification Changes", editor = "Ernie Cohen and Andrey Rybalchenko", booktitle = "VSTTE", series = "LNCS", volume = "8164", publisher = "Springer", pages = "191--201", url = "http://dx.doi.org/10.1007/978-3-642-54108-7_10", ) @inproceedings(CohenDahlweidHillebrandLeinenbachMoskalSantenSchulteTobies2009, author = "Ernie Cohen and Markus Dahlweid and Mark A. Hillebrand and Dirk Leinenbach and Micha{\l } 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 (TPHOLs)", series = "LNCS", volume = "5674", publisher = "Springer", pages = "23--42", url = "http://dx.doi.org/10.1007/978-3-642-03359-9_2", ) @article(OpenJML, author = "David R. Cok", year = "2010", title = "Improved usability and performance of {SMT} solvers for debugging specifications", journal = "Software Tools for Technology Transfer (STTT)", volume = "12", number = "6", pages = "467--481", url = "http://dx.doi.org/10.1007/s10009-010-0138-x", ) @inproceedings(OpenJML:F-IDE2014, author = "David R. Cok", year = "2014", title = "{OpenJML}: Software verification for {J}ava 7 using {JML}, {OpenJDK}, and {E}clipse", editor = "Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'e}ry", booktitle = "1st Workshop on Formal-IDE", ) @inproceedings(SPARK2014:toolset, author = "Claire Dross and Pavlos Efstathopoulos and David Lesens and David Mentr{\'e} and Yannick Moy", year = "2014", title = "Rail, Space, Security: Three Case Studies for {SPARK} 2014", booktitle = "7th Europen Congress on Embedded Real Time Software and Systems (ERTS${}^2$ 2014)", url = "http://www.spark-2014.org/uploads/erts_2014.pdf", ) @inproceedings(FilliatrePaskevich2013, author = "Jean-Christophe Filli{\^a}tre and Andrei Paskevich", year = "2013", title = "Why3 --- Where Programs Meet Provers", editor = "Matthias Felleisen and Philippa Gardner", booktitle = "European Symposium on Programming (ESOP)", series = "LNCS", volume = "7792", publisher = "Springer", pages = "125--128", url = "http://dx.doi.org/10.1007/978-3-642-37036-6_8", ) @inproceedings(LeGouesLeinoMoskal7041, author = "Claire Le Goues and K. Rustan M. Leino and Micha{\l } Moskal", year = "2011", title = "The {Boogie} Verification Debugger (Tool Paper)", editor = "Gilles Barthe and Alberto Pardo and Gerardo Schneider", booktitle = "Software Engineering and Formal Methods (SEFM)", series = "LNCS", volume = "7041", publisher = "Springer", pages = "407--414", url = "http://dx.doi.org/10.1007/978-3-642-24690-6_28", ) @inproceedings(GrigoreMoskal:EditAndVerify, author = "Radu Grigore and Micha{\l } Moskal", year = "2007", title = "Edit and Verify", booktitle = "Workshop on First-Order Theorem Proving (FTP)", url = "http://arxiv.org/abs/0708.0713", ) @book(ACL2:book, author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", year = "2000", title = "Computer-Aided Reasoning: An Approach", publisher = "Kluwer Academic Publishers", ) @phdthesis(Klebanov:PhD, author = "Vladimir Klebanov", year = "2009", title = "Extending the Reach and Power of Deductive Program Verification", school = "Department of Computer Science, Universit{\"a}t Koblenz-Landau", url = "http://formal.iti.kit.edu/~klebanov/pubs/thesis-klebanov.pdf", ) @incollection(KoenigLeino:MOD2011, author = "Jason Koenig and K. Rustan M. Leino", year = "2012", title = "Getting Started with {D}afny: A Guide", editor = "Tobias Nipkow and Orna Grumberg and Benedikt Hauptmann", booktitle = "Software Safety and Security: Tools for Analysis and Verification", series = "NATO Science for Peace and Security Series D: Information and Communication Security", volume = "33", publisher = "IOS Press", pages = "152--181", url = "http://dx.doi.org/10.3233/978-1-61499-028-4-152", note = "Summer School Marktoberdorf 2011 lecture notes. A version of this tutorial is available online at \url {http://rise4fun.com/dafny}", ) @incollection(Leino:Dafny:MOD2008, author = "K. Rustan M. Leino", year = "2009", title = "Specification and verification of object-oriented software", editor = "Manfred Broy and Wassiou Sitou and Tony Hoare", booktitle = "Engineering Methods and Tools for Software Safety and Security", series = "NATO Science for Peace and Security Series D: Information and Communication Security", volume = "22", publisher = "IOS Press", pages = "231--266", url = "http://dx.doi.org/10.3233/978-1-58603-976-9-231", note = "Summer School Marktoberdorf 2008 lecture notes", ) @inproceedings(Leino2010, author = "K. Rustan M. Leino", year = "2010", title = "Dafny: An Automatic Program Verifier for Functional Correctness", editor = "Edmund M. Clarke and Andrei Voronkov", booktitle = "Logic for Programming Artificial Intelligence and Reasoning (LPAR)", series = "LNCS", volume = "6355", publisher = "Springer", pages = "348--370", url = "http://dx.doi.org/10.1007/978-3-642-17511-4_20", ) @inproceedings(Leino:induction, author = "K. Rustan M. Leino", year = "2012", title = "Automating Induction with an {SMT} Solver", editor = "Viktor Kuncak and Andrey Rybalchenko", booktitle = "Verification, Model Checking, and Abstract Interpretation (VMCAI)", series = "LNCS", volume = "7148", publisher = "Springer", pages = "315--331", url = "http://dx.doi.org/10.1007/978-3-642-27940-9_21", ) @techreport(LeinoMoskal:Coinduction, author = "K. Rustan M. Leino and Micha{\l } Moskal", year = "2013", title = "Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier", type = "Technical Report", number = "MSR-TR-2013-49", institution = "Microsoft Research", url = "http://research.microsoft.com/pubs/192276/coinduction.pdf", ) @techreport(VC-splitting, author = "K. Rustan M. Leino and Micha{\l } Moskal and Wolfram Schulte", year = "2008", title = "Verification Condition Splitting", type = "Technical Report", institution = "Microsoft Research", url = "http://research.microsoft.com/pubs/77373/VerificationConditionSplitting(Draft2008).pdf", note = "Manuscript KRML 192", ) @inproceedings(LeinoRuemmer:Boogie2, author = "K. Rustan M. Leino and Philipp R{\"u}mmer", year = "2010", title = "A Polymorphic Intermediate Verification Language: Design and Logical Encoding", editor = "Javier Esparza and Rupak Majumdar", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010", series = "LNCS", volume = "6015", publisher = "Springer", pages = "312--327", url = "http://dx.doi.org/10.1007/978-3-642-12002-2_26", ) @inproceedings(deMouraBjorner2008, author = "Leonardo de Moura and Nikolaj Bj{\o }rner", year = "2008", title = "Z3: An Efficient SMT Solver", editor = "C. R. Ramakrishnan and Jakob Rehof", booktitle = "Tools and Algorithms for Construction and Analysis of Systems (TACAS)", series = "LNCS", volume = "4963", publisher = "Springer", pages = "337--340", url = "http://dx.doi.org/10.1007/978-3-540-78800-3_24", ) @inproceedings(DBLP:conf/fsttcs/ReifS93, author = "Wolfgang Reif and Kurt Stenzel", year = "1993", title = "Reuse of Proofs in Software Verification", editor = "R. K. Shyamasundar", booktitle = "Foundations of Software Technology and Theoretical Computer Science", series = "LNCS", volume = "761", publisher = "Springer", pages = "284--293", url = "http://dx.doi.org/10.1007/3-540-57529-4_61", ) @inproceedings(Sternagel2012, author = "Christian Sternagel", year = "2012", title = "Getting Started with {I}sabelle/{jEdit}", booktitle = "Isabelle Users Workshop (IUW)", url = "http://arxiv.org/abs/1208.1368", ) @inproceedings(Wenzel:jEdit, author = "Makarius Wenzel", year = "2010", title = "Asynchronous Proof Processing with {I}sabelle/{S}cala and {I}sabelle/{jEdit}", booktitle = "9th International Workshop On User Interfaces for Theorem Provers (UITP 2010)", series = "Electronic Notes in Theoretical Computer Science", publisher = "Elsevier", url = "http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf", )