Ignore:
Timestamp:
Jun 15, 2011, 10:53:50 AM (9 years ago)
Author:
mulligan
Message:

more changes, including additions to the bibliography, and tightening up the introduction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.bib

    r927 r953  
     1@article
     2{ asperti:user:2007,
     3  author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
     4  title = {User interaction with the {Matita} proof assistant},
     5  journal = {Journal of Automated Reasoning},
     6  pages = {109--139},
     7  volume = {39},
     8  issue = {2},
     9  year = {2007}
     10}
     11
     12@article
     13{ bate:wcet:2011,
     14  author = {Iain Bate and Usman Khan},
     15  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
     16  journal = {Empirical Software Engineering},
     17  pages = {5--28},
     18  volume = {16},
     19  issue = {1},
     20  year = {2011}
     21}
     22
    123@article
    224{ klein:sel4:2010,
     
    1032}
    1133
    12 @proceedings
     34@article
     35{ leroy:formal:2009,
     36  author = {Xavier Leroy},
     37  title = {Formal verification of a realistic compiler},
     38  journal = {Communications of the {Association of Computing Machinery}},
     39  volume = {52},
     40  number = {7},
     41  pages = {107--115},
     42  year = {2009}
     43}
     44
     45@article
     46{ leroy:formally:2009,
     47  author = {Xavier Leroy},
     48  title = {A formally verified compiler back-end},
     49  journal = {Journal of Automated Reasoning},
     50  volume = {43},
     51  number = {4},
     52  pages = {363--446},
     53  year = {2009}
     54}
     55
     56@inproceedings
     57{ blazy:formal:2006,
     58  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
     59  title = {Formal Verification of a {C} Compiler Front-End},
     60  booktitle = {International Symposium on Formal Methods},
     61  pages = {460--475},
     62  year = {2006}
     63}
     64
     65@inproceedings
    1366{ klein:sel4:2009,
    1467  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
     
    1871}
    1972
     73@inproceedings
     74{ yan:wcet:2008,
     75  author = {Jun Yan and Wei Zhang},
     76  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
     77  booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
     78  pages = {80--89},
     79  year = {2008}
     80}
     81
    2082@misc
    2183{ cerco:2011,
    22   title = {The {CerCo} project},
    23   url = {http://cerco.cs.unibo.it/},
    24   year = {2011}
     84  title = {The {CerCo} {FET-Open} project},
     85  howpublished = {\url{http://cerco.cs.unibo.it/}},
     86  year = {2011},
     87  key = {cerco:2011}
     88}
     89
     90@misc
     91{ cerco-report-code:2011,
     92  title = {{CerCo Deliverable D2.2}: prototype cost-preserving C compiler},
     93  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2_Code.tar.gz}},
     94  year = {2011},
     95  key = {cerco-2.2-report-code:2011}
    2596}
    2697
     
    2899{ compcert:2011,
    29100  title = {The {CompCert} project},
    30   url = {http://compcert.inria.fr/},
    31   year = {2011}
     101  howpublished = {\url{http://compcert.inria.fr/}},
     102  year = {2011},
     103  key = {compcert:2011}
     104}
     105
     106@misc
     107{ sdcc:2011,
     108  title = {Small Device {C} Compiler 3.0.0},
     109  howpublished = {\url{http://sdcc.sourceforge.net/}},
     110  year = {2011},
     111  key = {sdcc:2010}
    32112}
    33113
     
    35115{ sel4:2011,
    36116  title = {The {l4.verified} project},
    37   url = {http://ertos.nicta.com.au/research/l4.verified/},
     117  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
    38118  year = {2011}
    39119}
     120
     121@misc
     122{ siemens:2011,
     123  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
     124  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
     125  year = {2011},
     126  key = {siemens:2011}
     127}
     128
     129@techreport
     130{ amadio:certifying:2010,
     131  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
     132  title = {Cerifying cost annotations in compilers},
     133  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
     134  year = {2010}
     135}
Note: See TracChangeset for help on using the changeset viewer.