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/krml250.bib | 2026 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2026 insertions(+) create mode 100644 Docs/DafnyRef/krml250.bib (limited to 'Docs/DafnyRef/krml250.bib') diff --git a/Docs/DafnyRef/krml250.bib b/Docs/DafnyRef/krml250.bib new file mode 100644 index 00000000..f30547f7 --- /dev/null +++ b/Docs/DafnyRef/krml250.bib @@ -0,0 +1,2026 @@ +@string{lncs = "LNCS"} + +@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}, +} + +@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{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}, + 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 Joseph 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 = {VMCAI 2012}, + pages = {315-331}, + year = {2012}, + 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 = {Dept. of Computer Science, Katholieke Universiteit Leuven}, + year = {2008}, + number = {CW-520}, +} + +@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{Coq:book, + author = {Yves Bertot and Pierre Cast{\'e}ran}, + title = {{C}oq'{A}rt: The Calculus of Inductive Constructions}, + publisher = {Springer}, + year = {2004}, + series = {Texts in Theoretical Comp. Sci.}, +} + +@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}, + series = {Cambridge Tracts in Theoretical Comp. Sci.}, + number = {52}, + publisher = {Cambridge Univ. Press}, + 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 = {ITP 2013}, + year = {2013}, + 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}, +} + +@InProceedings{AutoProof:TACAS2015, + author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova}, + title = {{AutoProof}: Auto-Active Functional Verification of Object-Oriented Programs}, + booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems --- 21st International Conference, + TACAS 2015}, + OPTyear = {2015}, + editor = {Christel Baier and Cesare Tinelli}, + volume = {9035}, + series = lncs, + pages = {566-580}, + month = apr, + publisher = {Springer}, +} + +@Article{Doyle:TMS, + author = {Jon Doyle}, + title = {A Truth Maintenance System}, + journal = {Artificial Intelligence}, + year = {1979}, + month = nov, + volume = {12}, + number = {3}, + pages = {231-272}, +} + +@InProceedings{LeinoMueller:SpecSharp:Tutorial, + author = {K. Rustan M. Leino and Peter M{\"u}ller}, + title = {Using the {Spec\#} Language, Methodology, and Tools to Write Bug-Free Programs}, + booktitle = {LASER Summer School 2007/2008}, + editor = {Peter M{\"u}ller}, + series = lncs, + volume = 6029, + year = 2010, + publisher = {Springer}, + pages = {91-139}, +} + +@inproceedings{TFNP-TACAS15, + author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova}, + title = {{AutoProof}: Auto-active Functional Verification of Object-oriented Programs}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- 21st International Conference, TACAS 2015}, + editor = {Christel Baier and Cesare Tinelli}, + series = lncs, + volume = {9035}, + month = apr, + year = {2015}, + publisher = {Springer}, + pages = {566-580}, +} + +@inproceedings{PTFM-FM14, + author = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia and Bertrand Meyer}, + title = {Flexible Invariants Through Semantic Collaboration}, + booktitle = {FM 2014}, + series = lncs, + volume = {8442}, + publisher = {Springer}, + month = may, + year = {2014}, + pages = {514-530} +} + +@InProceedings{VeriFast:Java:tutorial, + author = {Jan Smans and Bart Jacobs and Frank Piessens}, + title = {{VeriFast} for {J}ava: A Tutorial}, + booktitle = {Aliasing in Object-Oriented Programming. Types, Analysis and Verification}, + year = {2013}, + editor = {Dave Clarke and James Noble and Tobias Wrigstad}, + volume = {7850}, + series = lncs, + pages = {407-442}, + publisher = {Springer}, +} + +@InProceedings{Traits:ECOOP2003, + author = {Nathanael Sch{\"a}rli and St{\'e}phane Ducasse and Oscar Nierstrasz and Andrew P. Black}, + title = {Traits: Composable Units of Behaviour}, + booktitle = {ECOOP 2003 --- Object-Oriented Programming, 17th European Conference}, + editor = {Luca Cardelli}, + series = lncs, + volume = {2743}, + pages = {248-274}, + month = jul, + year = {2003}, + publisher = {Springer}, +} + +@Article{Traits:logic, + author = {Ferruccio Damiani and Johan Dovland and Einar Broch Johnsen and Ina Schaefer}, + title = {Verifying traits: an incremental proof system for fine-grained reuse}, + journal = {Formal Aspects of Computing}, + volume = {26}, + number = {4}, + pages = {761-793}, + month = jul, + year = {2014}, +} + +@inproceedings{LeinoPolikarpova:calc, + author = {K. Rustan M. Leino and + Nadia Polikarpova}, + title = {Verified Calculations}, + booktitle = {VSTTE 2013}, + series = lncs, + volume = 8164, + year = {2014}, + pages = {170-190}, + publisher = {Springer}, +} + +@Article{LeinoYessenov:ChaliceRefinement, + author = {K. Rustan M. Leino and Kuat Yessenov}, + title = {Stepwise refinement of heap-manipulating code in {C}halice}, + journal = {Formal Aspects of Computing}, + year = {2012}, + volume = {24}, + number = {4--6}, + pages = {519--535}, + month = jul, +} + +@article{Wirth:StepwiseRefinment, + author = "N. Wirth", + title = "{Program Development by Stepwise Refinement}", + journal = cacm, + volume = 14, + year = 1971, + pages = "221-227" +} + +@article{Dijkstra:Refinement, + author = "E. W. Dijkstra", + title = "A constructive approach to the problem of program correctness", + journal = "BIT", + volume = 8, + year = 1968, + pages = "174-186" +} + +@phdthesis{Back:thesis, + author = "R.-J. R. Back", + title = "On the Correctness of Refinement Steps in Program Development", + school = "University of Helsinki", + year = 1978, + note = "Report A-1978-4" +} + +@article{Morgan:SpecStmt, + author = "Carroll Morgan", + title = "The Specification Statement", + journal = toplas, + volume = 10, + number = 3, + year = 1988, + month = jul, + pages = "403-419" +} + +@book{Morgan:book, + author = "Carroll Morgan", + title = "Programming from Specifications", + publisher = "Prentice-Hall International", + series = "Series in Computer Science", + year = 1990 +} + +@article{Morris:Refinement, + author = "Joseph M. Morris", + title = "A theoretical basis for stepwise refinement and the + programming calculus", + journal = scp, + volume = 9, + number = 3, + month = dec, + year = 1987, + pages = "287-306" +} + +@article{GriesVolpano:Transform, + author = "David Gries and Dennis Volpano", + title = "The Transform --- a New Language Construct", + journal = "Structured Programming", + volume = 11, + number = 1, + year = 1990, + pages = "1-10" +} + +@Book{Abrial:BBook, + author = "J.-R. Abrial", + title = "The {B}-Book: Assigning Programs to Meanings", + publisher = "Cambridge University Press", + year = 1996 +} + +@Book{Jones:VDM:book, + Author = "Cliff B. Jones", + Title = "Systematic Software Development Using {VDM}", + Publisher = "Prentice Hall", + Series = "International Series in Computer Science", + Address = "Englewood Cliffs, N.J.", + Edition = "Second", + Year = 1990 +} + +@Book{Abrial:EventB:book, + author = {Jean-Raymond Abrial}, + title = {Modeling in {Event-B}: System and Software Engineering}, + publisher = {Cambridge University Press}, + year = {2010}, +} + +@Misc{ClearSy:AtelierB, + author = {ClearSy}, + title = {Atelier {B}}, + howpublished = {\url{http://www.atelierb.eu/}}, +} + +@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}, +} + +@Book{Abrial:EventB-book, + author = {Jean-Raymond Abrial}, + title = {Modeling in {Event-B}: System and Software Engineering}, + publisher = {Cambridge University Press}, + year = {2010}, +} + +@Article{BackSere:ActionSystems, + author = {Ralph-Johan Back and Kaisa Sere}, + title = {Stepwise Refinement of Action Systems}, + journal = {Structured Programming}, + year = {1991}, + volume = {12}, + number = {1}, + pages = {17-30}, +} + +@InProceedings{VCC:overview, + author = {Ernie Cohen and Markus Dahlweid and Mark 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}, + month = aug, + year = {2009}, + pages = {23-42}, +} + +@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}, +} + +@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 +} + +@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}, +} + +@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" +} + +@manual{baudin09acsl, + title = {{ACSL}: {ANSI}/{ISO} {C} Specification Language, version 1.4}, + author = {Patrick Baudin and Jean-Christophe Filli{\^a}tre and + Claude March{\'e} and Benjamin Monate and Yannick + Moy and Virgile Prevosto}, + year = 2009, + note = {\url{http://frama-c.com/}} +} + +@InProceedings{BarnettEtAl:Boogie, + 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" +} + +@inproceedings{deMouraBjorner:Z3:overview, + author = "de Moura, Leonardo and Nikolaj Bj{\o}rner", + title = {{Z3}: An efficient {SMT} solver}, + booktitle = {TACAS 2008}, + series = lncs, + volume = 4963, + publisher = {Springer}, + month = mar # "--" # apr, + year = 2008, + pages = {337-340}, +} + +@Article{Back-Mikhajlova-vonWright:ClassRefinement, + author = {Ralph-Johan Back and Anna Mikhaljova and von Wright, Joakim}, + title = {Class Refinement as Semantics of Correct Object Substitutability}, + journal = {Formal Aspects of Computing}, + volume = {12}, + number = {1}, + year = {2000}, + month = oct, + pages = {18-40}, +} + +@InProceedings{MikhajlovaSekerinski:ClassRefinement, + author = {Anna Mikhaljova and Emil Sekerinski}, + title = {Class Refinement and Interface Refinement in Object-Oriented Programs}, + booktitle = {FME '97: Industrial Applications and Strengthened + Foundations of Formal Methods, 4th International + Symposium of Formal Methods Europe}, + editor = {John S. Fitzgerald and Cliff B. Jones and Peter Lucas}, + volume = {1313 }, + series = lncs, + publisher = {Springer}, + month = sep, + year = {1997}, + pages = {82-101}, +} + +@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}, +} + +@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 Robert Gorrieri}, + volume = {5705}, + series = lncs, + publisher = {Springer}, + year = {2009}, + pages = {195-222}, +} + +@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{tafat10foveoos, + author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e}, + title = {A Refinement Methodology for Object-Oriented Programs}, + booktitle = {Formal Verification of Object-Oriented Software, Papers + Presented at the International Conference}, + editor = {Bernhard Beckert and Claude March\'e}, + month = jun, + year = 2010, + pages = {143--159}, +} + +@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}, +} + +@TechReport{HatcliffEtAl:survey-tr, + 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}, + institution = {University of Central Florida, School of EECS}, + month = oct, + year = {2010}, + number = {CS-TR-09-01a}, +} + +@Article{HatcliffEtAl:survey:journal:tentativeInfo, + 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}, + year = {2012}, + volume = {44}, + number = {3}, + month = may, +} + +@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{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}, +} + +@Misc{Escher, + author = "{Escher Technologies, Inc.}", + title = "Getting started with {P}erfect", + howpublished = "\url{http://www.eschertech.com}", + year = 2001 +} + +@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" +} + +@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{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}, +} + +# References supplied by the reviewers. +# Added 12/20/11. + +@incollection{Potet:BComposition, + author = {Potet, Marie and Rouzaud, Yann}, + affiliation = {LSR-IMAG Grenoble France}, + title = {Composition and refinement in the B-method}, + booktitle = {B￿￿98: Recent Advances in the Development and Use of the B Method}, + series = lncs, + editor = {Bert, Didier}, + publisher = {Springer Berlin / Heidelberg}, + isbn = {978-3-540-64405-7}, + keyword = {Computer Science}, + pages = {46-65}, + volume = {1393}, + url = {http://dx.doi.org/10.1007/BFb0053355}, + note = {10.1007/BFb0053355}, + year = {1998} +} + +@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}, +} + +@inproceedings{Wehrheim:Subtypes, + author = {Heike Wehrheim}, + title = {Checking Behavioural Subtypes via Refinement}, + booktitle = {FMOODS}, + year = {2002}, + pages = {79-93}, + crossref = {DBLP:conf/fmoods/2002}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@article{Banerjee:ownership, + author = {Banerjee, Anindya and Naumann, David A.}, + title = {Ownership confinement ensures representation independence for object-oriented programs}, + journal = jacm, + volume = {52}, + issue = {6}, + month = {November}, + year = {2005}, + issn = {0004-5411}, + pages = {894--960}, + numpages = {67}, + url = {http://doi.acm.org/10.1145/1101821.1101824}, + doi = {http://doi.acm.org/10.1145/1101821.1101824}, + acmid = {1101824}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {Alias control, confinement, data refinement, relational parametricity, simulation}, +} + +@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, +} + +@InProceedings{Heule:FractionsWithoutFractions, + author = {Stefan Heule and K. Rustan M. Leino and Peter + M{\"u}ller and Alexander J. Summers}, + title = {Fractional Permissions without the Fractions}, + booktitle = {13th Workshop on Formal Techniques for Java-like + Programs, FTfJP 2011}, + year = {2011}, + month = jul, +} + +@incollection{Morgan:Capjunctive, + author = "Carroll Morgan", + title = "The Cuppest Capjunctive Capping, and {G}alois", + editor = "A. W. Roscoe", + booktitle = "A Classical Mind: Essays in Honour of C.A.R. Hoare", + publisher = "Prentice-Hall", + series = "International Series in Computer Science", + pages = "317-332", + year = 1994 +} + +@Article{Morgan:CompositionalNoninterference, + author = {Carroll Morgan}, + title = {Compositional noninterference from first principles}, + journal = fac, + year = {2012}, + volume = {24}, + number = {1}, + pages = {3-26}, +} + +@article{DenningDenning:Certification, + author = "Dorothy E. Denning and Peter J. Denning", + title = "Certification of Programs for Secure Information Flow", + journal = cacm, + volume = 20, + number = 7, + month = jul, + year = 1977, + pages = "504-513" +} + +@article{Jones:Interference, + author = "C. B. Jones", + title = "Accommodating interference in the formal design of + concurrent object-based programs", + journal = "Formal Methods in System Design", + volume = 8, + number = 2, + pages = "105-122", + month = mar, + year = 1996 +} + +@Book{Jackson:Alloy:book, + author = {Daniel Jackson}, + title = {Software Abstractions: Logic, Language, and Analysis}, + publisher = {MIT Press}, + year = {2006}, +} + +@inproceedings{LeuschelButler:FME03, + author = {Michael Leuschel and Michael Butler}, + title = {Pro{B}: A Model Checker for {B}}, + booktitle = {FME 2003: Formal Methods}, + editor = {Araki, Keijiro and Gnesi, Stefania and Mandrioli, Dino}, + publisher = {Springer}, + series = lncs, + number = {2805}, + year = 2003, + pages = {855-874}, +} + +@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}, +} + +@Article{LiskovWing94, + author = "Barbara Liskov and Jeannette M. Wing", + title = "A Behavioral Notion of Subtyping", + journal = toplas, + year = 1994, + volume = 16, + number = 6 +} + +@book{WoodcockDavies:UsingZ, + title = "Using {Z}: Specification, Refinement, and Proof", + author = "Jim Woodcock and Jim Davies", + year = "1996", + publisher = "Prentice Hall International", +} + +@Article{Leavens:ModularOOSpecs, + author = {Gary T. Leavens}, + title = {Modular Specification and Verification of Object-Oriented Programs}, + journal = {IEEE Software}, + year = {1991}, + volume = {8}, + number = {4}, + pages = {72-80}, +} + +@InProceedings{ShieldHayes:InvsAndDynConstraints, + author = {Jamie Shield and Ian J. Hayes}, + title = {Refining Object-Oriented Invariants and Dynamic Constraints}, + booktitle = {9th Asia-Pacific Software Engineering Conference (APSEC 2002)}, + pages = {52-61}, + year = {2002}, + publisher = {IEEE Computer Society}, +} + +@TechReport{Chalice:predicates:TR, + author = {S. Heule and I. T. Kassios and P. M\"uller and A. J. Summers}, + title = {Verification Condition Generation for Permission Logics with Abstraction Functions}, + institution = {ETH Zurich}, + year = {2012}, + number = {761} +} + +@InCollection{KleinEtAl:DataRefinement, + author = {Gerwin Klein and Thomas Sewell and Simon Winwood}, + title = {Refinement in the formal verification of {seL4}}, + booktitle = {Design and Verification of Microprocessor Systems for High-Assurance Applications}, + editor = {David S. Hardin}, + pages = {323--339}, + month = Mar, + year = {2010}, + publisher = {Springer}, +} + +@InProceedings{DharaLeavens:forcing, + author = {Krishna Kishore Dhara and Gary T. Leavens}, + title = {Forcing Behavioral Subtyping through Specification Inheritance}, + booktitle = {18th International Conference on Software Engineering}, + year = {1996}, + editor = {H. Dieter Rombach and T. S. E. Maibaum and Marvin V. Zelkowitz}, + pages = {258-267}, + month = mar, + publisher = {IEEE Computer Society}, +} + +@InProceedings{SpiritOfGhostCode, + author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and Andrei Paskevich}, + title = {The Spirit of Ghost Code}, + booktitle = {Computer Aided Verification --- 26th International Conference, CAV 2014}, + year = {2014}, + editor = {Armin Biere and Roderick Bloem}, + series = lncs, + volume = {8559}, + pages = {1-16}, + month = jul, + publisher = {Springer}, +} + +@InProceedings{Dafny:traits, + author = {Reza Ahmadi and K. Rustan M. Leino and Jyrki Nummenmaa}, + title = {Automatic Verification of {D}afny Programs with Traits}, + booktitle = {Formal Techniques for {J}ava-like Programs, FTfJP 2015}, + year = {2015}, + editor = {Rosemary Monahan}, + publisher = {ACM}, +} + +@InProceedings{Dafny:Cloudmake, + author = {Maria Christakis and K. Rustan M. Leino and Wolfram Schulte}, + title = {Formalizing and Verifying a Modern Build Language}, + booktitle = {FM 2014: Formal Methods --- 19th International Symposium}, + year = {2014}, + editor = {Cliff B. Jones and Pekka Pihlajasaari and Jun Sun}, + volume = {8442}, + series = lncs, + pages = {643-657}, + month = may, + publisher = {Springer}, +} + +@Misc{Leino:SPLASH2012:keynote, + author = {K. Rustan M. Leino}, + title = {Staged Program Development}, + howpublished = {SPLASH 2012 keynote}, + note = {InfoQ video, \url{http://www.infoq.com/presentations/Staged-Program-Development}}, + month = oct, + year = {2012}, +} + +@article{Parnas:secret, + author = "D. L. Parnas", + title = "On the criteria to be used in decomposing systems into modules", + journal = cacm, + volume = 15, + number = 12, + month = dec, + year = 1972, + pages = "1053-1058", + note = "Reprinted as {\tt www.acm.org/classics/may96/}" +} + +@InProceedings{KIV:overview, + author = {Wolfgang Reif}, + title = {The {KIV} System: Systematic Construction of Verified Software}, + booktitle = {Automated Deduction --- CADE-11, 11th International Conference + on Automated Deduction}, + editor = {Deepak Kapur}, + series = lncs, + volume = {607}, + publisher = {Springer}, + pages = {753-757}, + month = jun, + year = {1992}, +} + +@InProceedings{LeinoMoskal:Coinduction, + author = {K. Rustan M. Leino and Micha{\l} Moskal}, + title = {Co-induction Simply --- Automatic Co-inductive Proofs in a Program Verifier}, + booktitle = {FM 2014}, + series = lncs, + volume = {8442}, + publisher = {Springer}, + month = may, + year = {2014}, + pages = {382-398}, +} + +@Article{Tarski:theorem, + author = "Alfred Tarski", + title = "A lattice-theoretical fixpoint theorem and its applications", + journal = "Pacific Journal of Mathematics", + year = 1955, + volume = 5, + pages = "285-309" +} + +@TechReport{KozenSilva:Coinduction, + author = {Dexter Kozen and Alexandra Silva}, + title = {Practical coinduction}, + institution = {Comp. and Inf. Science, Cornell Univ.}, + year = {2012}, + number = {\url{http://hdl.handle.net/1813/30510}}, +} + +@book{Milner:CCS, + author = "Robin Milner", + title = {A Calculus of Communicating Systems}, + year = {1982}, + publisher = {Springer}, +} + +@Book{NipkowKlein:ConcreteSemantics, + author = {Tobias Nipkow and Gerwin Klein}, + title = {Concrete Semantics with {I}sabelle/{HOL}}, + publisher = {Springer}, + year = {2014}, +} + +@Book{Pierce:SoftwareFoundations, + author = {Benjamin C. Pierce and Chris Casinghino and + Marco Gaboardi and Michael Greenberg and + C{\u{a}}t{\u{a}}lin Hri\c{t}cu and Vilhelm Sj{\"o}berg and + Brent Yorgey}, + title = {Software Foundations}, + publisher = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}, + year = {2015}, + edition = {version 3.2}, + month = jan, +} + +@InProceedings{ClochardEtAl:SemanticsInWhy3, + author = {Martin Clochard and Jean-Christophe + Filli\^atre and Claude March\'e and Andrei Paskevich}, + title = {Formalizing Semantics with an Automatic Program Verifier}, + booktitle = {VSTTE 2014}, + volume = {8471}, + series = lncs, + publisher = {Springer}, + month = jul, + year = {2014}, + pages = {37--51}, +} + +@Article{LeroyGrall:CoinductiveBigStep, + author = {Xavier Leroy and Herv\'e Grall}, + title = {Coinductive big-step operational semantics}, + journal = {Information and Computation}, + volume = {207}, + number = {2}, + pages = {284-304}, + month = feb, + year = {2009}, +} + +@InProceedings{SwamyEtAl:Fstar2011, + author = {Nikhil Swamy and Juan Chen and C{\'e}dric Fournet and + Pierre-Yves Strub and Karthikeyan Bhargavan and Jean Yang}, + title = {Secure distributed programming with value-dependent types}, + booktitle = {ICFP 2011}, + publisher = {ACM}, + month = sep, + year = {2011}, + pages = {266-278}, +} + +@Book{Nipkow-Paulson-Wenzel02, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic}, + publisher = {Springer}, + year = 2002, + volume = 2283, + series = LNCS, +} + +@InProceedings{BoveDybjerNorell:BriefAgda, + author = {Ana Bove and Peter Dybjer and Ulf Norell}, + title = {A Brief Overview of {A}gda --- A Functional Language with Dependent Types}, + booktitle = {TPHOLs 2009}, + series = lncs, + volume = {5674}, + publisher = {Springer}, + month = aug, + year = {2009}, + pages = {73-78}, +} + +@InProceedings{PaulinMohring:InductiveCoq, + author = {Christine Paulin-Mohring}, + title = {Inductive Definitions in the system {C}oq --- Rules and Properties}, + booktitle = {TLCA '93}, + series = lncs, + volume = {664}, + pages = {328-345}, + year = {1993}, + publisher = {Springer}, +} + +@TechReport{CamilleriMelham:InductiveRelations, + author = {Juanito Camilleri and Tom Melham}, + title = {Reasoning with Inductively Defined Relations + in the {HOL} Theorem Prover}, + institution = {University of Cambridge Computer Laboratory}, + year = {1992}, + number = {265}, + OPTmonth = aug, +} + +@Book{Winskel:FormalSemantics, + author = {Glynn Winskel}, + title = {The Formal Semantics of Programming Languages: An Introduction}, + publisher = {MIT Press}, + year = {1993}, +} + +@inproceedings{Paulson:CADE1994, + author = {Lawrence C. Paulson}, + title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions}, + booktitle = {CADE-12}, + editor = {Alan Bundy}, + volume = {814}, + series = lncs, + publisher = {Springer}, + year = {1994}, + pages = {148-161}, +} + +@InProceedings{Harrison:InductiveDefs, + author = {John Harrison}, + title = {Inductive Definitions: Automation and Application}, + booktitle = {TPHOLs 1995}, + year = {1995}, + editor = {E. Thomas Schubert and Phillip J. Windley and Jim Alves-Foss}, + volume = {971}, + series = lncs, + pages = {200-213}, + publisher = {Springer}, +} + +@Article{ManoliosMoore:PartialFunctions, + author = {Panagiotis Manolios and J Strother Moore}, + title = {Partial Functions in {ACL2}}, + journal = {Journal of Automated Reasoning}, + year = {2003}, + volume = {31}, + number = {2}, + pages = {107-127}, +} + +@PhdThesis{Krauss:PhD, + author = {Alexander Krauss}, + title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic}, + school = {Technische Universit{\"a}t M{\"u}nchen}, + year = {2009}, +} + -- cgit v1.2.3