diff options
Diffstat (limited to 'Docs/DafnyRef/poc.bib')
| -rw-r--r-- | Docs/DafnyRef/poc.bib | 523 |
1 files changed, 523 insertions, 0 deletions
diff --git a/Docs/DafnyRef/poc.bib b/Docs/DafnyRef/poc.bib new file mode 100644 index 00000000..a0f1ed79 --- /dev/null +++ b/Docs/DafnyRef/poc.bib @@ -0,0 +1,523 @@ +@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,
+
|