diff options
Diffstat (limited to 'Docs/DafnyRef/paper-full.bib')
| -rw-r--r-- | Docs/DafnyRef/paper-full.bib | 577 |
1 files changed, 577 insertions, 0 deletions
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,
+}
|