From fca241c91ba0f27d145bf083a283491844da1da1 Mon Sep 17 00:00:00 2001 From: "Richard L. Ford" Date: Wed, 27 Jan 2016 21:35:30 -0800 Subject: Add Dafny reference manual This version is still a draft, but is mostly complete and about half reviewed. The manual is written using Madoko. The sources are in the Docs/DafnyRef directory. The processed sources are available in the Docs/DafnyRef/out directory in the form of a single HTML page or as a PDF. --- Docs/DafnyRef/references.bib | 1446 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1446 insertions(+) create mode 100644 Docs/DafnyRef/references.bib (limited to 'Docs/DafnyRef/references.bib') 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}, +} -- cgit v1.2.3