path: root/Docs/DafnyRef/paper-full.bib

@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,
}