Changeset 3477 for Papers/sttt/biblio.bib

Timestamp:

Sep 22, 2014, 3:50:30 PM (5 years ago)

Author:

mulligan

Message:

changes to intro, in progress...

File:

• Papers/sttt/biblio.bib (modified) (1 diff)

Papers/sttt/biblio.bib

@@ +1 @@
+@article
+{ asperti:user:2007,
+  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
+  title = {User interaction with the {Matita} proof assistant},
+  journal = {Automated Reasoning},
+  pages = {109--139},
+  volume = {39},
+  issue = {2},
+  year = {2007}
+}
+
+@article
+{ bate:wcet:2011,
+  author = {Iain Bate and Usman Khan},
+  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
+  journal = {Empirical Software Engineering},
+  pages = {5--28},
+  volume = {16},
+  issue = {1},
+  year = {2011}
+}
+
+@article
+{ klein:machine:2006,
+  author = {Gerwin Klein and Tobias Nipkow},
+  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
+  journal = {{ACM} Transactions on Programming Languages and Systems},
+  volume = {28}, 
+  number = {4}, 
+  pages = {619--695},
+  year = {2006}
+}
+
+@article
+{ klein:sel4:2010,
+  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},
+  title = {{seL4}: Formal verification of an operating system kernel},
+  journal = {Communications of the {ACM}},
+  issue = {6},
+  volume = {53},
+  pages = {107--115},
+  year = {2010}
+}
+
+@article
+{ leroy:formal:2009,
+  author = {Xavier Leroy},
+  title = {Formal verification of a realistic compiler},
+  journal = {Communications of the {ACM}},
+  volume = {52},
+  number = {7},
+  pages = {107--115},
+  year = {2009}
+}
+
+@article
+{ leroy:formally:2009,
+  author = {Xavier Leroy},
+  title = {A formally verified compiler back-end},
+  journal = {Automated Reasoning},
+  volume = {43},
+  number = {4},
+  pages = {363--446},
+  year = {2009}
+}
+
+@book
+{ moore:piton:1996,
+  author = {J Strother Moore},
+  title = {Piton: A mechanically verified assembly language},
+  series = {Automated Reasoning Series},
+  volume = {3},
+  isbn = {978-0-7923-3920-5},
+  publisher = {Springer},
+  year = {1996}
+}
+
+@inproceedings
+{ atkey:coqjvm:2007,
+  author = {Robert Atkey},
+  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
+  booktitle = {Types},
+  pages = {18--32},
+  year = {2007}
+}
+
+@inproceedings
+{ blazy:formal:2006,
+  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
+  title = {Formal Verification of a {C} Compiler Front-End},
+  booktitle = {{FM}},
+  pages = {460--475},
+  year = {2006}
+}
+
+@inproceedings
+{ fox:trustworthy:2010,
+  author = {Anthony Fox and Magnus O. Myreen},
+  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
+  booktitle = {{ITP}},
+  pages = {243--258},
+  year = {2010}
+}
+
+@inproceedings
+{ sevcik:relaxed-memory:2011,
+  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
+  title = {Relaxed-Memory Concurrency and Verified Compilation},
+  booktitle = {{POPL}},
+  year = {2011}
+}
+
+@inproceedings
+{ tuch:types:2007,
+  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
+  title = {Types, Bytes, and Separation Logic},
+  booktitle = {{POPL}},
+  pages = {97--108},
+  year =  {2007}
+}
+
+
+@inproceedings
+{ klein:sel4:2009,
+  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},
+  title = {{seL4}: Formal verification of an operating system kernel},
+  booktitle = {{SOSP}},
+  year = {2009}
+}
+
+@inproceedings
+{ mulligan:executable:2011,
+  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
+  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
+  booktitle = {{FMCAD}},
+  year = {2011},
+  note = {Submitted}
+}
+
+@inproceedings
+{ sarkar:semantics:2009,
+  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},
+  title = {The semantics of {x86-CC} multiprocessor machine code},
+  booktitle = {{POPL}},
+  pages = {379--391},
+  year = {2009}
+}
+
+@inproceedings
+{ sozeau:subset:2006,
+  author = {Matthieu Sozeau},
+  title = {Subset Coercions in {Coq}},
+  booktitle = {Types},
+  pages = {237--252},
+  year = {2006}
+}
+
+@inproceedings
+{ yan:wcet:2008,
+  author = {Jun Yan and Wei Zhang},
+  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
+  booktitle = {{RTAS}},
+  pages = {80--89},
+  year = {2008}
+}
+
+@misc
+{ boender:correctness:2012,
+  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
+  title = {On the correctness of a branch displacement algorithm},
+  howpublished = {\url{http://arxiv.org/abs/1209.5920}},
+  year = {2012}
+}
+
+@misc
+{ cerco:2011,
+  title = {The {CerCo} {FET-Open} project},
+  howpublished = {\url{http://cerco.cs.unibo.it/}},
+  year = {2011},
+  key = {CerCo:2011}
+}
+
+@misc
+{ cerco-report-code:2011,
+  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
+  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}},
+  year = {2011},
+  key = {CerCo-2.2-Report-Code:2011}
+}
+
+@misc
+{ compcert:2011,
+  title = {The {CompCert} project},
+  howpublished = {\url{http://compcert.inria.fr/}},
+  year = {2011},
+  key = {CompCert:2011}
+}
+
+@misc
+{ hyde:branch:2006,
+  title = {Branch displacement optimisation},
+  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
+  year = {2006},
+  key = {Hyde:Branch:2006}
+}
+
+@misc
+{ moore:grand:2005,
+  author = {J Strother Moore},
+  title = {A Grand Challenge Proposal for Formal Methods},
+  year = {2005}
+}
+
+@misc
+{ sdcc:2011,
+  title = {Small Device {C} Compiler 3.0.0},
+  howpublished = {\url{http://sdcc.sourceforge.net/}},
+  year = {2011},
+  key = {sdcc:2010}
+}
+
+@misc
+{ sel4:2011,
+  title = {The {l4.verified} project},
+  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
+  year = {2011}
+}
+
+@misc
+{ siemens:2011,
+  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
+  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
+  year = {2011},
+  key = {siemens:2011}
+}
+
+@techreport
+{ amadio:certifying:2010,
+  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
+  title = {Cerifying cost annotations in compilers},
+  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
+  year = {2010}
+}
+
+@techreport
+{ klein:machine:2010,
+  author = {Gerwin Klein and Tobias Nipkow},
+  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
+  institution = {National {ICT} Australia},
+  number = {0400001T.1},
+  year = {2010}
+
+}
+
+
 @article{Szymanski1978,
  author = {Szymanski, Thomas G.},