diff options
Diffstat (limited to 'papers/cfrontend_new/blazy.bib')
| -rwxr-xr-x | papers/cfrontend_new/blazy.bib | 1033 |
1 files changed, 0 insertions, 1033 deletions
diff --git a/papers/cfrontend_new/blazy.bib b/papers/cfrontend_new/blazy.bib deleted file mode 100755 index d51242c0..00000000 --- a/papers/cfrontend_new/blazy.bib +++ /dev/null @@ -1,1033 +0,0 @@ -@String{CSM = {Proc. of the Conf. on Soft. Maintenance (CSM)}} -@String{PLDI = {Proc. of the Programming Languages Design and Implementation Conf. (PLDI)}} -@String{POPL = {Proc. of Principles Of Progamming Languages symposium (POPL)}} -@String{LNCS = {Lecture Notes in Computer Science}} -@String{TOPLAS = {ACM Transactions on Programing Languages and Systems}} -@String{SV = {Springer-Verlag}} -@String{JUCS = "Journal of Universal Computer Science"} - -@Book{B:book, - AUTHOR = "J.R. Abrial", - TITLE = "The B-Book assigning programs to meanings", - PUBLISHER="Cambridge University Press", - YEAR = "1996"} - -@Book{compil:book, - AUTHOR = "A.V. Aho and R.Sethi and J.D.Ullman", - TITLE = "Compilers: Principles, Techniques and Tools", - PUBLISHER="Addison-Wesley", - YEAR = "1988"} - -@phdthesis{C:andersen, - AUTHOR = "L.O. Andersen", - TITLE = "Program analysis and specialization for the C programming language", - YEAR="1994", - SCHOOL="University of Copenhagen", NOTE="DIKU report 94/19"} - -@InProceedings{ppc:appel, - author = {A.W. Appel}, - title = {Foundational Proof-Carrying Code}, - booktitle = {16th Annual IEEE Symp. on Logic in Computer Science (LICS)}, - year = {2001}, - month = {June}, - address = {Washington, DC, United States}, - pages = {247} -} - -@INPROCEEDINGS{pepm:glueck, - AUTHOR="R. Baier and R. Gl{\"u}ck and R. Z{\"o}chling", - TITLE="Partial evaluation of numerical programs in {F}ortran", - PAGES="119-132", - BOOKTITLE = "Proc. of the Partial Evaluation and semantics based Program Manipulation Workshop", - ORGANIZATION="ACM SIGPLAN", - ADDRESS="Melbourne", YEAR="1994"} - -@ARTICLE{slicing:berg, - AUTHOR="J.A. Bergstra and T.B. Dinesh and J. Field and J. Heering", - TITLE="Toward a complete transformational toolkit for compilers", - PAGES="639-684", - JOURNAL = TOPLAS, - VOLUME="19", NUMBER="5", - MONTH = "September", YEAR="1997"} - -@Book{CoqArt, - author = "Y. Bertot and P. Castéran", - title = {Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions}, - publisher = {Springer Verlag}, - year = {2004}, -} - -@TechReport{bertot:compilo, - author = {Y. Bertot}, - title = {A certified compiler for an imperative langage}, - institution = {INRIA}, - year = {1998}, - number = {RR-3488} -} - -@inproceedings{coq:bertot95, - author = "Y. Bertot and R. Fraer", - title = "Reasoning with Executable Specifications", - booktitle = "{TAPSOFT '95}: Theory and Practice of Software Development", - series = LNCS, volume = "915", - publisher = "Springer-Verlag", - editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach", - pages = "531--45", - ADDRESS = "Aarhus", MONTH = "May", year = "1995"} - -@PhdThesis{these:sb, - author = {S.Blazy}, - title = {La spécialisation de programmes pour l'aide à la maintenance du logiciel}, - school = {CNAM}, - year = {1993}, - month = {December} -} - -@INPROCEEDINGS{washington:sb, - AUTHOR = "S. Blazy and P. Facon", - TITLE = "{SFAC}, a tool for program comprehension by specialization", - BOOKTITLE = "Proc. of the Third Workshop on Program Comprehension", - ORGANIZATION = "IEEE", - PAGES = "162-167", - ADDRESS = "Washington D.C.", MONTH = "November", YEAR = {1994} } - -@INPROCEEDINGS{tapsoft:sb, - AUTHOR = "S. Blazy and P. Facon", - TITLE = "Formal specification and prototyping of a program specializer", - BOOKTITLE = "{TAPSOFT '95}: Theory and Practice of Software Development", - PAGES = "666-680", - SERIES = LNCS, VOLUME = "915", - publisher = "Springer-Verlag", - editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach", - ADDRESS = "Aarhus", MONTH = "May", YEAR = {1995} } - -@INPROCEEDINGS{pe1996:sb, - AUTHOR = "S. Blazy and P. Facon", - TITLE = "An automatic interprocedural analysis for the understanding of scientific application - Programs", - PAGES = "1-16", - crossref={pe1996:tout} } - -@ARTICLE{sope:sb, - AUTHOR = "S. Blazy and P. Facon", - TITLE = "Partial evaluation for program understanding", - crossref={sope:tout} } - -@INPROCEEDINGS{ase:sb, - AUTHOR = "S. Blazy and P. Facon", - TITLE = "Application of formal methods to the development of a software maintenance tool", - BOOKTITLE = "Proc. of the Automated Software Engineering Conference", - PAGES = "162-171", - ORGANIZATION = "IEEE", - MONTH = "November", YEAR = {1997} } - -@article{sekejal:sb, - AUTHOR = "S. Blazy", - TITLE = "Partial Evaluation for the understanding of {F}ortran programs", - journal = "Journal of Software Engineering and Knowledge Engineering", - VOLUME = "4", NUMBER = "4", - PAGES = "535-559", - YEAR = {1994} } - -@article{asejal:sb, - AUTHOR = "S. Blazy", - TITLE = "Specifying and Automatically Generating a Specialization Tool for {F}ortran 90", - journal = "Journal of Automated Software Engineering", - VOLUME = "7", NUMBER = "4", - PAGES = "345-376", - MONTH = "December", YEAR = {2000} } - -@techreport{cedric02:sb, - title = "Transformations certifiées de programmes impératifs", - author = "S. Blazy", - type = "Technical report", - institution = "CEDRIC", - number = "398", - month = "December", - year = "2002", -} - -@INPROCEEDINGS{icfem:sb, - AUTHOR = "S. Blazy and X. Leroy", - TITLE = "Formal verification of a memory model for - {C}-like imperative languages", - BOOKTITLE = "Proc. of Int. Conf. on Formal Engineering Methods {ICFEM}", - PAGES = {280--299}, - SERIES = LNCS, VOLUME = 3785 , - publisher = "Springer-Verlag", - ADDRESS = "Manchester, UK", - MONTH = "November", - YEAR = {2005} -} - -@inproceedings{blazy06:fm, - author = {Sandrine Blazy and Zaynah Dargaye and - Xavier Leroy}, - title = {Formal Verification of a {C} Compiler Front-End}, - booktitle = {Symp. on Formal Methods (FM'06)}, - SERIES = {Lecture Notes in Computer Science}, - VOLUME = 4805, - year = {2006}, - pages = {460-475}, - ee = {http://dx.doi.org/10.1007/11813040_31}} - - -@InProceedings{table:ob, - author = {O. Boite and C. Dubois}, - title = {Proving {T}ype {S}oundness of a {S}imply {T}yped {ML}-like {L}anguage with {R}eferences}, - year = 2001, - Booktitle = {Supplemental Proc. of TPHOL'01, Informatics - Research Report EDI-INF-RR-0046 of University of Edinburgh}, - Editor = {R. Boulton and P. Jackson}, - pages = {69--84} -} - -@INPROCEEDINGS{coq:dataflow, - AUTHOR = {D. Cachera and T. Jensen and D. Pichardie and V. Rusu}, - TITLE = {{Extracting a Data Flow Analyser in Constructive Logic}}, - BOOKTITLE = {Proc.\ of 13th European Symp. on Programming (ESOP'04)}, - YEAR = {2004}, - PAGES = {385--400}, - NUMBER = {2986}, - SERIES = LNCS, - PUBLISHER = SV} -} - -@INPROCEEDINGS{pldi:carini, - AUTHOR = "R. Carini and M. Hind", - TITLE = "Flow-sensitive interprocedural constant propagation", - BOOKTITLE = PLDI, - ORGANIZATION="ACM SIGPLAN", - PAGES = "23-31", - ADDRESS = "La Jolla", - MONTH = "June", YEAR = {1995} } - -@misc{cavalcanti-procedures, - author = "Ana Cavalcanti and Augusto Sampaio and Jim Woodcock", - title = "Procedures, Parameters, And Substitution In The Refinement Calculus", - url = "citeseer.nj.nec.com/cavalcanti97procedures.html" } - -@MANUAL{Centaur, - TITLE = "Centaur 1.2 documentation", - ORGANIZATION = "INRIA", - YEAR = "1994" } - -@Misc{Coq, - title = {The {C}oq proof assistant}, - note = "http://coq.inria.fr" -} - -@INPROCEEDINGS{pldi:chase, - AUTHOR = "D.R. Chase and F.K. Zadeck", - TITLE = "Analysis of pointers and structures", - BOOKTITLE = PLDI, - ORGANIZATION="ACM SIGPLAN", - PAGES = "296-31", - ADDRESS = "White Plains", - MONTH = "June", YEAR = {1990} } - -@PhdThesis{chrzaszcz04phd, - author = {J. Chrz{\k a}szcz}, - title = {Modules in Type Theory with Generative Definitions}, - school = {Warsaw Univerity and University of Paris-Sud}, - year = 2004, - month = {January} -} - -@article{pe:conselproof, - author = "C. Consel and S.-C. Khoo", - title = "On-Line Off-Line Partial Evaluation: Semantic Specifications and Correctness Proofs", - journal = "Journal of Functional Programming", - volume = "5", - number = "4", - pages = "461-500", - year = "1995" } - -@InProceedings{pe:tutorial, - author = {C.Consel and O.Danvy}, - title = {Tutorial notes on partial evaluation}, - booktitle = POPL, - pages = {493-501}, - year = {1993}, -} - -@InProceedings{coq:courtieu, - author = {P. Courtieu}, - title = {Normalized types}, - booktitle = {CSL}, - year = {2001}, -} - -@INPROCEEDINGS{preuve:despeyroux, - AUTHOR = "J. Despeyroux", - TITLE = "Proof of translation in natural semantics", - BOOKTITLE = "Proc. of the Symposium on Logic in Computer Science", - ADDRESS = "Cambridge, USA", - MONTH = "June", YEAR = {1986} } - -@mastersthesis{stage:pointeurs, - AUTHOR = "N. Dubois and P. Sayarath", - TITLE = "Aide {\`{a}} la {compr\'{e}hension} et {\`{a}} la maintenance: - pointeurs pour la {sp\'{e}cialisation} de programmes", - MONTH = "June", YEAR="1996", - SCHOOL="IIE-CNAM", NOTE="in French"} - -@INPROCEEDINGS{pldi:emami, - AUTHOR = "M. Emami and R. Ghiya and L.J. Hendren", - TITLE = "Context-sensitive interprocedural points-to analysis in the presence of function pointers", - BOOKTITLE = PLDI, - ORGANIZATION="ACM SIGPLAN", - PAGES = "242-256", - MONTH = "June", YEAR = {1994} } - -@techreport {cite110, - title = "Modelling program compilation in the refinement calculus", - author = "C. J. Fidge", - type = "Technical report", - institution = "Software Verification Research Centre", - address = "School of Information Technology, - The University of Queensland, Brisbane 4072. Australia", - number = "97-22", - month = may, - year = "1997", - keywords = "refinement, compilers.", - abstract = "This report shows how compilation of high-level language -programs to assembler code can be formally represented in the -refinement calculus. New operators are introduced to widen the -modelling language to encompass assembler code. A compilation -strategy is then embodied as a set of derived refinement rules.", - url = "http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-22" -} - -@INPROCEEDINGS{slicing:field, - AUTHOR = "J. Field and G. Ramalingam and F. Tip", - TITLE = "Parametric program slicing", - BOOKTITLE = POPL, - ADDRESS = "San Francisco, USA", - PAGES = "379-392", - YEAR = {1995} } - -@InProceedings{fsets, - author = {J.-C. Filli{\^a}tre and P. Letouzey}, - title = {Functors for Proofs and Programs}, - booktitle = {{European Symposium on Programing, (ESOP)}}, - volume = 2986, - publisher = {Springer-Verlag}, - series = LNCS, - year = {2004}, - address = {Barcelona, Spain}, - month = {April}, -} - -@INPROCEEDINGS{caduceus, - AUTHOR = {J.-C. Filli\^atre and C. March\'e}, - TITLE = {{Multi-Prover Verification of C Programs}}, - BOOKTITLE = {6th Int. Conf. on Formal Engineering Methods (ICFEM)}, - YEAR = 2004, - ADDRESS = {Seattle}, - MONTH = {November}, - PUBLISHER = SV, - SERIES = LNCS, - VOLUME = 3308, - PAGES = {15--29} -} - -@INCOLLECTION{frazer:reverse, - AUTHOR = "A. Frazer", - TITLE = "Reverse engineering", - BOOKTITLE = "Software reuse and reverse engineering in practice", - PUBLISHER = "P.A.V. Hall", - YEAR = "1992", - PAGES = "209-243" } - -@ARTICLE{slicing:gallagher, - AUTHOR = "K. Gallagher and J.R. Lyle", - TITLE = "Using program slicing in software mainetnance", - JOURNAL = {ACM Trans. Soft. Eng.}, - VOLUME = {17}, NUMBER = {8}, - PAGES = "751-761", - YEAR = {1991} } - -@Article{Glesner:2003, - author = "S. Glesner", - title = "{Using Program Checking to Ensure the Correctness of Compiler Implementations}", - journal = JUCS, - year = "2003", - volume = "9", - number = "3", - pages = "191--222", - month = {March}} - -@inproceedings{verifix, - author = {G. Goos and W. Zimmermann}, - title = {Verification of Compilers}, - booktitle = {Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel)}, - year = {1999}, - pages = {201--230}, - publisher = SV, - address = {London, UK} - } - -@article{fpcc:coq, - author = {N. Hamid and Z. Shao and V. Trifonov and S. Monnier and Z. Ni}, - title = {A Syntactic Approach to Foundational Proof-Carrying Code}, - journal= {Journal of Automated Reasoning}, - volume = 31, - number={3-4}, - year= {2003}, - month= {September}, - pages= "191-229" -} - -@ARTICLE{natsem:hannan, - AUTHOR="J. Hannan", - TITLE="Extended natural semantics", - PAGES="123-152", - JOURNAL = "Journal of functional programming", - VOLUME="3", NUMBER="2", - MONTH = "April", YEAR="1993"} - -@INPROCEEDINGS{pe:haraldsson, - AUTHOR = "A. Haraldsson", - TITLE = "A partial evaluator and its Use for compiling iterative statements in Lisp", - BOOKTITLE = POPL, - ADDRESS = "Tucson", - YEAR = {1978} } - -@INPROCEEDINGS{pldi:horwitz, - AUTHOR = "R. Hasti and S. Horwitz", - TITLE = "Using static single assignment form to improve flow-insensitive pointer analysis", - BOOKTITLE = PLDI, - ORGANIZATION="ACM SIGPLAN", - PAGES = "97-105", - ADDRESS = "Montreal", - MONTH = "June", YEAR = {1998} } - -@inproceedings{pe:hatcliff95, - author = "J. Hatcliff", - title = "Mechanically Verifying the Correctness of an Offline Partial Evaluator", - booktitle = "Proc. of the 7th Int. Symp. on Programming Languages: Implementations, Logics and Programs", - month = "September", - series = LNCS, volume = "982", - publisher = "Springer-Verlag", - address = "Utrecht, The Netherlands", - editor = "M. Hermenegildo and S.D. Swierstra", - pages = "279--298", - year = "1995"} - -@article{hatcliff97computational, - author = "John Hatcliff and Olivier Danvy", - title = "A Computational Formalization for Partial Evaluation", - journal = "Mathematical Structures in Computer Science", - volume = "7", - number = "5", - pages = "507-541", - year = "1997"} - - -@Article{hoare:verif, - author = {T. Hoare}, - title = {The Verifying Compiler: a Grand Challenge for Computing Research}, - journal = {Journal of the ACM}, - year = {2003}, - volume = {50}, - number = {1}, - pages = {63-69}, - month = {January}, -} - -@article{jifeng93specification, - author = "{H. Jifeng} and J. P. Bowen", - title = "Specification, Verification and Prototyping of an Optimized Compiler", - journal = "Formal Aspects of Computing", - volume = "6", - number = "6", - pages = "643-658", - year = "1993" } - -@Book{VDM:book, - AUTHOR = "C.B. Jones", - TITLE = "Systematic development using VDM", - PUBLISHER="Prentice-Hall", - YEAR = "1990"} - -@Book{pe:book, - AUTHOR = "N.D. Jones and C.K. Gomard and P. Sestoft", - TITLE = "Partial evaluation and automatic program generation", - PUBLISHER="Prentice-Hall", - YEAR = "1993"} - -@inproceedings{natsem:kahn, - AUTHOR = "G.Kahn", - booktitle = {{Proc. of the Symp. on Theoretical Aspects of Comp. Science}}, - pages = {237-257}, - publisher = "Springer-Verlag", - SERIES = LNCS, VOLUME = "247", - title = {{Natural Semantics}}, - year = {1987} -} - -@INPROCEEDINGS{pldi:landi, - AUTHOR = "W. Landi and B.G. Ryder", - TITLE = "A safe approximate algorithm for interprocedural pointer aliasing", - BOOKTITLE = PLDI, - PAGES = "235-248", - ORGANIZATION="ACM SIGPLAN", - MONTH = "June", YEAR = {1992} } - -@inproceedings{lawall:sound, - author = "J. Lawall and P. Thiemann", - title = "Sound Specialization in the Presence of Computational Effects", - booktitle = "Theoretical Aspects of Computer Software", - series = LNCS, volume = "1281", - publisher = "Springer-Verlag", - pages = "165--190", - month = "September", - address = {Sendai, Japan}, - year = "1997"} - -@inproceedings{paul:sefm, - author= {D. Leinenbach and W. Paul and E. Petrova}, - title= {Towards the Formal Verification of a {C}0 Compiler}, - booktitle= {Proc. Conf. on Software Engineering and Formal Methods (SEFM)}, - month={September}, - year= 2005, - address= {Koblenz, Germany} -} - -@INPROCEEDINGS{rhodium:popl, - AUTHOR = "S.Lerner and T. Millstein and E. Rice and C. Chambers", - TITLE = "Automated soundness proofs for dataflow analyses and transformations", - BOOKTITLE = POPL, - ADDRESS = "Long Beach, United States", - YEAR = {2005} } - -@InProceedings{xl:jfla, - author = {X. Leroy}, - title = {Certification d'un Compilateur: Enjeux, Problèmes et Approches}, - booktitle = {Journées Francophones des Langages Applicatifs (JFLA)}, - year = {2004}, - month = {January}, - organization = {INRIA}, - note = {invited talk} -} - -@InProceedings{xl:popl, - author = {X. Leroy}, - title = {Formal certification of a compiler back-end, or: programming a compiler - with a proof assistant}, - booktitle = POPL, - year = {2006}, - month = "January", - address = {Charleston, USA}, - pages = "42--54", - publisher = "ACM Press" -} - -@TechReport{xl:cminor, - author = {X. Leroy}, - title = {Le langage Intermédiaire {C} minor}, - institution = {Concert technical report}, - year = {2003}, - month = {February}, -} - -@misc{xl:compcert-backend, - author = {X. Leroy}, - title = {The {Compcert} certified compiler back-end -- - commented {Coq} development}, - howpublished = {Available on-line at \citeurl{http://cristal.inria.fr/~xleroy/compcert-backend/}}, - year = {2006} -} - -@INPROCEEDINGS{fse:liang, - AUTHOR = "D. Liang and M.J. Harrold", - TITLE = "Efficient points-to analysis for whole-program analysis", - BOOKTITLE = "Proc. of ESEC/FSE joint Conf.", - ADDRESS = "Toulouse, France", - PAGES = "199-215", - SERIES = LNCS, VOLUME = "1687", - ORGANIZATION="ACM SIGSOFT", - MONTH = "September", YEAR = {1999} } - -@phdthesis{letouzey04, - author = "P. Letouzey", - month = "July", - school = "Universit{\'e} Paris-Sud", - title = "Programmation fonctionnelle certifi{\'e}e -- L'extraction de programmes dans l'assistant {Coq}", - year = "2004" -} - -@InProceedings{nipkow:pt, - author = {F. Mehta and T. Nipkow}, - title = {Proving pointer programs in higher-order logic}, - booktitle="Automated Deduction --- CADE-19", - editor="F. Baader", - year=2003, - publisher=SV, - series=LNCS, - volume={2741}, - pages={121--135}} - -} - -@InProceedings{seplog:ref, - author = {I. Mijajlovic and N. Torp-Smith}, - title = {Refinement in Separation Context}, - booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, - year = {2004}, - address = {Venice, Italy}, - month = {January}, -} - -@InProceedings{space:region, - author = {S.Monnier}, - title = {Typed regions}, - booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, - year = {2004}, - address = {Venice, Italy}, - month = {January}, -} - -@Book{muchnik:book, - AUTHOR = "S.S. Muchnick", - TITLE = "Advanced compiler-design and implementation", - PUBLISHER="Morgan Kaufmann", - YEAR = "1997"} - - - -@InProceedings{pcc:necula, - author = {G. Necula}, - title = {Proof Carrying Code}, - booktitle = POPL, - year = {1997}, - month = {January}, -} - -@InProceedings{tv:necula, - author = "G. Necula", - title = "Translation Validation for an Optimizing Compiler", - booktitle = "{ACM} {SIG\-PLAN} Conf. on Programming Language - Design and Implementation (PLDI)", - pages = "83--95", - year = "2000" -} - -@inproceedings{russes:C, - author = {V.A. Nepomniaschy and I.S. Anureev and A.V. Promsky}, - title = {Verification-Oriented Language {C}-Light and Its Structural - Operational Semantics.}, - booktitle = {Ershov Memorial Conference}, - year = {2003}, - pages = {103-111}, -} - -@inproceedings{tv:pnueli, - author = {A. Pnueli and M. Siegel and E. Singerman}, - title = {Translation Validation}, - booktitle = {Proc. of the 4th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS)}, - year = {1998}, - pages = {151--166}, - publisher = SV, - address = {London, UK} - } - -@inproceedings{cocv:pnueli, - author = {Y. Hu and C. Barrett and B. Goldberg and A. Pnueli}, - title = {Validating More Loop Optimizations}, - booktitle = {Workshop on Compiler Optimization Meets Compiler Verification (COCV)}, - year = {2005}, - address = {Edinburgh, UK} - } - - -@Book{nielson:book, - AUTHOR = "H.R. Nielson and F. Nielson", - TITLE = "Semantics with application - A formal introduction", - PUBLISHER="John Wiley and Sons", - YEAR = "1992"} - -@Book{intabs:book, - AUTHOR = "F. Nielson and H.R. Nielson and C. Hankin", - TITLE = "Principles of Program Analysis", - PUBLISHER="Springer-Verlag", - YEAR = "1999"} - -@INPROCEEDINGS{ase:consel, - AUTHOR = "R. Marlet and S. Thibault and C. Consel", - TITLE = "Mapping software architectures to efficient implementation via partial evaluation", - BOOKTITLE = "Proc. of the Automated Software Engineering Conference", - PAGES = "183-192", - ORGANIZATION = "IEEE", - MONTH = "November", YEAR = {1997} } - -@InProceedings{cil, - author = {G. Necula and S. McPeak and S.P. Rahul and W. Weimer}, - title = {CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs}, - booktitle = {Conf. on Compiler Construction (CC'02)}, - address = {Grenoble, France}, - year = {2002}, - month = {March}, -} - -@article{borger:C, - author = "{E. B{\"o}rger} and N.G. Fruja and V.Gervasi and R.F. St{\"a}rk", - title = "A high-level modular definition of the semantics of {C\#}", - journal = "Theoretical Computer Science", - volume = "336", - number = "2-3", - pages = "235-284", - year = "2005" } - -@InProceedings{gurevich:C, - author = "Y. Gurevich and J.K. Huggins", - title = "The Semantics of the {C} Programming Language", - booktitle = "Proc. of CSL'92 (Computer Science Logic)", - publisher = "Springer Verlag", - SERIES = LNCS, VOLUME = "702", - year = 1993, - pages = "274-308", -} - -@techreport{KleinN-Toplas, - author = {Gerwin Klein and Tobias Nipkow}, - title = {A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler}, - number = {0400001T.1}, - institution= {National ICT Australia}, - month=mar, - year=2004, - note = "To appear in ACM TOPLAS"} -} - -@PhdThesis{Norrish:phd, - author = "M. Norrish", - title = "{C} formalised in HOL", - school = "University of Cambridge", - year = 1998, - month = "December" -} - - -@misc{norvell94machine, - author = "T. Norvell", - title = "Machine code programs are predicates too", - text = "Theodore S. Norvell. Machine code programs are predicates too. In David - Till, editor, Sixth Refinement Workshop, Workshops in Computing, pages 188--204. - Springer Verlag, 1994.", - year = "1994"} - -@article{palsberg93correctness, - author = "J. Palsberg", - title = "Correctness of Binding-Time Analysis", - journal = "Journal of Functional Programming", - volume = "3", - number = "3", - pages = "347-363", - year = "1993"} - -@PhdThesis{papaspyrou-1998-fscpl, - author = "N.S. Papaspyrou", - title = "A formal semantics for the {C} programming language", - school = "National Technical University of Athens", - year = 1998, - month = "February" -} - -@TechReport{strecker05:_compil_verif_c0, - author = {Martin Strecker}, - title = {Compiler Verification for {C0}}, - institution = {Universit{\'e} Paul Sabatier}, - year = 2005, - address = {Toulouse}, - month = {April} -} - -@inproceedings{rival:popl, - author = {X. Rival}, - title = {Symbolic transfer function-based approaches to certified compilation}, - booktitle = POPL, - year = {2004}, - pages = {1--13}, - location = {Venice, Italy}, - publisher = {ACM Press}, - } - -@manual{f90, - author = "S. Ramsden and F. Lin and M.A. Pettipher and G.S. Noland and J.M. Brooke", - title="{Fortran} 90: a conversion course for {F}ortran 77 programmers", - organization="Manchester and north {HC} {T\&EC}", - edition="Third", - year="1995" -} - -@Misc{coq:renard, - author = {C. Renard}, - title = {Un peu d'extensionnalité en {C}oq}, - note = {Université Paris VI}, - year = {2001}, - howpublished = {Mémoire de DEA}, - month = {September} -} - -@INPROCEEDINGS{rinard:compil, - AUTHOR ="M. Rinard and D. Marinov", - TITLE = "Credible compilation with pointers", - BOOKTITLE = "Workshop on Run-Time Result Verification (RTRV)", - address = {Trento, Italy}, - MONTH = "July", - YEAR = {1999} } - -@manual{f90:norme, - title="Programming language {Fortran 90}", - organization="ANSI", - address="New York", - year="1992", - note="ANSI X3.198-1992 and ISO/IEC 1539-1991(E)" -} - -@INPROCEEDINGS{ptr:sagiv, - AUTHOR = "M. Sagiv and T. Reps and R. Wilhelm", - TITLE = "Solving shape-analysis problems in languages with destructive updating", - BOOKTITLE = POPL, - MONTH = "January", YEAR = {1997} } - - - -@Book{sampaio:compil, - author = {A.Sampaio}, - title = {An algebraic approach to compiler design}, - publisher = {World Scientific}, - year = {1997}, - volume = {4}, - OPTnumber = {}, - series = {AMAST series in computing}, - OPTaddress = {}, - OPTedition = {}, - OPTmonth = {}, - OPTnote = {}, - OPTannote = {} -} - -@inproceedings{mem:crf, - author = {X. Shen and Arvind and L. Rudolph}, - title = {Commit-reconcile \& fences ({CRF}): a new memory model for architects and compiler writers}, - booktitle = {ISCA '99: Proc. of the 26th symposium on Computer architecture}, - year = {1999}, - pages = {150--161}, - location = {Atlanta, Georgia, United States}, - address = {Washington, DC, United States}, - } - -@INPROCEEDINGS{ptr:steens, - AUTHOR = "B. Steensgaard", - TITLE = "Points-to analysis in almost linear time", - BOOKTITLE = POPL, - PAGES = "32-41", - YEAR = {1996} } - -@inproceedings{coq:terrasse, - author = "D. Terrasse", - title = "Encoding Natural Semantics in {Coq}", - booktitle = "Proc. of the 4th Conf. on Algebraic Methodology and Software Technology", - publisher = SV, - SERIES = LNCS, VOLUME = "936", - address = "Montreal, Canada", - editor = "V. S. Alagar", - pages = "230--244", - year = "1995" } - -@mastersthesis{stage:vassallo, - AUTHOR = "R. Vassallo", - TITLE = "Ergonomie et {\'{e}volution} d'un outil de {compr\'{e}hension} de programmes", - MONTH = "June", YEAR="1996", - SCHOOL="IIE-CNAM", NOTE="in French"} - -@Article{Wand93, - author = "M. Wand", - title = "Specifying the Correctness of Binding-Time Analysis", - journal = "Journal of Functional Programming", - year = "1993", - volume = "3", - number = "3", - pages = "365--387", - month = "July"} - -@INPROCEEDINGS{pldi:wilson, - AUTHOR = "R.P. Wilson and M.S. Lam", - TITLE = "Efficient context-sensitive pointer analysis for C programs", - BOOKTITLE = PLDI, - PAGES = "1-12", - ORGANIZATION="ACM SIGPLAN", - MONTH = "June", YEAR = {1995} } - -@Book{formal:winskel, - AUTHOR = "G. Winskel", - TITLE = "The formal semantics of programming languages - an introduction", - PUBLISHER="MIT Press", - YEAR = "1993"} - -@INPROCEEDINGS{alias:ryder, - AUTHOR = "S. Zhang and B. Ryder and W. Landi", - TITLE = "Program decomposition for pointer aliasing: a step toward practical analyses", - BOOKTITLE = "Proc. of the Symp. on Foundations of Soft. Eng.", - ADDRESS = "San Francisco", - MONTH = "October", YEAR = "1996", - PAGES = "81-92" } - -@PROCEEDINGS{pe1996:tout, - editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", - TITLE = "International seminar on partial evaluation", - ADDRESS = "Dagstuhl castle", - SERIES = LNCS, VOLUME = "1110", - publisher = SV, - MONTH = "February", YEAR = {1996} } - -@proceedings{sope:tout, - TITLE = "Symposium on partial evaluation", - SERIES = "ACM Computing Surveys", - ORGANIZATION = "ACM", - NUMBER = "4", - MONTH = "December", YEAR = {1998} } - -@TechReport{outil:2, - author = {M.G.J. van den Brand and P. Klint and C. Verhoef}, - title = {{R}everse engineering and system renovation: an annotated bibliography}, - institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup}, - number = {P9603}, - year = {1996}, - fileurl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/P9603.ps.Z}, - abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/abstracts/P9603.txt}, -} - -@TechReport{P9702, - author = {M.G.J. van den Brand and M.P.A. Sellink and C. Verhoef}, - title = {{R}eengineering {COBOL} {S}oftware {I}mplies {S}pecification of the - {U}nderlying {D}ialects}, - institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup}, - number = {P9702}, - year = {1997}, - fileurl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/P9702.ps.Z}, - abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/abstracts/P9702.txt}, - note = {Available by anonymous ftp from ftp.wins.uva.nl, - file pub/programming-research/reports/1997/P9702.ps.Z} -} - -@INPROCEEDINGS{outil:3, - author = {M.P.A. Sellink and C. Verhoef}, - title = {Scaffolding for Software Renovation}, - BOOKTITLE = CSM, - ORGANIZATION = "IEEE", - ADDRESS = "Z{\"u}rich", MONTH = "March", YEAR = "2000", -} - -@INPROCEEDINGS{outil:4, - author = {H. Yank and P. Luker and W.Chu}, - title = {Code understanding through program transformation for reusable component identification}, - BOOKTITLE = "Fifth Workshop on Program Comprehension Proceedings", - ORGANIZATION = "IEEE", - YEAR = "1997", -} - -@INPROCEEDINGS{outil:1, - author = {I. Baxter and A. Yahin and L. Moura and M. Sant'Anna and L. Bier}, - title = {Clone detection using abstract syntax trees}, - BOOKTITLE = CSM, - ORGANIZATION = "IEEE", - YEAR = "1998", -} - -@article{mem:sota, - AUTHOR = "R.D. Tennent and D.R. Ghica and ", - TITLE = "Abstract models of storage", - journal = "Higher-Order and Symbolic Computation", - volume = "13", - number = "1/2", - MONTH = "", YEAR = "2000", - PAGES = "119-129" } - - - -@INPROCEEDINGS{mem:bornat, - AUTHOR = "R. Bornat", - TITLE = "Proving pointer programs in {H}oare logic", - BOOKTITLE = "5th Conf. on Mathematics of Program Construction", - publisher = SV, - MONTH = "", YEAR = "2000", - PAGES = "102-126" } - -@PROCEEDINGS{space:tout, - TITLE = "Second workshop on semantics, program analysis, and computing environments for memory management", - ADDRESS = "Venice", - ORGANIZATION="ACM SIGPLAN", - MONTH = "January", YEAR = {2004} } - -@InProceedings{typebin:popl, - author = {Z. Shao and B.Saha and V. Trifonov and N. Papaspyrou}, - title = {A type system for certified binaries}, - booktitle = POPL, - year = {2002}, - address = {Portland, United States}, - month = {January}, - pages = "217-232" -} - -@InProceedings{shao:cac, - author = {D.Yu and Z. Shao}, - title = {Verification of safety properties for concurrent assembly code}, - booktitle = {Int. Conf. on Functional Programming (ICFP)}, - year = {2004}, - address = {Snowbird, United States}, - month = {September}, - pages = "175-188" -} - - @InProceedings{walker:space, - author = {D. Walker}, - title = {Stacks, heaps and regions: one logic to bind them}, - year = {2004}, -booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, - note = {invited talk}, - address = {Venice, Italy}, - month = {January}, -} - - - -@InProceedings{mem:watson, - author = {G.Watson}, - title = {Compilation of refinement for a practical language}, - booktitle = {Proc. of the 5th Int. Conf. on Formal Engineering Methods (ICFEM)}, - crossref = {icfem2003} -} - -@Misc{concert, - title = {ARC Concert}, - note = {http://www-sop.inria.fr/lemme/concert}, -} - - -@proceedings{icfem2003, - editor = {J. S. Dong and J. Woodcock}, - title = {Proc. of the 5th Int. Conf. on Formal Engineering Methods, ICFEM 2003}, - publisher = SV, - series = LNCS, - volume = {2885}, - address = {Singapore}, - year = {2003}, - month = {November} -} - -@article{dave:survey, - author = {Maulik A. Dave}, - title = {Compiler verification: a bibliography}, - journal = {SIGSOFT Softw. Eng. Notes}, - volume = {28}, - number = {6}, - year = {2003}, - pages = {2--2}, - urlpublisher = {http://doi.acm.org/10.1145/966221.966235}, - publisher = "ACM Press" -} - |