From 22ff08b38616ceef336f5f974d4edc4d37d955e8 Mon Sep 17 00:00:00 2001 From: blazy Date: Fri, 3 Aug 2007 17:04:06 +0000 Subject: Version longue et mise a jour du papier sur le front-end (premier jet). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- papers/cfrontend_new/blazy.bib | 1033 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1033 insertions(+) create mode 100755 papers/cfrontend_new/blazy.bib (limited to 'papers/cfrontend_new/blazy.bib') diff --git a/papers/cfrontend_new/blazy.bib b/papers/cfrontend_new/blazy.bib new file mode 100755 index 00000000..d51242c0 --- /dev/null +++ b/papers/cfrontend_new/blazy.bib @@ -0,0 +1,1033 @@ +@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" +} + -- cgit