path: root/Docs/DafnyRef/poc.bib

@string{lncs = "LNCS"}
@string{lnai = "LNAI"}

@InCollection{LeinoMoskal:UsableProgramVerification,
  author = 	 {K. Rustan M. Leino and Micha{\l} Moskal},
  title = 	 {Usable Auto-Active Verification},
  booktitle = 	 {Usable Verification workshop},
  year =	 {2010},
  editor =	 {Tom Ball and Lenore Zuck and N. Shankar},
  publisher =	 {\url{http://fm.csl.sri.com/UV10/}},
}
  booktitle = 	 {UV10 (Usable Verification) workshop},
  month =	 nov,

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

@Manual{Isabelle:Guide,
  title = 	 {Programming and Proving in {I}sabelle/{HOL}},
  author =	 {Tobias Nipkow},
  organization = {\url{http://isabelle.informatik.tu-muenchen.de/}},
  year =	 {2012},
}
  month = 	 may,

@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},
}
  editor =       {Edmund M. Clarke and Andrei Voronkov},
  month =        apr,

@InProceedings{VCC:TPHOLs,
  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},
  volume =       {5674},
  series =       lncs,
  publisher =    {Springer},
  year =         {2009},
  pages =        {23-42},
}
  booktitle =    {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009},
  editor =       {Stefan Berghofer and Tobias Nipkow and Christian
                  Urban and Makarius Wenzel},
  month =        aug,

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

@Article{IPL:vol53:3,
  author = 	 {Roland Backhouse},
  title = 	 {Special issue on The Calculational Method},
  journal = 	 {Information Processing Letters},
  year = 	 {1995},
  volume =	 {53},
  number =	 {3},
  pages =        {121-172},
}
  month =	 feb,

@InProceedings{VonWright:ExtendingWindowInference,
  author = 	 {von Wright, Joakim},
  title = 	 {Extending Window Inference},
  booktitle =	 {TPHOLs'98},
  pages =	 {17-32},
  year =	 {1998},
  volume =	 {1479},
  series =	 lncs,
  publisher =	 {Springer},
}
  booktitle =	 {Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98},
  editor =	 {Jim Grundy and Malcolm C. Newey},

@PhdThesis{Wenzel:PhD,
  author = 	 {Markus Wenzel},
  title = 	 {{I}sabelle/{I}sar --- a versatile environment for human-readable formal proof documents},
  school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
  year = 	 {2002},
}

@InProceedings{BauerWenzel:IsarExperience,
  author = 	 {Gertrud Bauer and Markus Wenzel},
  title = 	 {Calculational reasoning revisited: an {I}sabelle/{I}sar experience},
  booktitle =	 {TPHOLs 2001},
  pages =	 {75-90},
  year =	 {2001},
  volume =	 {2152},
  series =	 lncs,
  publisher =	 {Springer},
}
  booktitle =	 {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001},
  editor =	 {Richard J. Boulton and Paul B. Jackson},
  month =	 sep,

@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},
}
  volume =    {33},
  series =    {NATO Science for Peace and Security Series D: Information and Communication Security},
  editor =    {Tobias Nipkow and Orna Grumberg and Benedikt Hauptmann},  
  note =      {Summer School Marktoberdorf 2011 lecture notes},

@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,
  publisher =	 {Springer},
}
  booktitle =	 {Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012},
  editor =	 {Viktor Kuncak and Andrey Rybalchenko},
  month =	 jan,

@article{Hoare:AxiomaticBasis,
  author    = "C. A. R. Hoare",
  title     = "An axiomatic basis for computer programming",
  journal   = cacm,
  volume    = 12,
  number    = 10,
  year      = 1969,
  pages     = "576--580,583"
}
  month     = oct,

@Article{Simplify:tome,
  author = "David Detlefs and Greg Nelson and James B. Saxe",
  title = "Simplify: a theorem prover for program checking",
  journal = JACM,
  volume = 52,
  number = 3,
  year = 2005,
  pages = "365-473",
}
  month = may,

@techreport{Nelson:thesis,
  author = "Charles Gregory Nelson",
  title = "Techniques for Program Verification",
  institution = "Xerox PARC",
  year = 1981,
  number = "CSL-81-10",
  note = "PhD thesis, Stanford University"
}
  month = jun,

@inproceedings{deMouraBjorner:Z3:overview,
  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},
  series    = lncs,
  volume    = 4963,
  publisher = {Springer},
  year      = 2008,
  pages     = {337-340},
}
  editor    = {C. R. Ramakrishnan and Jakob Rehof},
  month     = mar # "--" # apr,

@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},
  volume =	 {7041},
  series =	 lncs,
  publisher =	 {Springer},
}
  editor =	 {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
  month =	 nov,

@InProceedings{HipSpec:WING,
  author = 	 {Koen Claessen and Moa Johansson and Dan Ros{\'e}n and Nicholas Smallbone},
  title = 	 {{HipSpec}: Automating Inductive Proofs of Program Properties},
  booktitle =	 {Workshop on {A}utomated {T}heory e{X}ploration: {ATX} 2012},
  year =	 {2012},
}
  month =	 jul,

@InProceedings{HipSpec:CADE,
  author = 	 {Koen Claessen and Moa Johansson and Dan Ros{\'e}n and Nicholas Smallbone},
  title = 	 {Automating Inductive Proofs Using Theory Exploration},
  booktitle =	 {CADE-24},
  pages =	 {392-406},
  year =	 {2013},
  volume =	 {7898},
  series =	 lncs,
  publisher =	 {Springer},
}
  booktitle =	 {Automated Deduction --- CADE-24 --- 24th International Conference on Automated Deduction},
  editor =	 {Maria Paola Bonacina},
  month =	 jun,

@article{ManoliosMoore:Calc,
  author    = {Panagiotis Manolios and J. Strother Moore},
  title     = {On the desirability of mechanizing calculational proofs},
  journal   = {Inf. Process. Lett.},
  volume    = {77},
  number    = {2-4},
  year      = {2001},
  pages     = {173-179},
  ee        = {http://dx.doi.org/10.1016/S0020-0190(00)00200-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Lifschitz:DS,
  title={On Calculational Proofs},
  author={Vladimir Lifschitz},
  volume={113},
  journal={Annals of Pure and Applied Logic},
  pages={207-224},
  url="http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805",
  year={2002}
}

@article{BackGrundyWright:SCP,
  author      = {Ralph Back and Jim Grundy and Joakim von Wright},
  title       = {Structured Calculational Proof},
  journal     = {Formal Aspects of Computing},
  year        = {1997},
  volume      = {9},
  number      = {5--6},
  pages       = {469--483}
}

@article{Back:SD,
 author = {Back, Ralph-Johan},
 title = {Structured derivations: a unified proof style for teaching mathematics},
 journal = {Formal Aspects of Computing},
 issue_date = {September 2010},
 volume = {22},
 number = {5},
 year = {2010},
 issn = {0934-5043},
 pages = {629--661},
 numpages = {33},
 url = {http://dx.doi.org/10.1007/s00165-009-0136-5},
 doi = {10.1007/s00165-009-0136-5},
 acmid = {1858559},
 publisher = {Springer},
} 
 month = sep,

@article{Dijkstra:EWD1300,
  author    = {Edsger W. Dijkstra},
  title     = {{EWD1300}: The Notational Conventions {I} Adopted, and Why},
  journal   = {Formal Asp. Comput.},
  volume    = {14},
  number    = {2},
  year      = {2002},
  pages     = {99-107},
  ee        = {http://dx.doi.org/10.1007/s001650200030},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BCDJL05:Boogie,
  author    = {Michael Barnett and
               Bor-Yuh Evan Chang and
               Robert DeLine and
               Bart Jacobs and
               K. Rustan M. Leino},
  title     = {Boogie: A Modular Reusable Verifier for Object-Oriented
               Programs},
  booktitle = {FMCO 2005},
  series = lncs,
  volume = 4111,
  publisher = "Springer",
  year      = {2006},
  pages     = {364-387},
}
  month = sep,

@article{BVW:Mathpad,
  author    = {Roland Backhouse and
               Richard Verhoeven and
               Olaf Weber},
  title     = {Math{$\!\!\int\!\!$}pad: A System for On-Line Preparation of Mathematical
               Documents},
  journal   = {Software --- Concepts and Tools},
  volume    = {18},
  number    = {2},
  year      = {1997},
  pages     = {80-},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{VB:MathpadPVS,
  author    = {Richard Verhoeven and
               Roland Backhouse},
  title     = {Interfacing Program Construction and Verification},
  booktitle = {World Congress on Formal Methods},
  year      = {1999},
  pages     = {1128-1146},
  ee        = {http://dx.doi.org/10.1007/3-540-48118-4_10},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Corbineau:CoqDecl,
  author    = {Pierre Corbineau},
  title     = {A Declarative Language for the {Coq} Proof Assistant},
  booktitle = {TYPES},
  year      = {2007},
  pages     = {69-84},
  ee        = {http://dx.doi.org/10.1007/978-3-540-68103-8_5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Wiedijk:Sketches,
  author    = {Freek Wiedijk},
  title     = {Formal Proof Sketches},
  booktitle = {TYPES},
  year      = {2003},
  pages     = {378-393},
  ee        = {http://dx.doi.org/10.1007/978-3-540-24849-1_24},
  crossref  = {DBLP:conf/types/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DijkstraScholten:Book,
  author    = {Edsger W. Dijkstra and
               Carel S. Scholten},
  title     = {Predicate calculus and program semantics},
  publisher = {Springer},
  series    = {Texts and monographs in computer science},
  year      = {1990},
  isbn      = {978-3-540-96957-0},
  pages     = {I-X, 1-220},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Rudnicki:Mizar,
    author = {Piotr Rudnicki},
    title = {An Overview of the {MIZAR} Project},
    booktitle = {University of Technology, Bastad},
    year = {1992},
    pages = {311--332},
    publisher = {}
}

@inproceedings{ORS:PVS,
    AUTHOR = {S. Owre and J. M. Rushby and N. Shankar},
    TITLE = {{PVS:} {A} Prototype Verification System},
    BOOKTITLE = {CADE-11},
    YEAR = {1992},
    SERIES = lnai,
    VOLUME = {607},
    PAGES = {748--752},
    PUBLISHER = {Springer},
    URL = {http://www.csl.sri.com/papers/cade92-pvs/}
}
    BOOKTITLE = {11th International Conference on Automated Deduction (CADE)},
    EDITOR = {Deepak Kapur},

@article{Robinson:Window,
  author    = {Peter J. Robinson and
               John Staples},
  title     = {Formalizing a Hierarchical Structure of Practical Mathematical
               Reasoning},
  journal   = {J. Log. Comput.},
  volume    = {3},
  number    = {1},
  year      = {1993},
  pages     = {47-61},
  ee        = {http://dx.doi.org/10.1093/logcom/3.1.47},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Grundy:WindowHOL,
  author    = {Jim Grundy},
  title     = {Transformational Hierarchical Reasoning},
  journal   = {Comput. J.},
  volume    = {39},
  number    = {4},
  year      = {1996},
  pages     = {291-302},
  ee        = {http://dx.doi.org/10.1093/comjnl/39.4.291},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BN:Sledgehammer,
  author    = {Sascha B{\"o}hme and
               Tobias Nipkow},
  title     = {Sledgehammer: Judgement Day},
  booktitle = {IJCAR},
  year      = {2010},
  pages     = {107-121},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14203-1_9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Armand:CoqSMT,
  author    = {Micha{\"e}l Armand and
               Germain Faure and
               Benjamin Gr{\'e}goire and
               Chantal Keller and
               Laurent Th{\'e}ry and
               Benjamin Werner},
  title     = {A Modular Integration of {SAT}/{SMT} Solvers to {Coq} through
               Proof Witnesses},
  booktitle = {CPP},
  year      = {2011},
  pages     = {135-150},
  ee        = {http://dx.doi.org/10.1007/978-3-642-25379-9_12},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Besson:CoqSMTReflexive,
  author    = {Fr{\'e}d{\'e}ric Besson and
               Pierre-Emmanuel Cornilleau and
               David Pichardie},
  title     = {Modular SMT Proofs for Fast Reflexive Checking Inside Coq},
  booktitle = {CPP},
  year      = {2011},
  pages     = {151-166},
  ee        = {http://dx.doi.org/10.1007/978-3-642-25379-9_13},
  crossref  = {DBLP:conf/cpp/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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{boogie11why3,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
  title = {{Why3}: Shepherd Your Herd of Provers},
  booktitle = {BOOGIE 2011: Workshop on Intermediate Verification Languages},
  year = 2011,
  pages = {53--64},
  url = {http://proval.lri.fr/publications/boogie11final.pdf},
}
  booktitle = {BOOGIE 2011: First International Workshop on Intermediate Verification Languages},
  month = aug,
  
@InProceedings{zeno,
  author = 	 {William Sonnex and Sophia Drossopoulou and Susan Eisenbach},
  title = 	 {Zeno: An Automated Prover for Properties of Recursive
                  Data Structures},
  booktitle =	 {TACAS},
  volume =	 {7214},
  series =	 lncs,
  year =	 {2012},
  publisher =	 {Springer},
  pages =	 {407-421},
}
  booktitle =	 {Tools and Algorithms for the Construction and Analysis of
                  Systems --- 18th International Conference, TACAS 2012},
  editor =	 {Cormac Flanagan and Barbara K{\"o}nig},
  month =	 mar # "--" # apr,

@InProceedings{Chisholm:CalculationByComputer,
  author = 	 {P. Chisholm},
  title = 	 {Calculation by computer},
  booktitle =	 {Third International Workshop on Software Engineering and its Applications},
  address =	 {Toulouse, France},
  year =	 {1990},
  month =	 dec,
  pages =	 {713-728},
}

@TechReport{VanDeSnepscheut:Proxac,
  author = 	 {van de Snepscheut, Jan L. A.},
  title = 	 {Proxac: an editor for program transformation},
  institution =  {Caltech},
  year = 	 {1993},
  number =	 {CS-TR-93-33},
}

@InProceedings{VanGasterenBijlsma:CalcExtension,
  author = 	 {A. J. M. van Gasteren and A. Bijlsma},
  title = 	 {An extension of the program derivation format},
  booktitle =	 {PROCOMET '98},
  pages =	 {167-185},
  year =	 {1998},
  publisher =	 {IFIP Conference Proceedings},
}
  booktitle =	 {Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on
                  Programming Concepts and Methods (PROCOMET '98)},
  editor =	 {David Gries and Willem P. de Roever},
  month =	 jun,