Ignore:
Timestamp:
Sep 22, 2014, 3:50:30 PM (5 years ago)
Author:
mulligan
Message:

changes to intro, in progress...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/sttt/biblio.bib

    r3470 r3477  
     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 = {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
     23@article
     24{ klein:machine:2006,
     25  author = {Gerwin Klein and Tobias Nipkow},
     26  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     27  journal = {{ACM} Transactions on Programming Languages and Systems},
     28  volume = {28},
     29  number = {4},
     30  pages = {619--695},
     31  year = {2006}
     32}
     33
     34@article
     35{ klein:sel4:2010,
     36  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 and Harvey Tuch and Simon Winwood},
     37  title = {{seL4}: Formal verification of an operating system kernel},
     38  journal = {Communications of the {ACM}},
     39  issue = {6},
     40  volume = {53},
     41  pages = {107--115},
     42  year = {2010}
     43}
     44
     45@article
     46{ leroy:formal:2009,
     47  author = {Xavier Leroy},
     48  title = {Formal verification of a realistic compiler},
     49  journal = {Communications of the {ACM}},
     50  volume = {52},
     51  number = {7},
     52  pages = {107--115},
     53  year = {2009}
     54}
     55
     56@article
     57{ leroy:formally:2009,
     58  author = {Xavier Leroy},
     59  title = {A formally verified compiler back-end},
     60  journal = {Automated Reasoning},
     61  volume = {43},
     62  number = {4},
     63  pages = {363--446},
     64  year = {2009}
     65}
     66
     67@book
     68{ moore:piton:1996,
     69  author = {J Strother Moore},
     70  title = {Piton: A mechanically verified assembly language},
     71  series = {Automated Reasoning Series},
     72  volume = {3},
     73  isbn = {978-0-7923-3920-5},
     74  publisher = {Springer},
     75  year = {1996}
     76}
     77
     78@inproceedings
     79{ atkey:coqjvm:2007,
     80  author = {Robert Atkey},
     81  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
     82  booktitle = {Types},
     83  pages = {18--32},
     84  year = {2007}
     85}
     86
     87@inproceedings
     88{ blazy:formal:2006,
     89  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
     90  title = {Formal Verification of a {C} Compiler Front-End},
     91  booktitle = {{FM}},
     92  pages = {460--475},
     93  year = {2006}
     94}
     95
     96@inproceedings
     97{ fox:trustworthy:2010,
     98  author = {Anthony Fox and Magnus O. Myreen},
     99  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
     100  booktitle = {{ITP}},
     101  pages = {243--258},
     102  year = {2010}
     103}
     104
     105@inproceedings
     106{ sevcik:relaxed-memory:2011,
     107  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
     108  title = {Relaxed-Memory Concurrency and Verified Compilation},
     109  booktitle = {{POPL}},
     110  year = {2011}
     111}
     112
     113@inproceedings
     114{ tuch:types:2007,
     115  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
     116  title = {Types, Bytes, and Separation Logic},
     117  booktitle = {{POPL}},
     118  pages = {97--108},
     119  year =  {2007}
     120}
     121
     122
     123@inproceedings
     124{ klein:sel4:2009,
     125  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 and Harvey Tuch and Simon Winwood},
     126  title = {{seL4}: Formal verification of an operating system kernel},
     127  booktitle = {{SOSP}},
     128  year = {2009}
     129}
     130
     131@inproceedings
     132{ mulligan:executable:2011,
     133  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
     134  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
     135  booktitle = {{FMCAD}},
     136  year = {2011},
     137  note = {Submitted}
     138}
     139
     140@inproceedings
     141{ sarkar:semantics:2009,
     142  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
     143  title = {The semantics of {x86-CC} multiprocessor machine code},
     144  booktitle = {{POPL}},
     145  pages = {379--391},
     146  year = {2009}
     147}
     148
     149@inproceedings
     150{ sozeau:subset:2006,
     151  author = {Matthieu Sozeau},
     152  title = {Subset Coercions in {Coq}},
     153  booktitle = {Types},
     154  pages = {237--252},
     155  year = {2006}
     156}
     157
     158@inproceedings
     159{ yan:wcet:2008,
     160  author = {Jun Yan and Wei Zhang},
     161  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
     162  booktitle = {{RTAS}},
     163  pages = {80--89},
     164  year = {2008}
     165}
     166
     167@misc
     168{ boender:correctness:2012,
     169  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
     170  title = {On the correctness of a branch displacement algorithm},
     171  howpublished = {\url{http://arxiv.org/abs/1209.5920}},
     172  year = {2012}
     173}
     174
     175@misc
     176{ cerco:2011,
     177  title = {The {CerCo} {FET-Open} project},
     178  howpublished = {\url{http://cerco.cs.unibo.it/}},
     179  year = {2011},
     180  key = {CerCo:2011}
     181}
     182
     183@misc
     184{ cerco-report-code:2011,
     185  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
     186  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}},
     187  year = {2011},
     188  key = {CerCo-2.2-Report-Code:2011}
     189}
     190
     191@misc
     192{ compcert:2011,
     193  title = {The {CompCert} project},
     194  howpublished = {\url{http://compcert.inria.fr/}},
     195  year = {2011},
     196  key = {CompCert:2011}
     197}
     198
     199@misc
     200{ hyde:branch:2006,
     201  title = {Branch displacement optimisation},
     202  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
     203  year = {2006},
     204  key = {Hyde:Branch:2006}
     205}
     206
     207@misc
     208{ moore:grand:2005,
     209  author = {J Strother Moore},
     210  title = {A Grand Challenge Proposal for Formal Methods},
     211  year = {2005}
     212}
     213
     214@misc
     215{ sdcc:2011,
     216  title = {Small Device {C} Compiler 3.0.0},
     217  howpublished = {\url{http://sdcc.sourceforge.net/}},
     218  year = {2011},
     219  key = {sdcc:2010}
     220}
     221
     222@misc
     223{ sel4:2011,
     224  title = {The {l4.verified} project},
     225  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
     226  year = {2011}
     227}
     228
     229@misc
     230{ siemens:2011,
     231  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
     232  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
     233  year = {2011},
     234  key = {siemens:2011}
     235}
     236
     237@techreport
     238{ amadio:certifying:2010,
     239  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
     240  title = {Cerifying cost annotations in compilers},
     241  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
     242  year = {2010}
     243}
     244
     245@techreport
     246{ klein:machine:2010,
     247  author = {Gerwin Klein and Tobias Nipkow},
     248  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     249  institution = {National {ICT} Australia},
     250  number = {0400001T.1},
     251  year = {2010}
     252
     253}
     254
     255
    1256@article{Szymanski1978,
    2257 author = {Szymanski, Thomas G.},
Note: See TracChangeset for help on using the changeset viewer.