source: Papers/sttt/biblio.bib @ 3470

Last change on this file since 3470 was 3470, checked in by boender, 5 years ago
  • added first version of STTT paper
File size: 5.5 KB
Line 
1@article{Szymanski1978,
2 author = {Szymanski, Thomas G.},
3 title = {Assembling code for machines with span-dependent instructions},
4 journal = {Commun. ACM},
5 issue_date = {April 1978},
6 volume = {21},
7 number = {4},
8 month = apr,
9 year = {1978},
10 issn = {0001-0782},
11 pages = {300--308},
12 numpages = {9},
13 url = {http://doi.acm.org/10.1145/359460.359474},
14 doi = {10.1145/359460.359474},
15 acmid = {359474},
16 publisher = {ACM},
17 address = {New York, NY, USA},
18 keywords = {NP-complete, assemblers, code generation, compilers, computational complexity, span-dependent instructions, variable-length addressing},
19} 
20
21@article{Robertson1979,
22 author = {Robertson, Edward L.},
23 title = {Code Generation and Storage Allocation for Machines with Span-Dependent Instructions},
24 journal = {ACM Trans. Program. Lang. Syst.},
25 issue_date = {July 1979},
26 volume = {1},
27 number = {1},
28 month = jan,
29 year = {1979},
30 issn = {0164-0925},
31 pages = {71--83},
32 numpages = {13},
33 url = {http://doi.acm.org/10.1145/357062.357067},
34 doi = {10.1145/357062.357067},
35 acmid = {357067},
36 publisher = {ACM},
37 address = {New York, NY, USA},
38} 
39
40@article{Dickson2008,
41  author    = {Neil G. Dickson},
42  title     = {A Simple, Linear-Time Algorithm for x86 Jump Encoding},
43  journal   = {CoRR},
44  volume    = {abs/0812.4973},
45  year      = {2008},
46  ee        = {http://arxiv.org/abs/0812.4973},
47  bibsource = {DBLP, http://dblp.uni-trier.de}
48}
49
50@inproceedings{Sozeau2006,
51  author = {Matthieu Sozeau},
52  title = {Subset Coercions in {Coq}},
53  booktitle = {{TYPES}},
54  pages = {237--252},
55  year = {2006}
56}
57
58@misc{SDCC2011,
59  title = {Small Device {C} Compiler 3.1.0},
60  howpublished = {\url{http://sdcc.sourceforge.net/}},
61  year = {2011},
62        key = {SDCC2011}
63}
64
65@misc{IntelDev,
66        author = {Intel},
67        title = {{Intel 64 and IA-32 Architectures Developer's Manual}},
68        howpublished={\url{http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}},
69        volume=2,
70  key = {IntelDev}
71}
72
73@article {Leroy2009,
74   author = {Leroy, Xavier},
75   affiliation = {INRIA Paris-Rocquencourt B.P. 105 78153 Le Chesnay France},
76   title = {A Formally Verified Compiler Back-end},
77   journal = {Journal of Automated Reasoning},
78   publisher = {Springer Netherlands},
79   issn = {0168-7433},
80   keyword = {Computer Science},
81   pages = {363-446},
82   volume = {43},
83   issue = {4},
84   url = {http://dx.doi.org/10.1007/s10817-009-9155-4},
85   note = {10.1007/s10817-009-9155-4},
86   year = {2009}
87}
88
89@book {Moore1996, 
90  author = {J Strother Moore},
91  title = {Piton: A mechanically verified assembly language},
92  series = {Automated Reasoning Series},
93  volume = {3},
94  isbn = {978-0-7923-3920-5},
95  publisher = {Springer},
96  year = {1996}
97}
98
99@misc {Hyde2006,
100  title = {Branch displacement optimisation},
101        author = {Randall Hyde},
102  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
103  year = {2006},
104}
105
106@misc{DC2012,
107        title={{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}},
108        author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
109        year = {2012},
110        booktitle = {Certified Proofs and Programs {(CPP)}},
111        note = {Submitted}
112}
113
114@article{Asperti2007,
115  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
116  title = {User interaction with the {Matita} proof assistant},
117  journal = {Automated Reasoning},
118  pages = {109--139},
119  volume = {39},
120  issue = {2},
121  year = {2007}
122}
123
124@article{TSO2011,
125 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
126 title = {Relaxed-memory concurrency and verified compilation},
127 journal = {SIGPLAN Not.},
128 issue_date = {January 2011},
129 volume = {46},
130 number = {1},
131 month = jan,
132 year = {2011},
133 issn = {0362-1340},
134 pages = {43--54},
135 numpages = {12},
136 url = {http://doi.acm.org/10.1145/1925844.1926393},
137 doi = {10.1145/1925844.1926393},
138 acmid = {1926393},
139 publisher = {ACM},
140 address = {New York, NY, USA},
141 keywords = {relaxed memory models, semantics, verifying compilation},
142} 
143
144@inproceedings{Sevcik:2011:RCV:1926385.1926393,
145 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
146 title = {Relaxed-memory concurrency and verified compilation},
147 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
148 series = {POPL '11},
149 year = {2011},
150 isbn = {978-1-4503-0490-0},
151 location = {Austin, Texas, USA},
152 pages = {43--54},
153 numpages = {12},
154 url = {http://doi.acm.org/10.1145/1926385.1926393},
155 doi = {10.1145/1926385.1926393},
156 acmid = {1926393},
157 publisher = {ACM},
158 address = {New York, NY, USA},
159 keywords = {relaxed memory models, semantics, verifying compilation},
160} 
161
162@incollection{lastyear,
163year={2012},
164isbn={978-3-642-35307-9},
165booktitle={Certified Programs and Proofs},
166volume={7679},
167series={Lecture Notes in Computer Science},
168editor={Hawblitzel, Chris and Miller, Dale},
169doi={10.1007/978-3-642-35308-6_7},
170title={On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor},
171url={http://dx.doi.org/10.1007/978-3-642-35308-6_7},
172publisher={Springer Berlin Heidelberg},
173keywords={Verified software; CerCo (Certified Complexity); MCS-51 microcontroller; Matita proof assistant},
174author={Mulligan, Dominic P. and Sacerdoti Coen, Claudio},
175pages={43-59}
176}
177
178@misc
179{ compcert:2011,
180  title = {The {CompCert} project},
181  howpublished = {\url{http://compcert.inria.fr/}},
182  year = {2011},
183  key = {compcert:2011}
184}
Note: See TracBrowser for help on using the repository browser.