@inproceedings{DBLP:conf/itp/BessonBW17,
  author    = {Fr{\'{e}}d{\'{e}}ric Besson and
               Sandrine Blazy and
               Pierre Wilke},
  title     = {CompCertS: {A} Memory-Aware Verified {C} Compiler Using Pointer as
               Integer Semantics},
  booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
               2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
  pages     = {81--97},
  year      = {2017},
  crossref  = {DBLP:conf/itp/2017},
  url       = {https://doi.org/10.1007/978-3-319-66107-0\_6},
  doi       = {10.1007/978-3-319-66107-0\_6},
  timestamp = {Thu, 12 Oct 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/BessonBW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

{"_id":"npLYmATufdEL8AtK3","bibbaseid":"besson-blazy-wilke-compcertsamemoryawareverifiedccompilerusingpointerasintegersemantics-2017","downloads":0,"creationDate":"2019-02-19T13:31:04.705Z","title":"CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics","author_short":["Besson, F.","Blazy, S.","Wilke, P."],"year":2017,"bibtype":"inproceedings","biburl":"https://dblp.uni-trier.de/pers/tb2/b/Blazy:Sandrine.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Frédéric"],"propositions":[],"lastnames":["Besson"],"suffixes":[]},{"firstnames":["Sandrine"],"propositions":[],"lastnames":["Blazy"],"suffixes":[]},{"firstnames":["Pierre"],"propositions":[],"lastnames":["Wilke"],"suffixes":[]}],"title":"CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics","booktitle":"Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings","pages":"81–97","year":"2017","crossref":"DBLP:conf/itp/2017","url":"https://doi.org/10.1007/978-3-319-66107-0_6","doi":"10.1007/978-3-319-66107-0_6","timestamp":"Thu, 12 Oct 2017 01:00:00 +0200","biburl":"https://dblp.org/rec/bib/conf/itp/BessonBW17","bibsource":"dblp computer science bibliography, https://dblp.org","bibtex":"@inproceedings{DBLP:conf/itp/BessonBW17,\n author = {Fr{\\'{e}}d{\\'{e}}ric Besson and\n Sandrine Blazy and\n Pierre Wilke},\n title = {CompCertS: {A} Memory-Aware Verified {C} Compiler Using Pointer as\n Integer Semantics},\n booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}\n 2017, Bras{\\'{\\i}}lia, Brazil, September 26-29, 2017, Proceedings},\n pages = {81--97},\n year = {2017},\n crossref = {DBLP:conf/itp/2017},\n url = {https://doi.org/10.1007/978-3-319-66107-0\\_6},\n doi = {10.1007/978-3-319-66107-0\\_6},\n timestamp = {Thu, 12 Oct 2017 01:00:00 +0200},\n biburl = {https://dblp.org/rec/bib/conf/itp/BessonBW17},\n bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n","author_short":["Besson, F.","Blazy, S.","Wilke, P."],"key":"DBLP:conf/itp/BessonBW17","id":"DBLP:conf/itp/BessonBW17","bibbaseid":"besson-blazy-wilke-compcertsamemoryawareverifiedccompilerusingpointerasintegersemantics-2017","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-319-66107-0_6"},"downloads":0,"html":""},"search_terms":["compcerts","memory","aware","verified","compiler","using","pointer","integer","semantics","besson","blazy","wilke"],"keywords":[],"authorIDs":[],"dataSources":["dFq2BpHTjvGdGdpXC"]}