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/paper-full.bib | 577 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 577 insertions(+) create mode 100644 Docs/DafnyRef/paper-full.bib (limited to 'Docs/DafnyRef/paper-full.bib') diff --git a/Docs/DafnyRef/paper-full.bib b/Docs/DafnyRef/paper-full.bib new file mode 100644 index 00000000..c382df3b --- /dev/null +++ b/Docs/DafnyRef/paper-full.bib @@ -0,0 +1,577 @@ +@string{lncs = "Lecture Notes in Computer Science"} +@string{lnai = "Lecture Notes in Artificial Intelligence"} + +@InProceedings{Dafny:LPAR16, + author = {K. Rustan M. Leino}, + title = {Dafny: An Automatic Program Verifier for Functional Correctness}, + booktitle = {LPAR-16}, + year = {2010}, + volume = {6355}, + series = lncs, + publisher = {Springer}, + month = apr, + editor = {Edmund M. Clarke and Andrei Voronkov}, + pages = {348-370}, +} + +@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{Leino:VMCAI2012, + author = {K. Rustan M. Leino}, + title = {Automating Induction with an {SMT} Solver}, + booktitle = {Verification, Model Checking, and Abstract Interpretation --- 13th International Conference, VMCAI 2012}, + pages = {315-331}, + year = {2012}, + editor = {Viktor Kuncak and Andrey Rybalchenko}, + volume = {7148}, + series = lncs, + month = jan, + publisher = {Springer}, +} + +@InProceedings{LeinoMonahan:Comprehensions, + author = {K. Rustan M. Leino and Rosemary Monahan}, + title = {Reasoning about Comprehensions with First-Order {SMT} Solvers}, + booktitle = {Proceedings of the 2009 ACM Symposium on Applied Computing (SAC)}, + editor = {Sung Y. Shin and Sascha Ossowski}, + publisher = {ACM}, + month = mar, + year = 2009, + pages = {615-622}, +} + +@TechReport{VeriFast:TR, + author = {Bart Jacobs and Frank Piessens}, + title = {The {VeriFast} program verifier}, + institution = {Department of Computer Science, Katholieke Universiteit Leuven}, + year = {2008}, + number = {CW-520}, + month = aug, +} + +@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{Paulson:coinduction2000, + author = {Lawrence C. Paulson}, + title = {A fixedpoint approach to (co)inductive and (co)datatype + definitions}, + booktitle = {Proof, Language, and Interaction}, + year = {2000}, + pages = {187-212}, + crossref = {DBLP:conf/birthday/1999milner}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/birthday/1999milner, + editor = {Gordon D. Plotkin and + Colin Stirling and + Mads Tofte}, + title = {Proof, Language, and Interaction, Essays in Honour of Robin + Milner}, + booktitle = {Proof, Language, and Interaction}, + publisher = {The MIT Press}, + year = {2000}, + isbn = {978-0-262-16188-6}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + +@inproceedings{Paulson:coinduction1994, + author = {Lawrence C. Paulson}, + title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions}, + booktitle = {CADE}, + year = {1994}, + pages = {148-161}, + ee = {http://dx.doi.org/10.1007/3-540-58156-1_11}, + crossref = {DBLP:conf/cade/1994}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/cade/1994, + editor = {Alan Bundy}, + title = {Automated Deduction - CADE-12, 12th International Conference + on Automated Deduction, Nancy, France, June 26 - July 1, + 1994, Proceedings}, + booktitle = {CADE}, + publisher = {Springer}, + series = lncs, + volume = {814}, + year = {1994}, + isbn = {3-540-58156-1}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + +@inproceedings{Hausmann:CoCasl, + author = {Daniel Hausmann and + Till Mossakowski and + Lutz Schr{\"o}der}, + title = {Iterative Circular Coinduction for {CoCasl} in {I}sabelle/{HOL}}, + booktitle = {Fundamental Approaches to Software Engineering, 8th International + Conference, FASE 2005}, + editor = {Maura Cerioli}, + series = lncs, + volume = {3442}, + publisher = {Springer}, + year = {2005}, + pages = {341-356}, +} + +@inproceedings{Rosu:CIRC, + author = {Dorel Lucanu and + Grigore Rosu}, + title = {{CIRC}: A Circular Coinductive Prover}, + booktitle = {CALCO}, + year = {2007}, + pages = {372-378}, + ee = {http://dx.doi.org/10.1007/978-3-540-73859-6_25}, + crossref = {DBLP:conf/calco/2007}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/calco/2007, + editor = {Till Mossakowski and + Ugo Montanari and + Magne Haveraaen}, + title = {Algebra and Coalgebra in Computer Science, Second International + Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, + Proceedings}, + booktitle = {CALCO}, + publisher = {Springer}, + series = lncs, + volume = {4624}, + year = {2007}, + isbn = {978-3-540-73857-2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + +@inproceedings{Rosu:circRule, + author = {Grigore Rosu and + Dorel Lucanu}, + title = {Circular Coinduction: A Proof Theoretical Foundation}, + booktitle = {CALCO}, + year = {2009}, + pages = {127-144}, + ee = {http://dx.doi.org/10.1007/978-3-642-03741-2_10}, + crossref = {DBLP:conf/calco/2009}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/calco/2009, + editor = {Alexander Kurz and + Marina Lenisa and + Andrzej Tarlecki}, + title = {Algebra and Coalgebra in Computer Science, Third International + Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. + Proceedings}, + booktitle = {CALCO}, + publisher = {Springer}, + series = lncs, + volume = {5728}, + year = {2009}, + isbn = {978-3-642-03740-5}, + ee = {http://dx.doi.org/10.1007/978-3-642-03741-2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@inproceedings{VCC, + author = {Ernie Cohen and + Markus Dahlweid and + Mark A. Hillebrand and + Dirk Leinenbach and + Micha{\l} Moskal and + Thomas Santen and + Wolfram Schulte and + Stephan Tobies}, + title = {{VCC}: A Practical System for Verifying Concurrent {C}}, + booktitle = {TPHOLs 2009}, + series = LNCS, + publisher = {Springer}, + volume = {5674}, + year = {2009}, + pages = {23-42}, +} + +@InProceedings{VeriFast:ProgramsAsProofs, + author = {Bart Jacobs and Jan Smans and Frank Piessens}, + title = {{VeriFast}: Imperative Programs as Proofs}, + booktitle = {VS-Tools workshop at VSTTE 2010}, + year = {2010}, + month = aug, +} + +@book{DijkstraScholten:book, + author = "Edsger W. Dijkstra and Carel S. Scholten", + title = "Predicate Calculus and Program Semantics", + publisher = "Springer-Verlag", + series = "Texts and Monographs in Computer Science", + year = 1990 +} + +@Book{BirdWadler:IntroFunctionalProgramming, + author = {Richard Bird and Philip Wadler}, + title = {Introduction to Functional Programming}, + publisher = {Prentice Hall}, + series = {International Series in Computing Science}, + year = {1992}, +} + +@inproceedings{Z3, + author = "de Moura, Leonardo and Nikolaj Bj{\o}rner", + title = {{Z3}: An efficient {SMT} solver}, + booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, 14th International Conference, + TACAS 2008}, + editor = {C. R. Ramakrishnan and Jakob Rehof}, + series = lncs, + volume = 4963, + publisher = {Springer}, + year = 2008, + pages = {337-340}, +} + +@phdthesis{moy09phd, + author = {Yannick Moy}, + title = {Automatic Modular Static Safety Checking for C Programs}, + school = {Universit{\'e} Paris-Sud}, + year = 2009, + month = jan, + topics = {team}, + x-equipes = {demons PROVAL}, + x-type = {these}, + x-support = {rapport}, + url = {http://www.lri.fr/~marche/moy09phd.pdf} +} +@Book{PeytonJones:Haskell, + author = {Peyton Jones, Simon}, + title = {Haskell 98 language and libraries: the Revised Report}, + publisher = {Cambridge University Press}, + year = {2003}, +} + +@InProceedings{Park:InfSeq, + author = {David Park}, + title = {Concurrency and automata on infinite sequences}, + booktitle = {Theoretical Computer Science, 5th GI-Conference}, + editor = {Peter Deussen}, + volume = {104}, + series = lncs, + publisher = {Springer}, + year = {1981}, + pages = {167-183}, +} + +@Article{Leroy:CompCert:CACM, + author = {Xavier Leroy}, + title = {Formal verification of a realistic compiler}, + journal = cacm, + volume = {52}, + number = {7}, + month = jul, + year = {2009}, + pages = {107-115}, +} + +@Book{KeY:book, + author = {Bernhard Beckert and Reiner H{\"a}hnle and Peter H. Schmitt}, + title = {Verification of Object-Oriented Software: The {KeY} Approach}, + volume = 4334, + series = lnai, + publisher = {Springer}, + year = 2007, +} + +@Book{Nipkow-Paulson-Menzel02, + author = {Tobias Nipkow and Lawrence Paulson and Markus Menzel}, + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic}, + publisher = {Springer}, + year = 2002, + volume = 2283, + series = LNCS, +} + +@Book{Coq:book, + author = {Yves Bertot and Pierre Cast{\'e}ran}, + title = {Interactive Theorem Proving and Program Development --- {C}oq'{A}rt: The Calculus of Inductive Constructions}, + publisher = {Springer}, + year = {2004}, + series = {Texts in Theoretical Computer Science}, +} + +@Book{ACL2:book, + author = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore}, + title = {Computer-Aided Reasoning: An Approach}, + publisher = {Kluwer Academic Publishers}, + year = {2000}, +} + +@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{Bertot:CoinductionInCoq, + location = {http://www.scientificcommons.org/8157029}, + title = {CoInduction in {C}oq}, + author = {Bertot, Yves}, + year = {2005}, + publisher = {HAL - CCSd - CNRS}, + url = {http://hal.inria.fr/inria-00001174/en/}, + institution = {CCSd/HAL : e-articles server (based on gBUS) [http://hal.ccsd.cnrs.fr/oai/oai.php] (France)}, +} + +@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}, +} + +@InProceedings{Boogie:Architecture, + author = "Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and + Bart Jacobs and K. Rustan M. Leino", + title = "{B}oogie: A Modular Reusable Verifier for Object-Oriented Programs", + booktitle = "Formal Methods for Components and Objects: 4th + International Symposium, FMCO 2005", + editor = "de Boer, Frank S. and Marcello M. Bonsangue and + Susanne Graf and de Roever, Willem-Paul", + series = lncs, + volume = 4111, + publisher = "Springer", + month = sep, + year = 2006, + pages = "364-387" +} + +@InCollection{JacobsRutten:IntroductionCoalgebra, + author = {Bart Jacobs and Jan Rutten}, + title = {An Introduction to (Co)Algebra and (Co)Induction}, + booktitle = {Advanced Topics in Bisimulation and Coinduction}, + editor = {Davide Sangiorgi and Jan Rutten}, + series = {Cambridge Tracts in Theoretical Computer Science}, + number = {52}, + publisher = {Cambridge University Press}, + month = oct, + year = {2011}, + pages = {38-99}, +} + +@Book{Chlipala, + author = {Adam Chlipala}, + title = {Certified Programming with Dependent Types}, + publisher = {MIT Press}, + year = {To appear}, + note = {http://adam.chlipala.net/cpdt/} +} + +@Misc{Charity, + author = {Robin Cockett}, + title = {The {CHARITY} home page}, + howpublished = {\url{http://pll.cpsc.ucalgary.ca/charity1/www/home.html}}, + year = {1996}, +} + +@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" +} + +@InProceedings{PVS, + author = "Sam Owre and S. Rajan and John M. Rushby and Natarajan + Shankar and Mandayam K. Srivas", + title = "{PVS}: Combining Specification, Proof Checking, and Model + Checking", + editor = "Rajeev Alur and Thomas A. Henzinger", + booktitle = "Computer Aided Verification, 8th International + Conference, CAV '96", + volume = 1102, + series = lncs, + publisher = "Springer", + year = 1996, + pages = "411-414" +} + +@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}, +} + +@book{Milner:CCS, + author = "Robin Milner", + title = {A Calculus of Communicating Systems}, + year = {1982}, + isbn = {0387102353}, + publisher = {Springer-Verlag New York, Inc.}, +} + +@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}, +} + +@PhdThesis{Norell:PhD, + author = {Ulf Norell}, + title = {Towards a practical programming language based on dependent type theory}, + school = {Department of Computer Science and Engineering, Chalmers + University of Technology}, + year = {2007}, + month = sep, +} + +@Article{Paulson:MechanizingCoRecursion, + author = {Lawrence C. Paulson}, + title = {Mechanizing Coinduction and Corecursion in Higher-order Logic}, + journal = {Journal of Logic and Computation}, + year = {1997}, + volume = {7}, +} + +@InProceedings{Bertot:sieve, + author = {Yves Bertot}, + title = {Filters on CoInductive Streams, an Application to {E}ratosthenes' Sieve}, + booktitle = {Typed Lambda Calculi and Applications, 7th International Conference, + TLCA 2005}, + editor = {Pawel Urzyczyn}, + series = lncs, + volume = {3461}, + month = apr, + year = {2005}, + pages = {102-115}, + publisher = {Springer}, +} + +@Misc{AltenkirchDanielsson:QuantifierInversion, + author = {Thorsten Altenkirch and Nils Anders Danielsson}, + title = {Termination Checking in the Presence of Nested Inductive and Coinductive Types}, + howpublished = {Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers}, + year = {2010}, + note = {Available from \url{http://www.cse.chalmers.se/~nad/publications/}.}, +} + +@InProceedings{HurEtAl:Paco, + author = {Hur, Chung-Kil and Neis, Georg and Dreyer, Derek and Vafeiadis, Viktor}, + title = {The power of parameterization in coinductive proof}, + booktitle = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13}, + editor = {Roberto Giacobazzi and Radhia Cousot}, + pages = {193--206}, + month = jan, + year = {2013}, + publisher = {ACM}, +} + +@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 = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009}, + editor = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel}, + series = lncs, + volume = {5674}, + publisher = {Springer}, + month = aug, + year = {2009}, + pages = {73-78}, +} + +@Article{Moore:Piton, + author = {J Strother Moore}, + title = {A Mechanically Verified Language Implementation}, + journal = {Journal of Automated Reasoning}, + year = {1989}, + volume = {5}, + number = {4}, + pages = {461-492}, +} + +@InProceedings{Leroy:ESOP2006, + author = {Xavier Leroy}, + title = {Coinductive Big-Step Operational Semantics}, + booktitle = {Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006}, + pages = {54-68}, + year = {2006}, + editor = {Peter Sestoft}, + volume = {3924}, + series = lncs, + month = mar, + publisher = {Springer}, +} + +@InProceedings{Leino:ITP2013, + author = {K. Rustan M. Leino}, + title = {Automating Theorem Proving with {SMT}}, + booktitle = {Interactive Theorem Proving --- 4th International Conference, ITP 2013}, + year = {2013}, + editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}, + volume = {7998}, + series = lncs, + pages = {2-16}, + month = jul, + publisher = {Springer}, +} + +@TechReport{TR-version, + author = {K. Rustan M. Leino and Micha{\l} Moskal}, + title = {Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier}, + institution = {Microsoft Research}, + year = {2013}, + number = {MSR-TR-2013-49}, + month = may, +} -- cgit v1.2.3