diff options
Diffstat (limited to 'Docs/DafnyRef/references.bib')
| -rw-r--r-- | Docs/DafnyRef/references.bib | 1446 |
1 files changed, 1446 insertions, 0 deletions
diff --git a/Docs/DafnyRef/references.bib b/Docs/DafnyRef/references.bib new file mode 100644 index 00000000..880d8446 --- /dev/null +++ b/Docs/DafnyRef/references.bib @@ -0,0 +1,1446 @@ +@InCollection{Leino:Dafny:MOD2008,
+ author = {K. Rustan M. Leino},
+ title = {Specification and verification of object-oriented software},
+ booktitle = {Engineering Methods and Tools for Software Safety and Security},
+ pages = {231-266},
+ publisher = {IOS Press},
+ year = {2009},
+ editor = {Manfred Broy and Wassiou Sitou and Tony Hoare},
+ volume = {22},
+ series = {NATO Science for Peace and Security Series D: Information and Communication Security},
+ note = {Summer School Marktoberdorf 2008 lecture notes},
+}
+
+@InCollection{LeinoSchulte:MOD2006,
+ author = {K. Rustan M. Leino and Wolfram Schulte},
+ title = {A verifying compiler for a multi-threaded object-oriented language},
+ booktitle = {Software Safety and Security},
+ pages = {351-416},
+ publisher = {IOS Press},
+ year = {2007},
+ editor = {Manfred Broy and Johannes Gr{\"u}nbauer and Tony Hoare},
+ volume = {9},
+ series = {NATO Science for Peace and Security Series D: Information and Communication Security},
+ note = {Summer School Marktoberdorf 2006 lecture notes},
+}
+
+@techreport{ESC:rr,
+ author = "David L. Detlefs and K. Rustan M. Leino and Greg Nelson
+ and James B. Saxe",
+ title = "Extended static checking",
+ institution = "Compaq Systems Research Center",
+ month = dec,
+ year = 1998,
+ type = "Research Report",
+ number = 159
+}
+
+@Article{Simplify:tome,
+ author = "David Detlefs and Greg Nelson and James B. Saxe",
+ title = "Simplify: a theorem prover for program checking",
+ journal = JACM,
+ volume = 52,
+ number = 3,
+ month = may,
+ year = 2005,
+ pages = "365-473",
+}
+
+@InProceedings{Doomed:FM2009,
+ author = {Jochen Hoenicke and K. Rustan M. Leino and Andreas
+ Podelski and Martin Sch{\"a}f and Thomas Wies},
+ title = {It's Doomed; We Can Prove It},
+ booktitle = {FM 2009: Formal Methods, Second World Congress},
+ editor = {Ana Cavalcanti and Dennis Dams},
+ volume = 5850,
+ series = lncs,
+ publisher = {Springer},
+ month = nov,
+ year = 2009,
+ pages = {338-353},
+}
+
+@InProceedings{Regis-Gianas:Pottier:MPC2008,
+ author = {Yann R{\'e}gis-Gianas and Fran{\c{c}}ois Pottier},
+ title = {A {Hoare} Logic for Call-by-Value Functional Programs},
+ booktitle = {Mathematics of Program Construction, 9th International Conference},
+ editor = {Philippe Audebaud and Christine Paulin-Mohring},
+ volume = {5133},
+ series = lncs,
+ publisher = {Springer},
+ month = jul,
+ year = {2008},
+ pages = {305-335},
+}
+
+@InProceedings{ZeeKuncakRinard:PLDI2008,
+ author = {Karen Zee and Viktor Kuncak and Martin C. Rinard},
+ title = {Full functional verification of linked data structures},
+ booktitle = {Proceedings of the ACM SIGPLAN 2008 Conference on
+ Programming Language Design and Implementation},
+ editor = {Rajiv Gupta and Saman P. Amarasinghe},
+ year = {2008},
+ month = jun,
+ publisher = {ACM},
+ pages = {349-361},
+}
+
+@InProceedings{VCC:TPHOLs,
+ 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},
+ title = {{VCC}: A Practical System for Verifying Concurrent {C}},
+ booktitle = {Theorem Proving in Higher Order Logics, 22nd
+ International Conference, TPHOLs 2009},
+ editor = {Stefan Berghofer and Tobias Nipkow and Christian
+ Urban and Makarius Wenzel},
+ volume = {5674},
+ series = lncs,
+ publisher = {Springer},
+ year = {2009},
+ month = aug,
+ pages = {23-42},
+}
+
+@InProceedings{seL4:SOSP2009,
+ author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser
+ and June Andronick and David Cock and Philip Derrin
+ and Dhammika Elkaduwe and Kai Engelhardt and Rafal
+ Kolanski and Michael Norrish and Thomas Sewell and
+ Harvey Tuch and Simon Winwood},
+ title = {{seL4}: formal verification of an {OS} kernel},
+ booktitle = {Proceedings of the 22nd ACM Symposium on Operating
+ Systems Principles 2009, SOSP 2009},
+ editor = {Jeanna Neefe Matthews and Thomas E. Anderson},
+ publisher = {ACM},
+ month = oct,
+ year = {2009},
+ pages = {207-220},
+}
+
+@book{Meyer:OOP,
+ author = "Bertrand Meyer",
+ title = "Object-oriented Software Construction",
+ publisher = "Prentice-Hall International",
+ series = "Series in Computer Science",
+ year = 1988
+}
+
+@InProceedings{SpecSharp:Overview,
+ author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
+ title = {The {Spec\#} Programming System: An Overview},
+ booktitle = {{CASSIS 2004}, Construction and Analysis of Safe,
+ Secure and Interoperable Smart devices},
+ editor = "Gilles Barthe and Lilian Burdy and Marieke Huisman and
+ Jean-Louis Lanet and Traian Muntean",
+ series = lncs,
+ volume = 3362,
+ publisher = "Springer",
+ year = 2005,
+ pages = "49-69"
+}
+
+@InProceedings{Kassios:FM2006,
+ author = "Ioannis T. Kassios",
+ title = "Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions",
+ booktitle = "FM 2006: Formal Methods, 14th International Symposium on Formal Methods",
+ editor = "Jayadev Misra and Tobias Nipkow and Emil Sekerinski",
+ series = lncs,
+ volume = 4085,
+ publisher = "Springer",
+ month = aug,
+ year = 2006,
+ pages = "268-283",
+}
+
+@InProceedings{Boogie:Architecture,
+ author = "Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and
+ Bart Jacobs and K. Rustan M. Leino",
+ title = "{B}oogie: A Modular Reusable Verifier for Object-Oriented Programs",
+ booktitle = "Formal Methods for Components and Objects: 4th
+ International Symposium, FMCO 2005",
+ editor = "de Boer, Frank S. and Marcello M. Bonsangue and
+ Susanne Graf and de Roever, Willem-Paul",
+ series = lncs,
+ volume = 4111,
+ publisher = "Springer",
+ month = sep,
+ year = 2006,
+ pages = "364-387"
+}
+
+@Misc{Leino:Boogie2-RefMan,
+ author = {K. Rustan M. Leino},
+ title = {This is {B}oogie 2},
+ howpublished = {Manuscript KRML 178},
+ year = 2008,
+ note = "Available at \url{http://research.microsoft.com/~leino/papers.html}",
+}
+
+@inproceedings{deMouraBjorner:Z3:overview,
+ author = "de Moura, Leonardo and Nikolaj Bj{\o}rner",
+ title = {{Z3}: An efficient {SMT} solver},
+ booktitle = {Tools and Algorithms for the Construction and
+ Analysis of Systems, 14th International Conference,
+ TACAS 2008},
+ editor = {C. R. Ramakrishnan and Jakob Rehof},
+ series = lncs,
+ volume = 4963,
+ publisher = {Springer},
+ month = mar # "--" # apr,
+ year = 2008,
+ pages = {337-340},
+}
+
+@InProceedings{Gonthier:CAV2006,
+ author = {Georges Gonthier},
+ title = {Verifying the safety of a practical concurrent
+ garbage collector},
+ booktitle = {Computer Aided Verification, 8th International Conference, CAV '96},
+ editor = {Rajeev Alur and Thomas A. Henzinger},
+ volume = {1102},
+ series = lncs,
+ publisher = {Springer},
+ month = jul # "--" # aug,
+ year = {1996},
+ pages = {462-465},
+}
+
+@Article{CLIncStack,
+ author = {William R. Bevier and Hunt, Jr., Warren A. and
+ J Strother Moore and William D. Young},
+ title = {Special issue on system verification},
+ journal = {Journal of Automated Reasoning},
+ volume = {5},
+ number = {4},
+ month = dec,
+ year = {1989},
+ pages = {409-530},
+}
+
+@InProceedings{ParkinsonBierman:POPL2005,
+ author = {Matthew J. Parkinson and Gavin M. Bierman},
+ title = {Separation logic and abstraction},
+ booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
+ on Principles of Programming Languages, POPL 2005},
+ publisher = {ACM},
+ month = jan,
+ year = {2005},
+ pages = {247-258},
+}
+
+@InProceedings{Weide:VSTTE2008,
+ author = {Bruce W. Weide and Murali Sitaraman and Heather
+ K. Harton and Bruce Adcock and Paolo Bucci and
+ Derek Bronish and Wayne D. Heym and Jason
+ Kirschenbaum and David Frazier},
+ title = {Incremental Benchmarks for Software Verification Tools and Techniques},
+ booktitle = {Verified Software: Theories, Tools, Experiments,
+ Second International Conference, VSTTE 2008},
+ editor = {Natarajan Shankar and Jim Woodcock},
+ volume = {5295},
+ series = lncs,
+ publisher = {Springer},
+ month = oct,
+ year = {2008},
+ pages = {84-98},
+}
+
+@Article{SchorrWaite:CACM1967,
+ author = {H. Schorr and W. M. Waite},
+ title = {An Efficient Machine-Independent Procedure for
+ Garbage Collection in Various List Structures},
+ journal = cacm,
+ volume = {10},
+ number = {8},
+ month = aug,
+ year = {1967},
+ pages = {501-506},
+}
+
+@phdthesis{Leino:thesis,
+ author = "K. Rustan M. Leino",
+ title = "Toward Reliable Modular Programs",
+ school = {California Institute of Technology},
+ year = 1995,
+ note = "Technical Report Caltech-CS-TR-95-03."
+}
+
+@inproceedings{Boyland:SAS2003,
+ author = {John Boyland},
+ title = {Checking Interference with Fractional Permissions},
+ booktitle = "Static Analysis, 10th International Symposium, SAS 2003",
+ editor = {Radhia Cousot},
+ series = lncs,
+ volume = 2694,
+ publisher = "Springer",
+ year = 2003,
+ pages = {55-72}
+}
+
+@InProceedings{Reynolds:SepLogic,
+ author = {John C. Reynolds},
+ title = {Separation Logic: A Logic for Shared Mutable Data Structures},
+ booktitle = {17th IEEE Symposium on Logic in Computer Science (LICS 2002)},
+ publisher = {IEEE Computer Society},
+ year = {2002},
+ month = jul,
+ pages = {55-74},
+}
+
+@InProceedings{Clarke-Drossopoulou02,
+ author = {Dave Clarke and Sophia Drossopoulou},
+ title = {Ownership, encapsulation and the disjointness of
+ type and effect},
+ booktitle = {Proceedings of the 2002 ACM SIGPLAN Conference on
+ Object-Oriented Programming Systems, Languages and
+ Applications, OOPSLA 2002},
+ publisher = {ACM},
+ Month = nov,
+ Year = 2002,
+ pages = {292--310},
+}
+
+@InProceedings{FAP:OOPSLA1998,
+ author = {Dave Clarke and John Potter and James Noble},
+ title = {Ownership Types for Flexible Alias Protection},
+ booktitle = {Proceedings of the 1998 ACM SIGPLAN Conference on
+ Object-Oriented Programming Systems, Languages \&
+ Applications (OOPSLA '98)},
+ publisher = {ACM},
+ month = oct,
+ year = {1998},
+ pages = {48-64},
+}
+
+@Article{LeinoNelson:tome,
+ author = "K. Rustan M. Leino and Greg Nelson",
+ title = "Data abstraction and information hiding",
+ journal = toplas,
+ month = sep,
+ year = 2002,
+ volume = 24,
+ number = 5,
+ pages = "491-553"
+}
+
+@PhdThesis{Darvas:thesis,
+ author = {{\'A}d{\'a}m P{\'e}ter Darvas},
+ title = {Reasoning About Data Abstraction in Contract Languages},
+ school = {ETH Zurich},
+ year = {2009},
+ note = {Diss. ETH No. 18622},
+}
+
+@InProceedings{SmansEtAl:VeriCool,
+ author = {Jan Smans and Bart Jacobs and Frank Piessens and Wolfram Schulte},
+ title = {Automatic Verifier for {J}ava-Like Programs Based on Dynamic Frames},
+ booktitle = {Fundamental Approaches to Software Engineering, 11th
+ International Conference, FASE 2008},
+ editor = {Jos{\'e} Luiz Fiadeiro and Paola Inverardi},
+ volume = {4961},
+ series = lncs,
+ publisher = {Springer},
+ month = mar # "--" # apr,
+ year = {2008},
+ pages = {261-275},
+}
+
+@inproceedings{Why:Platform,
+ author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
+ title = {The {Why}/{Krakatoa}/{Caduceus} Platform for Deductive Program Verification},
+ booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007},
+ editor = {Werner Damm and Holger Hermanns},
+ volume = {4590},
+ series = lncs,
+ publisher = {Springer},
+ month = jul,
+ year = {2007},
+ pages = {173--177}
+}
+
+@InProceedings{BarrettTinelli:CVC3,
+ author = {Clark Barrett and Cesare Tinelli},
+ title = {{CVC3}},
+ booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007},
+ editor = {Werner Damm and Holger Hermanns},
+ volume = {4590},
+ series = lncs,
+ publisher = {Springer},
+ month = jul,
+ year = {2007},
+ pages = {298-302},
+}
+
+@InProceedings{HubertMarche:SchorrWaite,
+ author = {Thierry Hubert and Claude March{\'e}},
+ title = {A case study of {C} source code verification: the
+ {S}chorr-{W}aite algorithm},
+ booktitle = {Third IEEE International Conference on Software
+ Engineering and Formal Methods (SEFM 2005)},
+ editor = {Bernhard K. Aichernig and Bernhard Beckert},
+ publisher = {IEEE Computer Society },
+ month = sep,
+ year = {2005},
+ pages = {190-199},
+}
+
+@Article{BroyPepper:SchorrWaite,
+ author = {Manfred Broy and Peter Pepper},
+ title = {Combining Algebraic and Algorithmic Reasoning: An
+ Approach to the {S}chorr-{W}aite Algorithm},
+ journal = toplas,
+ volume = {4},
+ number = {3},
+ month = jul,
+ year = {1982},
+ pages = {362-381},
+}
+
+@Article{MehtaNipkow:SchorrWaite,
+ author = {Farhad Mehta and Tobias Nipkow},
+ title = {Proving pointer programs in higher-order logic},
+ journal = {Information and Computation},
+ year = {2005},
+ volume = {199},
+ number = {1--2},
+ pages = {200-227},
+ month = may # "--" # jun,
+}
+
+@InProceedings{Abrial:SchorrWaite,
+ author = {Jean-Raymond Abrial},
+ title = {Event Based Sequential Program Development:
+ Application to Constructing a Pointer Program},
+ booktitle = {FME 2003: Formal Methods, International Symposium of
+ Formal Methods Europe},
+ editor = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
+ volume = {2805},
+ series = lncs,
+ publisher = {Springer},
+ month = sep,
+ year = {2003},
+ pages = {51-74},
+}
+
+@InCollection{Bubel:SchorrWaite,
+ author = {Richard Bubel},
+ title = {The Schorr-Waite-Algorithm},
+ booktitle = {Verification of Object-Oriented Software: The {KeY} Approach},
+ crossref = {KeY:book},
+ chapter = {15},
+}
+
+@InProceedings{BanerjeeEtAl:RegionLogic,
+ author = {Anindya Banerjee and David A. Naumann and Stan Rosenberg},
+ title = {Regional Logic for Local Reasoning about Global Invariants},
+ booktitle = {ECOOP 2008 --- Object-Oriented Programming, 22nd European Conference},
+ editor = {Jan Vitek},
+ series = lncs,
+ volume = 5142,
+ publisher = {Springer},
+ month = jul,
+ year = 2008,
+ pages = {387-411},
+}
+
+@Book{Abrial:BBook,
+ author = "J.-R. Abrial",
+ title = "The {B}-Book: Assigning Programs to Meanings",
+ publisher = "Cambridge University Press",
+ year = 1996
+}
+
+@Book{Abrial:EventB:book,
+ author = {Jean-Raymond Abrial},
+ title = {Modeling in {Event-B}: System and Software Engineering},
+ publisher = {Cambridge University Press},
+ year = {2010},
+}
+
+@Article{MisraCook:Orc,
+ author = {Jayadev Misra and William R. Cook},
+ title = {Computation Orchestration: A Basis for Wide-Area Computing},
+ journal = {Software and Systems Modeling},
+ year = {2007},
+ volume = 6,
+ number = 1,
+ pages = {83-110},
+ month = mar,
+}
+
+@Book{Jackson:Alloy:book,
+ author = {Daniel Jackson},
+ title = {Software Abstractions: Logic, Language, and Analysis},
+ publisher = {MIT Press},
+ year = {2006},
+}
+
+@InProceedings{JacksonEtAl:Formula,
+ author = {Ethan K. Jackson and Dirk Seifert and Markus
+ Dahlweid and Thomas Santen and Nikolaj Bj{\o}rner
+ and Wolfram Schulte},
+ title = {Specifying and Composing Non-functional Requirements
+ in Model-Based Development},
+ booktitle = {Proceedings of the 8th International Conference on
+ Software Composition},
+ pages = {72-89},
+ year = {2009},
+ editor = {Alexandre Bergel and Johan Fabry},
+ series = lncs,
+ volume = {5634},
+ month = jul,
+ publisher = {Springer},
+}
+
+@InProceedings{HarelEtAl:PlayInPlayOut,
+ author = {David Harel and Hillel Kugler and Rami Marelly and
+ Amir Pnueli},
+ title = {Smart {P}lay-out of Behavioral Requirements},
+ booktitle = {Formal Methods in Computer-Aided Design, 4th
+ International Conference, FMCAD 2002},
+ pages = {378-398},
+ year = {2002},
+ editor = {Mark Aagaard and John W. O'Leary},
+ volume = {2517},
+ series = lncs,
+ month = nov,
+ publisher = {Springer},
+}
+
+@Article{Smith:KIDS-overview,
+ author = "Douglas R. Smith",
+ title = "{KIDS}: A Semi-Automatic Program Development System",
+ journal = {IEEE Transactions on Software Engineering },
+ volume = 16,
+ number = 9,
+ month = sep,
+ year = 1990,
+ pages = "1024-1043",
+}
+
+@article{Hoare:DataRepresentations,
+ author = "C. A. R. Hoare",
+ title = "Proof of correctness of data representations",
+ journal = acta,
+ volume = 1,
+ number = 4,
+ year = 1972,
+ pages = "271-281"
+}
+
+@InProceedings{Abrial:FM-in-practice,
+ author = {Jean-Raymond Abrial},
+ title = {Formal methods in industry: achievements, problems, future},
+ booktitle = {28th International Conference on Software Engineering (ICSE 2006)},
+ editor = {Leon J. Osterweil and H. Dieter Rombach and Mary Lou Soffa},
+ month = may,
+ year = {2006},
+ publisher = {ACM},
+ pages = {761-768},
+}
+
+@InProceedings{MartinEtAl:AsynchMIPS,
+ author = {Alain J. Martin and Andrew Lines and Rajit Manohar
+ and Mika Nystr{\"o}m and Paul I. P{\'e}nzes and
+ Robert Southworth and Uri Cummings},
+ title = {The Design of an Asynchronous MIPS R3000 Microprocessor},
+ booktitle = {17th Conference on Advanced Research in VLSI (ARVLSI '97}},
+ month = sep,
+ year = {1997},
+ publisher = {IEEE Computer Society},
+ pages = {164-181},
+}
+
+@InProceedings{BallEtAll:ScalableChecking,
+ author = {Thomas Ball and Brian Hackett and Shuvendu K. Lahiri
+ and Shaz Qadeer and Julien Vanegue},
+ title = {Towards Scalable Modular Checking of User-Defined Properties},
+ booktitle = {Verified Software: Theories, Tools, Experiments,
+ (VSTTE 2010)},
+ editor = {Gary T. Leavens and Peter O'Hearn and Sriram K. Rajamani},
+ volume = {6217},
+ series = lncs,
+ publisher = {Springer},
+ month = aug,
+ year = {2010},
+ pages = {1-24},
+}
+
+@InProceedings{RegisGianasPottier:FunctionalHoare,
+ author = {Yann R{\'e}gis-Gianas and Fran{\,c}ois Pottier},
+ title = {A {H}oare Logic for Call-by-Value Functional Programs},
+ booktitle = {Mathematics of Program Construction, 9th International Conference, MPC 2008},
+ pages = {305-335},
+ year = {2008},
+ editor = {Philippe Audebaud and Christine Paulin-Mohring},
+ volume = {5133},
+ series = lncs,
+ month = jul,
+ publisher = {Springer},
+}
+
+@InProceedings{VeanesEtAl:SpecExplorer,
+ author = {Margus Veanes and Colin Campbell and Wolfgang
+ Grieskamp and Wolfram Schulte and Nikolai Tillmann
+ and Lev Nachmanson},
+ title = {Model-Based Testing of Object-Oriented Reactive
+ Systems with {Spec} {Explorer}},
+ booktitle = {Formal Methods and Testing},
+ pages = {39-76},
+ year = {2008},
+ editor = {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},
+ volume = {4949},
+ series = lncs,
+ publisher = {Springer},
+}
+
+@book{Dijkstra:Discipline,
+ author = "Edsger W. Dijkstra",
+ title = "A Discipline of Programming",
+ publisher = "Prentice Hall",
+ address = "Englewood Cliffs, NJ",
+ year = 1976
+}
+
+@InProceedings{LeinoMueller:ESOP2009,
+ author = {K. Rustan M. Leino and Peter M{\"u}ller},
+ title = {A Basis for Verifying Multi-threaded Programs},
+ booktitle = {Programming Languages and Systems, 18th European
+ Symposium on Programming, ESOP 2009},
+ editor = {Giuseppe Castagna},
+ volume = {5502},
+ series = lncs,
+ publisher = {Springer},
+ month = mar,
+ year = 2009,
+ pages = {378-393},
+}
+
+@InProceedings{LeinoRuemmer:Boogie2,
+ author = {K. Rustan M. Leino and Philipp R{\"u}mmer},
+ title = {A Polymorphic Intermediate Verification Language:
+ Design and Logical Encoding},
+ booktitle = {Tools and Algorithms for the Construction and
+ Analysis of Systems, 16th International Conference,
+ TACAS 2010},
+ editor = {Javier Esparza and Rupak Majumdar},
+ series = lncs,
+ volume = 6015,
+ publisher = {Springer},
+ month = mar,
+ year = 2010,
+ pages = {312-327},
+}
+
+@book{LiskovGuttag:book,
+ author = "Barbara Liskov and John Guttag",
+ title = "Abstraction and Specification in Program Development",
+ publisher = "MIT Press",
+ series = "MIT Electrical Engineering and Computer Science Series",
+ year = 1986
+}
+
+@TechReport{DahlEtAl:Simula67,
+ author = {Ole-Johan Dahl and Bj{\o}rn Myhrhaug and Kristen Nygaard},
+ title = {Common Base Language},
+ institution = {Norwegian Computing Center},
+ type = {Publication},
+ number = {S-22},
+ month = oct,
+ year = 1970,
+}
+
+@inproceedings{LeinoMueller:ModelFields,
+ author = {K. Rustan M. Leino and
+ Peter M{\"u}ller},
+ title = {A Verification Methodology for Model Fields},
+ booktitle = "Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006",
+ editor = "Peter Sestoft",
+ series = lncs,
+ volume = 3924,
+ publisher = "Springer",
+ month = mar,
+ year = 2006,
+ pages = {115-130},
+}
+
+@InProceedings{CarterEtAl:UsingPerfectDeveloper,
+ author = {Gareth Carter and Rosemary Monahan and Joseph M. Morris},
+ title = {Software Refinement with {P}erfect {D}eveloper},
+ booktitle = {Third IEEE International Conference on Software
+ Engineering and Formal Methods (SEFM 2005)},
+ pages = {363-373},
+ editor = {Bernhard K. Aichernig and Bernhard Beckert},
+ month = sep,
+ year = {2005},
+ publisher = {IEEE Computer Society},
+}
+
+@InProceedings{Abrial:SchorrWaite,
+ author = {Jean-Raymond Abrial},
+ title = {Event Based Sequential Program Development:
+ Application to Constructing a Pointer Program},
+ booktitle = {FME 2003: Formal Methods, International Symposium of
+ Formal Methods Europe},
+ editor = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
+ volume = {2805},
+ series = lncs,
+ publisher = {Springer},
+ month = sep,
+ year = {2003},
+ pages = {51-74},
+}
+
+@article{Barnett-etal04,
+ author = {Mike Barnett and Robert DeLine and Manuel F{\"a}hndrich and
+ K. Rustan M. Leino and Wolfram Schulte},
+ title = {Verification of Object-Oriented Programs with Invariants},
+ journal = {Journal of Object Technology},
+ volume = 3,
+ number = 6,
+ year = 2004,
+ pages = {27-56},
+}
+
+@InProceedings{SmansEtAl:ImplicitDynamicFrames,
+ author = {Jan Smans and Bart Jacobs and Frank Piessens},
+ title = {Implicit Dynamic Frames: Combining Dynamic Frames
+ and Separation Logic},
+ booktitle = {ECOOP 2009 --- Object-Oriented Programming, 23rd
+ European Conference},
+ editor = {Sophia Drossopoulou},
+ volume = {5653},
+ series = lncs,
+ publisher = {Springer},
+ month = jul,
+ year = {2009},
+ pages = {148-172},
+}
+
+@inproceedings{GriesPrins:Encapsulation,
+ author = "David Gries and Jan Prins",
+ title = "A New Notion of Encapsulation",
+ booktitle = "Proceedings of the {ACM} {SIGPLAN} 85
+ Symposium on Language Issues in Programming Environments",
+ publisher = "ACM",
+ series = "SIGPLAN Notices 20",
+ number = 7,
+ month = jul,
+ year = 1985,
+ pages = "131-139"
+}
+
+@InProceedings{YangHawblitzel:Verve,
+ author = {Jean Yang and Chris Hawblitzel},
+ title = {Safe to the last instruction: automated verification of a type-safe operating system},
+ booktitle = {Proceedings of the 2010 ACM SIGPLAN Conference on
+ Programming Language Design and Implementation, PLDI
+ 2010},
+ editor = {Benjamin G. Zorn and Alexander Aiken},
+ month = jun,
+ year = {2010},
+ publisher = {ACM},
+ pages = {99-110},
+}
+
+@Book{BoyerMoore:book,
+ author = {Robert S. Boyer and J Strother Moore},
+ title = {A Computational Logic},
+ publisher = {Academic Press},
+ series = {ACM Monograph Series},
+ year = {1979},
+}
+
+@article{HoareWirth:Pascal,
+ author = "C. A. R. Hoare and N. Wirth",
+ title = "An axiomatic definition of the programming language {PASCAL}",
+ journal = acta,
+ volume = 2,
+ number = 4,
+ year = 1973,
+ pages = "335-355"
+}
+
+@article{Hoare:AxiomaticBasis,
+ author = "C. A. R. Hoare",
+ title = "An axiomatic basis for computer programming",
+ journal = cacm,
+ volume = 12,
+ number = 10,
+ year = 1969,
+ month = oct,
+ pages = "576--580,583"
+}
+
+@InProceedings{LeinoMoskal:vacid0-notYetConfirmed,
+ author = {K. Rustan M. Leino and Micha{\l} Moskal},
+ title = {{VACID-0}: {V}erification of {A}mple {C}orrectness
+ of {I}nvariants of {D}ata-structures, Edition 0},
+ booktitle = {VS-Tools & Experiments},
+ year = 2010,
+ editor = {Rajeev Joshi and Tiziana Margaria and Peter
+ M{\"u}ller and David Naumann and Hongseok Yang},
+ series = {VSTTE 2010 Workshop Proceedings},
+ publisher = {ETH Zurich Technical Report 676},
+ month = aug,
+}
+
+@InCollection{Chalice:tutorial,
+ author = {K. Rustan M. Leino and Peter M{\"u}ller and Jan Smans},
+ title = {Verification of Concurrent Programs with {C}halice},
+ booktitle = {Foundations of Security Analysis and Design {V}: {FOSAD} 2007/2008/2009 Tutorial Lectures},
+ editor = {Alessandro Aldini and Gilles Barthe and Roberto Gorrieri},
+ volume = {5705},
+ series = lncs,
+ publisher = {Springer},
+ year = {2009},
+ pages = {195-222}
+}
+
+@inproceedings{LeinoMuellerSmans10,
+ author = {K. Rustan M. Leino and Peter M{\"u}ller and Jan Smans},
+ title = {Deadlock-Free Channels and Locks},
+ booktitle = {Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010},
+ editor = {Andrew D. Gordon},
+ volume = {6012},
+ series = lncs,
+ publisher = {Springer},
+ month = mar,
+ year = {2010},
+ pages = {407-426}
+}
+
+@Book{BundyEtAl:Rippling,
+ author = {Alan Bundy and David Basin and Dieter Hutter and Andrew Ireland},
+ title = {Rippling: Meta-level Guidance for Mathematical Reasoning},
+ publisher = {Cambridge University Press},
+ volume = {56},
+ series = {Cambridge Tracts in Theoretical Computer Science},
+ year = {2005},
+}
+
+@book{Gries:Science,
+ author = "David Gries",
+ title = "The Science of Programming",
+ publisher = "Springer-Verlag",
+ series = "Texts and Monographs in Computer Science",
+ year = 1981
+}
+
+@Book{DijkstraFeijen:Book,
+ author = "Edsger W. Dijkstra and W. H. J. Feijen",
+ title = "A Method of Programming",
+ publisher = "Addison-Wesley",
+ month = jul,
+ year = 1988,
+}
+
+@book{Kaldewaij:Programming,
+ author = "Anne Kaldewaij",
+ title = "Programming: The Derivation of Algorithms",
+ publisher = "Prentice-Hall International",
+ year = 1990,
+ series = "Series in Computer Science",
+}
+
+@InProceedings{LeinoMonahan:VSTTE2010,
+ author = {K. Rustan M. Leino and Rosemary Monahan},
+ title = {Dafny Meets the Verification Benchmarks Challenge},
+ booktitle = {Verified Software: Theories, Tools, Experiments,
+ Third International Conference, VSTTE 2010},
+ pages = {112-126},
+ year = {2010},
+ editor = {Gary T. Leavens and Peter W. O'Hearn and Sriram K. Rajamani},
+ volume = {6217},
+ series = lncs,
+ month = aug,
+ publisher = {Springer},
+}
+
+@InProceedings{VSComp2010:report,
+ author = {Vladimir Klebanov and Peter M{\"u}ller and Natarajan Shankar and
+ Gary T. Leavens and Valentin W{\"u}stholz and Eyad Alkassar and
+ Rob Arthan and Derek Bronish and Rod Chapman and Ernie Cohen and
+ Mark Hillebrand and Bart Jacobs and K. Rustan M. Leino and
+ Rosemary Monahan and Frank Piessens and Nadia Polikarpova and
+ Tom Ridge and Jan Smans and Stephan Tobies and Thomas Tuerk and
+ Mattias Ulbrich and Benjamin Wei{\ss}},
+ title = {The 1st Verified Software Competition: Experience Report},
+ booktitle = {FM 2011: Formal Methods --- 17th International
+ Symposium on Formal Methods},
+ pages = {154-168},
+ year = {2011},
+ editor = {Michael Butler and Wolfram Schulte},
+ volume = {6664},
+ series = lncs,
+ month = jun,
+ publisher = {Springer},
+}
+
+@InProceedings{Leino:Dafny:LPAR16,
+ author = {K. Rustan M. Leino},
+ title = {Dafny: An Automatic Program Verifier for Functional Correctness},
+ booktitle = {LPAR-16},
+ year = {2010},
+ volume = {6355},
+ series = lncs,
+ publisher = {Springer},
+ month = apr,
+ editor = {Edmund M. Clarke and Andrei Voronkov},
+ pages = {348-370},
+}
+
+@book{BackVonWright:Book,
+ author = "Ralph-Johan Back and von Wright, Joakim",
+ title = "Refinement Calculus: A Systematic Introduction",
+ series = "Graduate Texts in Computer Science",
+ publisher = "Springer-Verlag",
+ year = 1998
+}
+
+@Article{BalzerCheathamGreen:1990s,
+ author = {Robert Balzer and {Cheatham, Jr.}, Thomas E. and Cordell Green},
+ title = {Software Technology in the 1990's: Using a New Paradigm},
+ journal = {IEEE Computer},
+ year = {1983},
+ volume = {16},
+ number = {11},
+ pages = {39-45 },
+ month = nov,
+}
+
+@InProceedings{Zloof:QBE,
+ author = {Mosh{\'e} M. Zloof},
+ title = {Query by Example},
+ booktitle = {American Federation of Information Processing
+ Societies: 1975 National Computer Conference},
+ pages = {431-438},
+ year = {1975},
+ month = may,
+ publisher = {AFIPS Press },
+}
+
+@InProceedings{HarrisGulwani:PLDI2011,
+ author = {William R. Harris and Sumit Gulwani},
+ title = {Spreadsheet table transformations from examples},
+ booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on
+ Programming Language Design and Implementation, PLDI
+ 2011},
+ pages = {317-328},
+ year = {2011},
+ editor = {Mary W. Hall and David A. Padua},
+ month = jun,
+ publisher = {ACM},
+}
+
+@Article{Smith:KIDS-overview,
+ author = "Douglas R. Smith",
+ title = "{KIDS}: A Semi-Automatic Program Development System",
+ journal = {IEEE Transactions on Software Engineering },
+ volume = 16,
+ number = 9,
+ month = sep,
+ year = 1990,
+ pages = "1024-1043",
+}
+
+@Article{RodinToolset,
+ author = {Jean-Raymond Abrial and Michael Butler and Stefan
+ Hallerstede and Thai Son Hoang and Farhad Mehta and
+ Laurent Voisin},
+ title = {Rodin: An Open Toolset for Modelling and Reasoning in {Event-B}},
+ journal = {International Journal on Software Tools for Technology Transfer},
+ year = {2010},
+ month = apr,
+}
+
+@Article{Summers:LISP-from-examples,
+ author = {Phillip D. Summers},
+ title = {A Methodology for {LISP} Program Construction from Examples},
+ journal = jacm,
+ year = {1977},
+ volume = {24},
+ number = {1},
+ pages = {161-175},
+ month = jan,
+}
+
+@InProceedings{Pex:overview,
+ author = {Nikolai Tillmann and de Halleux, Jonathan},
+ title = {Pex---White Box Test Generation for {.NET}},
+ booktitle = {Tests and Proofs, Second International Conference, TAP 2008},
+ pages = {134-153},
+ year = {2008},
+ editor = {Bernhard Beckert and Reiner H{\"a}hnle},
+ series = lncs,
+ volume = {4966},
+ month = apr,
+ publisher = {Springer},
+}
+
+@InProceedings{GodefroidKlarlundSen:DART,
+ author = {Patrice Godefroid and Nils Klarlund and Koushik Sen},
+ title = {{DART}: directed automated random testing},
+ booktitle = {Proceedings of the ACM SIGPLAN 2005 Conference on
+ Programming Language Design and Implementation},
+ pages = {213-223},
+ year = {2005},
+ editor = {Vivek Sarkar and Mary W. Hall},
+ month = jun,
+ publisher = {ACM},
+}
+
+@PhdThesis{Monahan:thesis,
+ author = {Rosemary Monahan},
+ title = {Data Refinement in Object-Oriented Verification},
+ school = {Dublin City University},
+ year = {2010},
+}
+
+@InProceedings{Denali:pldi2002,
+ author = {Rajeev Joshi and Greg Nelson and Keith H. Randall},
+ title = {Denali: A Goal-directed Superoptimizer},
+ booktitle = {Proceedings of the 2002 ACM SIGPLAN Conference on
+ Programming Language Design and Implementation
+ (PLDI)},
+ pages = {304-314},
+ year = {2002},
+ month = jun,
+ publisher = {ACM},
+}
+@Book{SETL,
+ author = {J. T. Schwartz and R. B. K. Dewar and E. Dubinsky and E. Schonberg},
+ title = {Programming with Sets: An Introduction to {SETL}},
+ series = {Texts and Monographs in Computer Science},
+ publisher = {Springer},
+ year = {1986},
+}
+
+@InProceedings{KuncakEtAl:PLDI2010,
+ author = {Viktor Kuncak and Mika{\"e}l Mayer and Ruzica Piskac
+ and Philippe Suter},
+ title = {Complete functional synthesis},
+ booktitle = {Proceedings of the 2010 ACM SIGPLAN Conference on
+ Programming Language Design and Implementation, PLDI
+ 2010},
+ pages = {316-329},
+ year = {2010},
+ editor = {Benjamin G. Zorn and Alexander Aiken},
+ month = jun,
+ publisher = {ACM},
+}
+
+@Article{JML:ToolSuite:STTT,
+ author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and
+ Michael D. Ernst and Joeseph R. Kiniry and Gary T. Leavens and
+ K. Rustan M. Leino and Erik Poll},
+ title = {An overview of {JML} tools and applications},
+ journal = {International Journal on Software Tools
+ for Technology Transfer},
+ volume = 7,
+ number = 3,
+ publisher = {Springer},
+ month = jun,
+ year = 2005,
+ pages = {212-232},
+}
+
+@InProceedings{Green:ProblemSolving,
+ author = {Cordell Green},
+ title = {Application of Theorem Proving to Problem Solving},
+ booktitle = {Proceedings of the 1st International Joint Conference on Artificial Intelligence},
+ editor = {Donald E. Walker and Lewis M. Norton},
+ pages = {219-240},
+ year = {1969},
+ month = may,
+ publisher = {William Kaufmann},
+}
+
+@Article{MannaWaldinger:CACM1971,
+ author = {Zohar Manna and Richard J. Waldinger},
+ title = {Towards automatic program synthesis},
+ journal = cacm,
+ year = {1971},
+ volume = {14},
+ number = {3},
+ pages = {151-165},
+ month = mar,
+}
+
+@Article{RichWaters:ProgAppren,
+ author = {Charles Rich and Richard C. Waters},
+ title = {The {P}rogrammer's {A}pprentice: A Research Overview},
+ journal = {IEEE Computer},
+ year = {1988},
+ volume = {21},
+ number = {11},
+ pages = {10-25},
+ month = nov,
+}
+
+@InProceedings{Green:PSI,
+ author = {Cordell Green},
+ title = {The Design of the {PSI} Program Synthesis System},
+ booktitle = {Proceedings of the 2nd International Conference on Software Engineering},
+ pages = {4-18},
+ year = {1976},
+ month = oct,
+ publisher = {IEEE Computer Society},
+}
+
+@Article{SpecSharp:Retrospective:CACM,
+ author = {Mike Barnett and Manuel F{\"a}hndrich and
+ K. Rustan M. Leino and Peter M{\"u}ller and
+ Wolfram Schulte and Herman Venter},
+ title = {Specification and Verification: The {Spec\#} Experience},
+ journal = cacm,
+ volume = {54},
+ number = {6},
+ pages = {81-91},
+ month = jun,
+ year = 2011,
+}
+
+@article{Filipovic:SepLogicRefinement,
+ author = {Ivana Filipovi{\'c} and Peter O'Hearn and
+ Noah Torp-Smith and Hongseok Yang},
+ title = {Blaming the client: on data refinement in the presence of pointers},
+ journal = {Formal Aspects of Computing},
+ volume = {22},
+ number = {5},
+ month = sep,
+ year = {2010},
+ pages = {547-583},
+}
+
+@inproceedings{Grandy:JavaRefinement,
+ author = {Grandy, Holger and Stenzel, Kurt and Reif, Wolfgang},
+ title = {A refinement method for {J}ava programs},
+ booktitle = {Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007},
+ editor = {Marcello M. Bonsangue and Einar Broch Johnsen},
+ series = lncs,
+ number = {4468},
+ month = jun,
+ year = {2007},
+ publisher = {Springer},
+ pages = {221--235},
+}
+
+@InCollection{KoenigLeino:MOD2011,
+ author = {Jason Koenig and K. Rustan M. Leino},
+ title = {Getting Started with {D}afny: A Guide},
+ booktitle = {Software Safety and Security: Tools for Analysis and Verification},
+ pages = {152-181},
+ publisher = {IOS Press},
+ year = {2012},
+ editor = {Tobias Nipkow and Orna Grumberg and Benedikt Hauptmann},
+ volume = {33},
+ series = {NATO Science for Peace and Security Series D: Information and Communication Security},
+ note = {Summer School Marktoberdorf 2011 lecture notes},
+}
+
+@InProceedings{VonWright:ExtendingWindowInference,
+ author = {von Wright, Joakim},
+ title = {Extending Window Inference},
+ booktitle = {Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98},
+ pages = {17-32},
+ year = {1998},
+ editor = {Jim Grundy and Malcolm C. Newey},
+ volume = {1479},
+ series = lncs,
+ publisher = {Springer},
+}
+
+@InProceedings{BauerWenzel:IsarExperience,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Calculational reasoning revisited: an {I}sabelle/{I}sar experience},
+ booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001},
+ pages = {75-90},
+ year = {2001},
+ editor = {Richard J. Boulton and Paul B. Jackson},
+ volume = {2152},
+ series = lncs,
+ month = sep,
+ publisher = {Springer},
+}
+
+@InProceedings{Leino:induction,
+ author = {K. Rustan M. Leino},
+ title = {Automating Induction with an {SMT} Solver},
+ booktitle = {Verification, Model Checking, and Abstract Interpretation --- 13th International Conference, VMCAI 2012},
+ pages = {315-331},
+ year = {2012},
+ editor = {Viktor Kuncak and Andrey Rybalchenko},
+ volume = {7148},
+ series = lncs,
+ month = jan,
+ publisher = {Springer},
+}
+
+@InProceedings{LGLM:BVD,
+ author = {Le Goues, Claire and K. Rustan M. Leino and Micha{\l} Moskal},
+ title = {The {B}oogie {V}erification {D}ebugger (Tool Paper)},
+ booktitle = {Software Engineering and Formal Methods --- 9th International Conference, SEFM 2011},
+ pages = {407-414},
+ year = {2011},
+ editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
+ volume = {7041},
+ series = lncs,
+ month = nov,
+ publisher = {Springer},
+}
+
+@InProceedings{Filliatre:2lines,
+ author = {Jean-Christophe Filli{\^a}tre},
+ title = {Verifying two lines of {C} with {Why3}: an exercise in
+ program verification},
+ booktitle = {Verified Software: Theories, Tools, Experiments ---
+ 4th International Conference, VSTTE 2012},
+ pages = {83-97},
+ year = {2012},
+ editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
+ volume = {7152},
+ series = lncs,
+ month = jan,
+ publisher = {Springer},
+}
+
+@InCollection{LeinoMoskal:UsableProgramVerification,
+ author = {K. Rustan M. Leino and Micha{\l} Moskal},
+ title = {Usable Auto-Active Verification},
+ booktitle = {UV10 (Usable Verification) workshop},
+ year = {2010},
+ editor = {Tom Ball and Lenore Zuck and N. Shankar},
+ month = nov,
+ publisher = {\url{http://fm.csl.sri.com/UV10/}},
+}
+
+@InProceedings{LeinoMonahan:Comprehensions,
+ author = {K. Rustan M. Leino and Rosemary Monahan},
+ title = {Reasoning about Comprehensions with First-Order {SMT} Solvers},
+ booktitle = {Proceedings of the 2009 ACM Symposium on Applied Computing (SAC)},
+ editor = {Sung Y. Shin and Sascha Ossowski},
+ publisher = {ACM},
+ month = mar,
+ year = 2009,
+ pages = {615-622},
+}
+
+@TechReport{VeriFast:TR,
+ author = {Bart Jacobs and Frank Piessens},
+ title = {The {VeriFast} program verifier},
+ institution = {Department of Computer Science, Katholieke Universiteit Leuven},
+ year = {2008},
+ number = {CW-520},
+ month = aug,
+}
+
+@book{DijkstraScholten:book,
+ author = "Edsger W. Dijkstra and Carel S. Scholten",
+ title = "Predicate Calculus and Program Semantics",
+ publisher = "Springer-Verlag",
+ series = "Texts and Monographs in Computer Science",
+ year = 1990
+}
+
+@Book{KeY:book,
+ author = {Bernhard Beckert and Reiner H{\"a}hnle and Peter H. Schmitt},
+ title = {Verification of Object-Oriented Software: The {KeY} Approach},
+ volume = 4334,
+ series = lnai,
+ publisher = {Springer},
+ year = 2007,
+}
+
+@Book{Coq:book,
+ author = {Yves Bertot and Pierre Cast{\'e}ran},
+ title = {Interactive Theorem Proving and Program Development --- {C}oq'{A}rt: The Calculus of Inductive Constructions},
+ publisher = {Springer},
+ year = {2004},
+ series = {Texts in Theoretical Computer Science},
+}
+
+@Book{ACL2:book,
+ author = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore},
+ title = {Computer-Aided Reasoning: An Approach},
+ publisher = {Kluwer Academic Publishers},
+ year = {2000},
+}
+
+@InProceedings{Coq:Coinduction,
+ author = {Eduardo Gim{\'e}nez},
+ title = {An Application of Co-inductive Types in {Coq}: Verification of the Alternating Bit Protocol},
+ booktitle = {Types for Proofs and Programs, International Workshop TYPES'95},
+ pages = {135-152},
+ year = {1996},
+ editor = {Stefano Berardi and Mario Coppo},
+ volume = 1158,
+ series = lncs,
+ publisher = {Springer},
+}
+
+@InCollection{JacobsRutten:IntroductionCoalgebra,
+ author = {Bart Jacobs and Jan Rutten},
+ title = {An Introduction to (Co)Algebra and (Co)Induction},
+ booktitle = {Advanced Topics in Bisimulation and Coinduction},
+ editor = {Davide Sangiorgi and Jan Rutten},
+ series = {Cambridge Tracts in Theoretical Computer Science},
+ number = {52},
+ publisher = {Cambridge University Press},
+ month = oct,
+ year = {2011},
+ pages = {38-99},
+}
+
+@InProceedings{SonnexEtAl:Zeno,
+ author = {William Sonnex and Sophia Drossopoulou and Susan Eisenbach},
+ title = {Zeno: An Automated Prover for Properties of Recursive
+ Data Structures},
+ booktitle = {Tools and Algorithms for the Construction and Analysis of
+ Systems --- 18th International Conference, TACAS 2012},
+ editor = {Cormac Flanagan and Barbara K{\"o}nig},
+ volume = {7214},
+ series = lncs,
+ year = {2012},
+ month = mar # "--" # apr,
+ publisher = {Springer},
+ pages = {407-421},
+}
+
+@InProceedings{JohanssonEtAl:IPT2010,
+ author = {Moa Johansson and Lucas Dixon and Alan Bundy},
+ title = {Case-Analysis for {R}ippling and Inductive Proof},
+ booktitle = {Interactive Theorem Proving, First International Conference, ITP 2010},
+ editor = {Matt Kaufmann and Lawrence C. Paulson},
+ volume = {6172},
+ series = lncs,
+ publisher = {Springer},
+ month = jul,
+ year = {2010},
+ pages = {291-306},
+}
+
+@Article{HatcliffEtAl:BISL,
+ author = {John Hatcliff and Gary T. Leavens and
+ K. Rustan M. Leino and Peter M{\"u}ller and Matthew Parkinson},
+ title = {Behavioral interface specification languages},
+ journal = {ACM Computing Surveys},
+ volume = {44},
+ number = {3},
+ note = {Article 16},
+ month = jun,
+ year = {2012},
+}
+
+@InProceedings{BoehmeNipkow:Sledgehammer,
+ author = {Sascha B{\"o}hme and Tobias Nipkow},
+ title = {Sledgehammer: {J}udgement {D}ay},
+ booktitle = {Automated Reasoning, 5th International Joint Conference, IJCAR 2010},
+ editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
+ year = {2010},
+ pages = {107-121},
+ volume = {6173},
+ series = lncs,
+ month = jul,
+ publisher = {Springer},
+}
+
+@InProceedings{Dafny:LASER2011,
+ author = {Luke Herbert and K. Rustan M. Leino and Jose Quaresma},
+ title = {Using {Dafny}, an Automatic Program Verifier},
+ booktitle = {Tools for Practical Software Verification, {LASER}, International Summer School 2011},
+ editor = {Bertrand Meyer and Martin Nordio},
+ volume = {7682},
+ series = lncs,
+ year = {2012},
+ pages = {156-181},
+ publisher = {Springer},
+}
+
+@Article{Leroy:CompCert:CACM,
+ author = {Xavier Leroy},
+ title = {Formal verification of a realistic compiler},
+ journal = cacm,
+ volume = {52},
+ number = {7},
+ year = {2009},
+ pages = {107-115},
+}
+
+@InProceedings{Leino:ITP2013,
+ author = {K. Rustan M. Leino},
+ title = {Automating Theorem Proving with {SMT}},
+ booktitle = {Interactive Theorem Proving --- 4th International Conference, ITP 2013},
+ year = {2013},
+ editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
+ volume = {7998},
+ series = lncs,
+ pages = {2-16},
+ month = jul,
+ publisher = {Springer},
+}
+
+@techreport{Nelson:thesis,
+ author = "Charles Gregory Nelson",
+ title = "Techniques for Program Verification",
+ institution = "Xerox PARC",
+ month = jun,
+ year = 1981,
+ number = "CSL-81-10",
+ note = "The author's PhD thesis"
+}
+
+@InProceedings{LernerMillsteinChambers:VerifiedOptimizations,
+ author = {Sorin Lerner and Todd Millstein and Craig Chambers},
+ title = {Automatically proving the correctness of compiler optimizations},
+ booktitle = {Proceedings of the ACM SIGPLAN 2003 Conference on
+ Programming Language Design and Implementation 2003},
+ year = {2003},
+ editor = {Ron Cytron and Rajiv Gupta},
+ pages = {220-231},
+ month = jun,
+ publisher = {ACM},
+}
+
+@InProceedings{BoyerHunt:ACL2,
+ author = {Robert S. Boyer and Hunt, Jr., Warren A.},
+ title = {Function Memoization and Unique Object Representation for {ACL2} Functions},
+ booktitle = {Proceedings of the Sixth International Workshop on
+ the ACL2 Theorem Prover and its Applications, ACL2 2006},
+ editor = {Panagiotis Manolios and Matthew Wilding},
+ month = aug,
+ year = {2006},
+ pages = {81--89},
+ publisher = {ACM},
+}
+
+@inproceedings{LeinoWuestholz:DafnyIDE,
+ author = {K. Rustan M. Leino and
+ Valentin W{\"{u}}stholz},
+ title = {The {D}afny Integrated Development Environment},
+ booktitle = {Proceedings 1st Workshop on Formal Integrated Development Environment,
+ {F-IDE} 2014},
+ month = apr,
+ year = {2014},
+ pages = {3--15},
+ editor = {Catherine Dubois and
+ Dimitra Giannakopoulou and
+ Dominique M{\'{e}}ry},
+ series = {{EPTCS}},
+ volume = {149},
+}
+
+@inproceedings{BarnettLeino:Weakest,
+ author = {Mike Barnett and K. Rustan M. Leino},
+ title = {Weakest-precondition of unstructured programs},
+ booktitle = {Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on
+ Program Analysis For Software Tools and Engineering,
+ PASTE'05},
+ editor = {Michael D. Ernst and Thomas P. Jensen},
+ month = sep,
+ year = {2005},
+ pages = {82-87},
+ publisher = {ACM},
+}
|