summaryrefslogtreecommitdiff
path: root/Docs/DafnyRef/krml250.bib
diff options
context:
space:
mode:
Diffstat (limited to 'Docs/DafnyRef/krml250.bib')
-rw-r--r--Docs/DafnyRef/krml250.bib2026
1 files changed, 2026 insertions, 0 deletions
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},
+}
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 20:29:18 +0000