[BACK]Return to res.bib CVS log [TXT] [DIR] Up to [gforth] / res

Diff for /res/res.bib between versions 1.5 and 1.6

version 1.5, 2009/06/28 15:01:57 version 1.6, 2009/06/29 06:50:40
Line 1 Line 1
   
    @article{1328444,
    author = {Jean-Baptiste Tristan and Xavier Leroy},
    title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
    journal = {SIGPLAN Not.},
    volume = {43},
    number = {1},
    year = {2008},
    issn = {0362-1340},
    pages = {17--27},
    doi = {http://doi.acm.org/10.1145/1328897.1328444},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
   @inproceedings{KRS-pldi92,
      author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
      title = {Lazy Code Motion},
      booktitle = "Proc. ACM SIGPLAN Conf. on
                   Prog. Lang. Design and Impl.
                   $($PLDI'92$)$",
      series = {{ACM SIGPLAN} Not.},
      volume = {{\em 27},7}, 
      year = {1992},
      pages = {224 - 234}
    }
   
   @inproceedings{KRS-retrolcm04,
      author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
      title = {{\sc Retrospective}: Lazy Code Motion},
      booktitle = "``20 Years of the ACM SIGPLAN Conference on 
         Programming Language Design and
         Implementation (1979 - 1999): A Selection''",
      series = {{ACM SIGPLAN} Not.},
      volume = {{\em 39},4}, 
      year = {2004},
      pages = {460 - 461 \& 462 - 472}
    }
   
   @inproceedings{KRS-pldi94,
      author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
      title = {Partial Dead Code Elimination},
      booktitle = "Proc. ACM SIGPLAN Conf. on 
                   Prog. Lang. Design and Impl.
                   $($PLDI'94$)$",
      series = {{ACM SIGPLAN} Not.},
      volume = {{\em 29},6}, 
      year = {1994},
      pages = {147 - 158}
    }
   
   
   
   @inproceedings{RKS-popl00,
      author = {R\"uthing, O. and Knoop, J. and Steffen, B.},
      title = {Sparse Code Motion},
      booktitle = "Conf. Rec. 27th Annual 
                   Symp. on Principles of Prog. Lang.
                   $($POPL'00$)$",
      publisher = "ACM, NY",
      year = {2000},
      pages = {170 - 183},
   }
   
   @book{MMO-lncs1283,
      author = {M\"uller-Olm, M.},
      title = {Modular Compiler Verification},
      publisher = {LNCS 1283, Springer-V.},
      year = {1996},
   }
   
   @Misc{CompCert, 
     key =          {CompCert},
     author =       {Leroy, X.},
     title =        {The Compcert verified compiler}},
     howpublished = {\url{http://compcert.inria.fr/doc/index.html}},
     year =         {2005 - 2008},
     note =         {CompCert is funded by ANR (grant number ANR-05-SSIA-0019), 
                     as part of the ARA SSIA programme.}
   }
   
   @inproceedings{Le-popl06,
      author = {Leroy, X.},
      title = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant},
      booktitle = "Conf. Rec. 33rd Annual 
                   Symp. on Principles of Prog. Lang.
                   $($POPL'06$)$",
      publisher = "ACM, NY",
      year = {2006},
   }
   
   @InProceedings{BDL-fm06,
     author =       "Blazy, S. and Dargaye, Z. and Leroy, X.",
     title =        {Formal verification of a C compiler front-end},
     booktitle =    "{Formal Methods 2006}",
     year =         2006,
     volume =       4085,
     series =       {LNCS},
     publisher =    springer
   }
   
   @Article{Langmaack97a,
     Author        = {Langmaack, Hans},
     Title         = {{Softwareengineering zur Zertifizierung von
                     Systemen: Spezifikations-, Implementierungs-,
                     \"Ubersetzerkorrektheit}},
     Journal       = {Informationstechnik und Technische
                     Informatik it-ti},
     Pages         = {41-47},
     Number        = 3,
     Volume        = 97,
     Publisher     = {Oldenbourg Verlag},
     Year          = 1997,
   }
   
   @InProceedings{Goerigk-et-al:CC96,
     Author        = {W. Goerigk and A. Dold and T. Gaul and G. Goos and
                     A. Heberle and F. von Henke and U. Hoffmann and
                     H. Langmaack and H. Pfeifer and H. Ruess and W. Zimmermann},
     Title         = "{C}ompiler {C}orrectness and {I}mplementation
                     {V}erification: {T}he {V}erifix {A}pproach",
     BookTitle     = {Proceedings of the Poster Session of CC'96 -
                     International Conference on Compiler Construction },
     Editor        = {P. Fritzson},
     Publisher     = {ida},                  
     Year          = {1996},
     Note          = {TR-Nr.: R-96-12},
     Pages         = {65 -- 73},
   }
   
   
   @Article{Langmaack96a,
     Author        = {Langmaack, H.},
     Title         = {{The ProCoS Approach to Correct Systems}},
     Journal       = {Real Time Systems},
     Volume        = {13},
     Pages         = {253-275},
     Publisher     = {Kluwer Academic Publishers},
     Year          = 1997
   }
   
   
   @InProceedings{Goos:00:ASM,
     author =       "Gerhard Goos and
                     Wolf Zimmermann",
     title =        {Verifying Compilers and ASMs},
     booktitle =    "{Abstract State Machines, Theory and Applications}",
     year =         2000,
     pages =        {177-202},
     editor =       {Yuri Gurevich and Philipp W. Kutter and
                     Martin Odersky and Lothar Thiele},
     volume =       1912,
     series =       {LNCS},
     publisher =    springer
   }
   
   @InCollection{Goos:99:verifix,
     author =       {Gerhard Goos and Wolf Zimmermann},
     title =        {Verification of Compilers},
     booktitle =    {Correct System Design},
     pages =        {201-230},
     publisher =    {Springer-Verlag},
     year =         1999,
     editor =       {Bernhard Steffen and Ernst Rüdiger Olderog},
     volume =       1710,
     series =       {LNCS}
   }
   
   @book{Po-lncs124,
      author = {Polak, W.},
      title = {Compiler Specification and Verification.},
      publisher = {LNCS 124, Springer-V.},
      year = {1981},
   }
   
 @article{Hoare03,  @article{Hoare03,
  author = {Tony Hoare},   author = {Tony Hoare},
  title = {The verifying compiler: A grand challenge for computing research},   title = {The verifying compiler: A grand challenge for computing research},
Line 64 Line 239
  publisher = {ACM},   publisher = {ACM},
  address = {New York, NY, USA},   address = {New York, NY, USA},
  }   }
    
   @inproceedings{FNSG-tlfi07,
    author = {Feng, Xinyu and Ni, Zhaozhong and Shao, Zhong and Guo, Yu},
    title = {An open framework for foundational proof-carrying code},
    booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation},
    year = {2007},
    isbn = {1-59593-393-X},
    pages = {67--78},
    location = {Nice, Nice, France},
    doi = {http://doi.acm.org/10.1145/1190315.1190325},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
   @inproceedings{AF-popl00,
    author = {Appel, Andrew W. and Felty, Amy P.},
    title = {A semantic model of types and machine instructions for proof-carrying code},
    booktitle = {POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    year = {2000},
    isbn = {1-58113-125-9},
    pages = {243--253},
    location = {Boston, MA, USA},
    doi = {http://doi.acm.org/10.1145/325694.325727},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
 @inproceedings{ZaksPnueli08,  @inproceedings{ZaksPnueli08,
  author = {Anna Zaks and Amir Pnueli},   author = {Anna Zaks and Amir Pnueli},
Line 134 Line 335
 }  }
   
 @article{BlechPoetzsch07,  @article{BlechPoetzsch07,
   
  author = {Jan Olaf Blech and Arnd Poetzsch-Heffter},   author = {Jan Olaf Blech and Arnd Poetzsch-Heffter},
  title = {A Certifying Code Generation Phase},   title = {A Certifying Code Generation Phase},
  journal = {Electron. Notes Theor. Comput. Sci.},   journal = {Electron. Notes Theor. Comput. Sci.},
Line 160 Line 362
  address = {New York, NY, USA},   address = {New York, NY, USA},
  }   }
   
   @inproceedings{PSS-tacas98,
      author = {Pnueli, A. and Siegel, M. and Singermann, E.},
      title = {Translation Validation},
      booktitle = {Proc. 4th Int. Conf. on Tools and
         Algorithms for the Construction and Analysis of Systems
         $($TACAS'98$)$},  
      publisher = {Springer-V.},
      series = "LNCS 1384",
      year = {1998},
      pages = {151 - 166}
    }
   
   @inproceedings{Ne-popl97,
      author = {Necula, G. C.},
      title = {Proof-Carrying Code},
      booktitle = "Conf. Rec. 24th Annual 
                   Symp. on Principles of Prog. Lang.
                   $($POPL'97$)$",
      publisher = "ACM, NY",
      year = {1997},
      pages = {106 - 119},
   }
   
   @article{NL-pldi98,
    author = {Necula, George C. and Lee, Peter},
    title = {The design and implementation of a certifying compiler},
    journal = {SIGPLAN Not.},
    volume = {33},
    number = {5},
    year = {1998},
    issn = {0362-1340},
    pages = {333--344},
    doi = {http://doi.acm.org/10.1145/277652.277752},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
   @inproceedings{Colby-etal-pldi00,
    author = {Colby, Christopher and Lee, Peter and Necula, George C. and Blau, Fred and Plesko, Mark and Cline, Kenneth},
    title = {A certifying compiler for Java},
    booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
    year = {2000},
    isbn = {1-58113-199-2},
    pages = {95--107},
    location = {Vancouver, British Columbia, Canada},
    doi = {http://doi.acm.org/10.1145/349299.349315},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
   @inproceedings{Ne-pldi00,
    author = {Necula, George C.},
    title = {Translation validation for an optimizing compiler},
    booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
    year = {2000},
    isbn = {1-58113-199-2},
    pages = {83--94},
    location = {Vancouver, British Columbia, Canada},
    doi = {http://doi.acm.org/10.1145/349299.349314},
    publisher = {ACM},
    address = {New York, NY, USA},
    }
   
   @book{Kn-lncs1428,
      author = {Knoop, J.},
      title = {Optimal Interprocedural Program Optimization: A new Framework
               and its Application.},
      publisher = {LNCS Tutorial 1428, Springer-V.},
      year = {1998},
   }
   
 @INPROCEEDINGS{LeeShrivastava09a,  @INPROCEEDINGS{LeeShrivastava09a,
         TITLE       = {Compiler-Managed Register File Protection for Energy-Efficient Soft Error Reduction},          TITLE       = {Compiler-Managed Register File Protection for Energy-Efficient Soft Error Reduction},
         AUTHOR      = {Jongeun Lee and Aviral Shrivastava},          AUTHOR      = {Jongeun Lee and Aviral Shrivastava},
Line 280  ISSN={0018-9529}, } Line 553  ISSN={0018-9529}, }
         PAGES       = "288--292",          PAGES       = "288--292",
 }  }
   
   @inproceedings{Prantl:WCET2009,
           Address = {Dublin, Ireland},
           Author = {Adrian Prantl and Jens Knoop and Raimund Kirner and Albrecht Kadlec and Markus Schordan},
           Booktitle = {9th Intl. Workshop on Worst-Case Execution Time (WCET)
                    Analysis},
           Month = {June 30},
           Title = {From Trusted Annotations to Verified Knowledge},
           Year = {2009},
           URL = {http://costa.tuwien.ac.at/papers/wcet09.pdf}
   }
   
 @inproceedings{Prantl:WLPE2008,  @inproceedings{Prantl:WLPE2008,
         Address = {Udine, Italy},          Address = {Udine, Italy},
         Author = {Adrian Prantl and Jens Knoop and Markus Schordan and Markus Triska},          Author = {Adrian Prantl and Jens Knoop and Markus Schordan and Markus Triska},
Line 363  ISSN={0018-9529}, } Line 647  ISSN={0018-9529}, }
   annote =      {Keywords: Multi-core computing systems, scalable program analysis, reverse data-flow analysis, demand-driven data-flow analysis}    annote =      {Keywords: Multi-core computing systems, scalable program analysis, reverse data-flow analysis, demand-driven data-flow analysis}
 }  }
   
 @InProceedings{conf/cc/XueK06,  @InProceedings{Gus:ISoLA2006,
     author =       {Jan Gustafsson},
     title =        {The {WCET} Tool Challenge 2006},
     booktitle =    {Preliminary Proc. 2nd International IEEE Symposium on Leveraging
                     Applications of Formal Methods, Verification and Validation},
     year =         {2006},
     address =      {Paphos, Cyprus},
     month =        {November},
     pages =        {248 - 249},
     annote =       {}
   }
   
   
   @inproceedings{Holsti:WCET2008,
           Address = {Prague, Czech Republic},
           Author = {Niklas Holsti and Jan Gustafsson and Guillem Bernat (eds.) and
                     Cl\'ement Ballabriga and Armelle Bonenfant and Roman Bourgade and
                     Hugues Cass\'e  and Daniel Cordes and Albrecht Kadlec and 
                     Raimund Kirner and Jens Knoop and Paul Lokuciejewski and
                     Nicholas Merriam and Marianne de Michiel and Adrian Prantl and
                     Bernhard Rieder and Christine Rochange and Pascal Sainrat and
                     Markus Schordan},
           Booktitle = {Proc. 8th International Workshop on Worst-Case Execution Time Analysis (WCET 2008)},
           Month = {July},
           Title = {{WCET Tool Challenge 2008: Report}},
           Year = {2008},
           Pages = {149-171},
           Publisher = {{\"Osterreichische Computer Gesellschaft}},
           note = {ISBN: 978-3-85403-237-3},
           URL = {http://costa.tuwien.ac.at/papers/wcet08-challenge.pdf}
   }
   
   @Article{Wilhelm:TECS2008,
     author =       {Reinhard Wilhelm and Jakob Engblom and Andreas Ermedahl and Niklas Holsti and
                     Stephan Thesing and David Whalley and Guillem Bernat and Christian Ferdinand and
                     Reinhold Heckman and Tulika Mitra and Frank Mueller and Isabelle Puaut and
                     Peter Puschner and Jan Staschulat and Per Stenstrom},
     title =        {The Worst-Case Execution Time Problem - Overview of Methods
                     and Survey of Tools},
     journal =      {ACM Transactions on Embedded Computing Systems (TECS)},
     year =         {2008},
     volume =       {7},
     number =       {3},
     OPTpages =     {},
     month =        {Apr.},
     annote =       {http://www.artist-embedded.org/docs/Events/2007/MOTIVES/surveyTimingAnalysis_wilhelm.pdf}
   }
   
   @InProceedings{XueK06,
   title =       "A Fresh Look at {PRE} as a Maximum Flow Problem",    title =       "A Fresh Look at {PRE} as a Maximum Flow Problem",
   author =      "Jingling Xue and Jens Knoop",    author =      "Jingling Xue and Jens Knoop",
   bibdate =     "2006-04-05",    bibdate =     "2006-04-05",
Removed from v.1.5  
changed lines
  Added in v.1.6

FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>