1:
2: @article{781156,
3: author = {Lerner, Sorin and Millstein, Todd and Chambers, Craig},
4: title = {Automatically proving the correctness of compiler optimizations},
5: journal = {SIGPLAN Not.},
6: volume = {38},
7: number = {5},
8: year = {2003},
9: issn = {0362-1340},
10: pages = {220--231},
11: doi = {http://doi.acm.org/10.1145/780822.781156},
12: publisher = {ACM},
13: address = {New York, NY, USA},
14: }
15:
16: @article{1040335,
17: author = {Lerner, Sorin and Millstein, Todd and Rice, Erika and Chambers, Craig},
18: title = {Automated soundness proofs for dataflow analyses and transformations via local rules},
19: journal = {SIGPLAN Not.},
20: volume = {40},
21: number = {1},
22: year = {2005},
23: issn = {0362-1340},
24: pages = {364--377},
25: doi = {http://doi.acm.org/10.1145/1047659.1040335},
26: publisher = {ACM},
27: address = {New York, NY, USA},
28: }
29:
30: @article{1328444,
31: author = {Jean-Baptiste Tristan and Xavier Leroy},
32: title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
33: journal = {SIGPLAN Not.},
34: volume = {43},
35: number = {1},
36: year = {2008},
37: issn = {0362-1340},
38: pages = {17--27},
39: doi = {http://doi.acm.org/10.1145/1328897.1328444},
40: publisher = {ACM},
41: address = {New York, NY, USA},
42: }
43:
44: @inproceedings{KRS-pldi92,
45: author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
46: title = {Lazy Code Motion},
47: booktitle = "Proc. ACM SIGPLAN Conf. on
48: Prog. Lang. Design and Impl.
49: $($PLDI'92$)$",
50: series = {{ACM SIGPLAN} Not.},
51: volume = {{\em 27},7},
52: year = {1992},
53: pages = {224 - 234}
54: }
55:
56: @inproceedings{KRS-retrolcm04,
57: author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
58: title = {{\sc Retrospective}: Lazy Code Motion},
59: booktitle = "``20 Years of the ACM SIGPLAN Conference on
60: Programming Language Design and
61: Implementation (1979 - 1999): A Selection''",
62: series = {{ACM SIGPLAN} Not.},
63: volume = {{\em 39},4},
64: year = {2004},
65: pages = {460 - 461 \& 462 - 472}
66: }
67:
68: @inproceedings{KRS-pldi94,
69: author = {Knoop, J. and R\"uthing, O. and Steffen, B.},
70: title = {Partial Dead Code Elimination},
71: booktitle = "Proc. ACM SIGPLAN Conf. on
72: Prog. Lang. Design and Impl.
73: $($PLDI'94$)$",
74: series = {{ACM SIGPLAN} Not.},
75: volume = {{\em 29},6},
76: year = {1994},
77: pages = {147 - 158}
78: }
79:
80:
81:
82: @inproceedings{RKS-popl00,
83: author = {R\"uthing, O. and Knoop, J. and Steffen, B.},
84: title = {Sparse Code Motion},
85: booktitle = "Conf. Rec. 27th Annual
86: Symp. on Principles of Prog. Lang.
87: $($POPL'00$)$",
88: publisher = "ACM, NY",
89: year = {2000},
90: pages = {170 - 183},
91: }
92:
93: @book{MMO-lncs1283,
94: author = {M\"uller-Olm, M.},
95: title = {Modular Compiler Verification},
96: publisher = {LNCS 1283, Springer-V.},
97: year = {1996},
98: }
99:
100: @Misc{CompCert,
101: key = {CompCert},
102: author = {Leroy, X.},
103: title = {The Compcert verified compiler.
104: \url{http://compcert.inria.fr/doc/index.html}.
105: CompCert is funded by ANR (grant number ANR-05-SSIA-0019),
106: as part of the ARA SSIA programme. }},
107: howpublished = {\url{http://compcert.inria.fr/doc/index.html}},
108: year = {2005 - 2008},
109: note = {CompCert is funded by ANR (grant number ANR-05-SSIA-0019),
110: as part of the ARA SSIA programme.}
111: }
112:
113: @inproceedings{Le-popl06,
114: author = {Leroy, X.},
115: title = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant},
116: booktitle = "Conf. Rec. 33rd Annual
117: Symp. on Principles of Prog. Lang.
118: $($POPL'06$)$",
119: publisher = "ACM, NY",
120: year = {2006},
121: }
122:
123: @InProceedings{BDL-fm06,
124: author = "Blazy, S. and Dargaye, Z. and Leroy, X.",
125: title = {Formal verification of a C compiler front-end},
126: booktitle = "{Formal Methods 2006}",
127: year = 2006,
128: volume = 4085,
129: series = {LNCS},
130: publisher = "Springer"
131: }
132:
133: @Article{Langmaack97a,
134: Author = {Langmaack, Hans},
135: Title = {{Softwareengineering zur Zertifizierung von
136: Systemen: Spezifikations-, Implementierungs-,
137: \"Ubersetzerkorrektheit}},
138: Journal = {Informationstechnik und Technische
139: Informatik it-ti},
140: Pages = {41-47},
141: Number = 3,
142: Volume = 97,
143: Publisher = {Oldenbourg Verlag},
144: Year = 1997,
145: }
146:
147: @InProceedings{Goerigk-et-al:CC96,
148: Author = {W. Goerigk and A. Dold and T. Gaul and G. Goos and
149: A. Heberle and F. von Henke and U. Hoffmann and
150: H. Langmaack and H. Pfeifer and H. Ruess and W. Zimmermann},
151: Title = "{C}ompiler {C}orrectness and {I}mplementation
152: {V}erification: {T}he {V}erifix {A}pproach",
153: BookTitle = {Proceedings of the Poster Session of CC'96 -
154: International Conference on Compiler Construction },
155: Editor = {P. Fritzson},
156: Publisher = {ida},
157: Year = {1996},
158: Note = {TR-Nr.: R-96-12},
159: Pages = {65 -- 73},
160: }
161:
162:
163: @Article{Langmaack96a,
164: Author = {Langmaack, H.},
165: Title = {{The ProCoS Approach to Correct Systems}},
166: Journal = {Real Time Systems},
167: Volume = {13},
168: Pages = {253-275},
169: Publisher = {Kluwer Academic Publishers},
170: Year = 1997
171: }
172:
173:
174: @InProceedings{Goos:00:ASM,
175: author = "Gerhard Goos and
176: Wolf Zimmermann",
177: title = {Verifying Compilers and ASMs},
178: booktitle = "{Abstract State Machines, Theory and Applications}",
179: year = 2000,
180: pages = {177-202},
181: editor = {Yuri Gurevich and Philipp W. Kutter and
182: Martin Odersky and Lothar Thiele},
183: volume = 1912,
184: series = {LNCS},
185: publisher = "Springer"
186: }
187:
188: @InCollection{Goos:99:verifix,
189: author = {Gerhard Goos and Wolf Zimmermann},
190: title = {Verification of Compilers},
191: booktitle = {Correct System Design},
192: pages = {201-230},
193: publisher = {Springer-Verlag},
194: year = 1999,
195: editor = {Bernhard Steffen and Ernst Rüdiger Olderog},
196: volume = 1710,
197: series = {LNCS}
198: }
199:
200: @book{Po-lncs124,
201: author = {Polak, W.},
202: title = {Compiler Specification and Verification.},
203: publisher = {LNCS 124, Springer-V.},
204: year = {1981},
205: }
206:
207: @article{Hoare03,
208: author = {Tony Hoare},
209: title = {The verifying compiler: A grand challenge for computing research},
210: journal = {Journal of the ACM},
211: volume = {50},
212: number = {1},
213: year = {2003},
214: issn = {0004-5411},
215: pages = {63--69},
216: doi = {http://doi.acm.org/10.1145/602382.602403},
217: publisher = {ACM},
218: address = {New York, NY, USA},
219: }
220:
221: @inproceedings{TristanLeroy09,
222: author = {Jean-Baptiste Tristan and Xavier Leroy},
223: title = {Verified Validation of Lazy Code Motion},
224: booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
225: year = {2009},
226: isbn = {978-1-60558-392-1},
227: pages = {316--326},
228: location = {Dublin, Ireland},
229: doi = {http://doi.acm.org/10.1145/1542476.1542512},
230: publisher = {ACM},
231: address = {New York, NY, USA},
232: }
233:
234: @inproceedings{Kundu+09,
235: author = {Sudipta Kundu and Zachary Tatlock and Sorin Lerner},
236: title = {Proving Optimizations Correct using Parameterized Program Equivalence},
237: booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
238: year = {2009},
239: isbn = {978-1-60558-392-1},
240: pages = {327--337},
241: location = {Dublin, Ireland},
242: doi = {http://doi.acm.org/10.1145/1542476.1542513},
243: publisher = {ACM},
244: address = {New York, NY, USA},
245: }
246:
247: @inproceedings{Necula00,
248: author = {George C. Necula},
249: title = {Translation Validation for an Optimizing Compiler},
250: booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
251: year = {2000},
252: isbn = {1-58113-199-2},
253: pages = {83--94},
254: location = {Vancouver, British Columbia, Canada},
255: doi = {http://doi.acm.org/10.1145/349299.349314},
256: publisher = {ACM},
257: address = {New York, NY, USA},
258: }
259:
260: @article{TristanLeroy08,
261: author = {Jean-Baptiste Tristan and Xavier Leroy},
262: title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
263: journal = {SIGPLAN Not.},
264: volume = {43},
265: number = {1},
266: year = {2008},
267: issn = {0362-1340},
268: pages = {17--27},
269: doi = {http://doi.acm.org/10.1145/1328897.1328444},
270: publisher = {ACM},
271: address = {New York, NY, USA},
272: }
273:
274: @inproceedings{FNSG-tlfi07,
275: author = {Feng, Xinyu and Ni, Zhaozhong and Shao, Zhong and Guo, Yu},
276: title = {An open framework for foundational proof-carrying code},
277: booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation},
278: year = {2007},
279: isbn = {1-59593-393-X},
280: pages = {67--78},
281: location = {Nice, Nice, France},
282: doi = {http://doi.acm.org/10.1145/1190315.1190325},
283: publisher = {ACM},
284: address = {New York, NY, USA},
285: }
286:
287: @inproceedings{AF-popl00,
288: author = {Appel, Andrew W. and Felty, Amy P.},
289: title = {A semantic model of types and machine instructions for proof-carrying code},
290: booktitle = {POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
291: year = {2000},
292: isbn = {1-58113-125-9},
293: pages = {243--253},
294: location = {Boston, MA, USA},
295: doi = {http://doi.acm.org/10.1145/325694.325727},
296: publisher = {ACM},
297: address = {New York, NY, USA},
298: }
299:
300: @inproceedings{ZaksPnueli08,
301: author = {Anna Zaks and Amir Pnueli},
302: title = {Program Analysis for Compiler Validation},
303: booktitle = {PASTE '08: Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering},
304: year = {2008},
305: isbn = {978-1-60558-382-2},
306: pages = {1--7},
307: location = {Atlanta, Georgia},
308: doi = {http://doi.acm.org/10.1145/1512475.1512477},
309: publisher = {ACM},
310: address = {New York, NY, USA},
311: }
312:
313: @inproceedings{Pnueli98b,
314: author = {Amir Pnueli and Michael Siegel and Eli Singerman},
315: title = {Translation Validation},
316: booktitle = {TACAS '98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems},
317: year = {1998},
318: isbn = {3-540-64356-7},
319: pages = {151--166},
320: publisher = {Springer-Verlag},
321: address = {London, UK},
322: }
323:
324: @Article{Pnueli98a,
325: author = "Amir Pnueli and Ofer Shtrichman and Michael Siegel",
326: title = "The {Code Validation Tool (CVT)}: Automatic
327: verification of a compilation process",
328: journal = "International Journal on Software Tools for Technology
329: Transfer (STTT)",
330: volume = "2",
331: number = "2",
332: pages = "192--201",
333: month = "December",
334: year = "1998",
335: ISSN = "1433-2779 (print), 1433-2787 (electronic)",
336: }
337:
338: @article{GlesnerGoosZimmeermann04,
339: author = {Sabine Glesner and
340: Gerhard Goos and
341: Wolf Zimmermann},
342: title = {Verifix: Konstruktion und Architektur verifizierender {\"U}bersetzer
343: (Verifix: Construction and Architecture of Verifying Compilers)},
344: journal = {it - Information Technology},
345: volume = {46},
346: number = {5},
347: year = {2004},
348: pages = {265-276},
349: ee = {http://dx.doi.org/10.1524/itit.46.5.265.44799},
350: bibsource = {DBLP, http://dblp.uni-trier.de}
351: }
352:
353: @inproceedings{GoosZimmermann00,
354: author = {Gerhard Goos and Wolf Zimmermann},
355: title = {Verifying Compilers and ASMs},
356: booktitle = {Abstract State Machines},
357: editor = {Yuri Gurevich and
358: Philipp W. Kutter and
359: Martin Odersky and
360: Lothar Thiele},
361: year = {2000},
362: pages = {177-202},
363: publisher = {Springer},
364: series = {Lecture Notes in Computer Science},
365: volume = {1912},
366: }
367:
368: @article{BlechPoetzsch07,
369:
370: author = {Jan Olaf Blech and Arnd Poetzsch-Heffter},
371: title = {A Certifying Code Generation Phase},
372: journal = {Electron. Notes Theor. Comput. Sci.},
373: volume = {190},
374: number = {4},
375: year = {2007},
376: issn = {1571-0661},
377: pages = {65--82},
378: doi = {http://dx.doi.org/10.1016/j.entcs.2007.09.008},
379: publisher = {Elsevier Science Publishers B. V.},
380: address = {Amsterdam, The Netherlands, The Netherlands},
381: }
382:
383: @inproceedings{Blome+06,
384: author = {Jason A. Blome and Shantanu Gupta and Shuguang Feng and Scott Mahlke},
385: title = {Cost-efficient soft error protection for embedded microprocessors},
386: booktitle = {International Conference on Compilers, Architecture and Synthesis
387: for Embedded Systems (CASES'06)},
388: year = {2006},
389: isbn = {1-59593-543-6},
390: pages = {421--431},
391: location = {Seoul, Korea},
392: publisher = {ACM},
393: address = {New York, NY, USA},
394: }
395:
396: @inproceedings{PSS-tacas98,
397: author = {Pnueli, A. and Siegel, M. and Singermann, E.},
398: title = {Translation Validation},
399: booktitle = {Proc. 4th Int. Conf. on Tools and
400: Algorithms for the Construction and Analysis of Systems
401: $($TACAS'98$)$},
402: publisher = {Springer-V.},
403: series = "LNCS 1384",
404: year = {1998},
405: pages = {151 - 166}
406: }
407:
408: @inproceedings{Ne-popl97,
409: author = {Necula, G. C.},
410: title = {Proof-Carrying Code},
411: booktitle = "Conf. Rec. 24th Annual
412: Symp. on Principles of Prog. Lang.
413: $($POPL'97$)$",
414: publisher = "ACM, NY",
415: year = {1997},
416: pages = {106 - 119},
417: }
418:
419: @article{NL-pldi98,
420: author = {Necula, George C. and Lee, Peter},
421: title = {The design and implementation of a certifying compiler},
422: journal = {SIGPLAN Not.},
423: volume = {33},
424: number = {5},
425: year = {1998},
426: issn = {0362-1340},
427: pages = {333--344},
428: doi = {http://doi.acm.org/10.1145/277652.277752},
429: publisher = {ACM},
430: address = {New York, NY, USA},
431: }
432:
433: @inproceedings{Colby-etal-pldi00,
434: author = {Colby, Christopher and Lee, Peter and Necula, George C. and Blau, Fred and Plesko, Mark and Cline, Kenneth},
435: title = {A certifying compiler for Java},
436: booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
437: year = {2000},
438: isbn = {1-58113-199-2},
439: pages = {95--107},
440: location = {Vancouver, British Columbia, Canada},
441: doi = {http://doi.acm.org/10.1145/349299.349315},
442: publisher = {ACM},
443: address = {New York, NY, USA},
444: }
445:
446: @inproceedings{Ne-pldi00,
447: author = {Necula, George C.},
448: title = {Translation validation for an optimizing compiler},
449: booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
450: year = {2000},
451: isbn = {1-58113-199-2},
452: pages = {83--94},
453: location = {Vancouver, British Columbia, Canada},
454: doi = {http://doi.acm.org/10.1145/349299.349314},
455: publisher = {ACM},
456: address = {New York, NY, USA},
457: }
458:
459: @book{Kn-lncs1428,
460: author = {Knoop, J.},
461: title = {Optimal Interprocedural Program Optimization: A new Framework
462: and its Application.},
463: publisher = {LNCS Tutorial 1428, Springer-V.},
464: year = {1998},
465: }
466:
467: @INPROCEEDINGS{LeeShrivastava09a,
468: TITLE = {Compiler-Managed Register File Protection for Energy-Efficient Soft Error Reduction},
469: AUTHOR = {Jongeun Lee and Aviral Shrivastava},
470: BOOKTITLE = {Asia and South-Pacific Design Automation Conference},
471: EDITOR = {Ren-Song Tsay},
472: PAGES = {618--623},
473: LOCATION = {Yokohama, Japan},
474: PUBLISHER = {IEEE,ACM},
475: MONTH = {January},
476: YEAR = {2009},
477: }
478:
479: @INPROCEEDINGS{LeeShrivastava09c,
480: TITLE = {A Compiler Optimization to Reduce Soft Errors in Register Files},
481: AUTHOR = {Jongeun Lee and Aviral Shrivastava},
482: BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems},
483: EDITOR = {Mahmut Kandemir},
484: PUBLISHER = {ACM},
485: PAGES = {41--49},
486: LOCATION = {Dublin, Ireland},
487: ADDRESS = {New York, NY, USA},
488: MONTH = {June},
489: YEAR = {2009},
490: }
491:
492: @inproceedings{Reis+05,
493: author = {George A. Reis and Jonathan Chang and Neil Vachharajani and Ram Rangan and David I. August},
494: title = {{SWIFT}: Software Implemented Fault Tolerance},
495: booktitle = {International Symposium on Code Generation and Optimization (CGO '05)},
496: year = {2005},
497: isbn = {0-7695-2298-X},
498: pages = {243--254},
499: publisher = {IEEE Computer Society},
500: address = {Washington, DC, USA},
501: }
502:
503: @inproceedings{WapplerMueller08,
504: author = {Ute Wappler and Martin M\"{u}ller},
505: title = {Software Protection Mechanisms for Dependable Systems},
506: booktitle = {Conference on Design, Automation and Test in Europe (DATE '08)},
507: year = {2008},
508: isbn = {978-3-9810801-3-1},
509: pages = {947--952},
510: location = {Munich, Germany},
511: publisher = {ACM},
512: address = {New York, NY, USA},
513: }
514:
515: @ARTICLE{Oh+02a,
516: title={Error detection by duplicated instructions in super-scalar processors},
517: author={Oh, N. and Shirvani, P.P. and McCluskey, E.J.},
518: journal={Reliability, IEEE Transactions on},
519: year={2002},
520: month={Mar},
521: volume={51},
522: number={1},
523: pages={63-75},
524: keywords={error detection, instruction sets, parallel architectures, software fault tolerance, software reliabilityconcurrent error detection, error detection by duplicated instructions, error-detection coverage, error-detection coverage estimation, execution time overhead, fault tolerance, fault-coverage, instruction-level parallelism, instruction-scheduling, instructions duplication, memory code segment fault, performance overhead reduction, probabilistic methods, registers, single event upset, software technique, super-scalar processors, system operation, transient fault},
525: doi={10.1109/24.994913},
526: ISSN={0018-9529}, }
527:
528: @ARTICLE{Oh+02b,
529: title={Control-flow checking by software signatures},
530: author={Oh, N. and Shirvani, P.P. and McCluskey, E.J.},
531: journal={Reliability, IEEE Transactions on},
532: year={2002},
533: month={Mar},
534: volume={51},
535: number={1},
536: pages={111-122},
537: keywords={program diagnostics, program testing, software reliabilityassigned signatures, branching fault injection experiment, branching faults, code size reduction, compilation time, control flow checking by software signatures, error detection instructions, execution time overhead reduction, instructions checking, multitasking environment, program graph, run-time signatures, signature monitoring techniques, software method, undetected incorrect outputs, watchdog task},
538: doi={10.1109/24.994926},
539: ISSN={0018-9529}, }
540:
541: @ARTICLE{Oh+02c,
542: title={Error detection by selective procedure call duplication for low energy consumption},
543: author={Nahmshuk Oh, Nahmshuk and Edward J. McCluskey},
544: journal={IEEE Transactions onReliability},
545: year={2002},
546: month={Dec},
547: volume={51},
548: number={4},
549: pages={ 392-402},
550: keywords={ error detection, fault tolerant computing, power consumption, software fault tolerance commercial off-the-shelf components, data integrity, energy consumption reduction, error detection, error-detection latency, error-detection overhead minimisation, fault tolerance, hardware fault-tolerant techniques, instruction duplication, low energy consumption, low energy technique, low power technique, procedure cloning, selective procedure call duplication, software error detection, system reliability improvement, system-on-chip design technique, transient errors detection},
551: doi={10.1109/TR.2002.804735},
552: ISSN={0018-9529}, }
553:
554: @BOOK{MishraDutt08,
555: TITLE = {Processor Description Languages},
556: AUTHOR = {Prabhat Mishra and Nikil Dutt (Editor)},
557: PUBLISHER = {Morgan Kaufmann},
558: YEAR = {2008},
559: }
560:
561: @InProceedings{BrooksTiwariMartonosi00,
562: author = "David Brooks and Vivek Tiwari and Margaret Martonosi",
563: title = "Wattch: {A} Framework for Architectural-Level Power
564: Analysis and Optimizations",
565: booktitle = "Proceedings of the 27th Annual International Symposium
566: on Computer Architecture",
567: location = "Vancouver, British Columbia",
568: organization = "IEEE Computer Society and ACM SIGARCH",
569: month = "June" # " 12--14,",
570: year = "2000",
571: pages = "83--94",
572: }
573:
574:
575: @InProceedings{SchrSchoKn09,
576: TITLE = "Adding Timing-Awareness to {AUTOSAR} Basic-Software - A Component Based Approach",
577: AUTHOR = "Dietmar Schreiner and Markus Schordan and Jens Knoop",
578: BOOKTITLE = "12th IEEE International Symposium on Object/component/service-oriented
579: Real-time distributed Computing (ISORC 2009)",
580: PUBLISHER = "IEEE",
581: ADDRESS = "Tokyo, Japan",
582: YEAR = "2009",
583: MONTH = "March",
584: PAGES = "288--292",
585: }
586:
587: @inproceedings{Prantl:WCET2009,
588: Address = {Dublin, Ireland},
589: Author = {Adrian Prantl and Jens Knoop and Raimund Kirner and Albrecht Kadlec and Markus Schordan},
590: Booktitle = {9th Intl. Workshop on Worst-Case Execution Time (WCET)
591: Analysis},
592: Month = {June 30},
593: Title = {From Trusted Annotations to Verified Knowledge},
594: Year = {2009},
595: URL = {http://costa.tuwien.ac.at/papers/wcet09.pdf}
596: }
597:
598: @inproceedings{Prantl:WLPE2008,
599: Address = {Udine, Italy},
600: Author = {Adrian Prantl and Jens Knoop and Markus Schordan and Markus Triska},
601: Booktitle = {The 18th Workshop on Logic-based methods in Programming Environments (WLPE 2008)},
602: Month = {December 12},
603: Title = {Constraint solving for high-level WCET analysis},
604: Year = {2008},
605: URL = {http://costa.tuwien.ac.at/papers/wlpe08.pdf}
606: }
607:
608: @InProceedings{prantl_et_al:DSP:2008:1661,
609: author = "Adrian Prantl and Markus Schordan and Jens Knoop",
610: title = "TuBound - {A} Conceptually New Tool for Worst-Case
611: Execution Time Analysis",
612: booktitle = "8th Intl. Workshop on Worst-Case Execution Time (WCET)
613: Analysis",
614: year = "2008",
615: editor = "Raimund Kirner",
616: publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
617: Germany",
618: address = "Dagstuhl, Germany",
619: URL = "http://drops.dagstuhl.de/opus/volltexte/2008/1661",
620: annote = "Keywords: Worst-case execution time (WCET) analysis,
621: Tool Chain, Flow Constraints, Source-To-Source",
622: ISBN = "978-3-939897-10-1",
623: note = "also published in print by Austrian Computer Society
624: (OCG) under ISBN 978-3-85403-237-3",
625: }
626:
627: @InProceedings{kirner_et_al:DSP:2008:1657,
628: author = "Raimund Kirner and Albrecht Kadlec and Adrian Prantl
629: and Markus Schordan and Jens Knoop",
630: title = "Towards a Common {WCET} Annotation Language: Essential
631: Ingredients",
632: booktitle = "8th Intl. Workshop on Worst-Case Execution Time (WCET)
633: Analysis",
634: year = "2008",
635: editor = "Raimund Kirner",
636: publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
637: Germany",
638: address = "Dagstuhl, Germany",
639: URL = "http://drops.dagstuhl.de/opus/volltexte/2008/1657",
640: annote = "Keywords: Worst-case execution time (WCET) analysis,
641: annotation languages, WCET annotation language
642: challenge",
643: ISBN = "978-3-939897-10-1",
644: note = "also published in print by Austrian Computer Society
645: (OCG) under ISBN 978-3-85403-237-3",
646: }
647:
648: @InProceedings{kirner_et_al:DSP:2007:1197,
649: author = "Raimund Kirner and Jens Knoop and Adrian Prantl and
650: Markus Schordan and Ingomar Wenzel",
651: title = "{WCET} Analysis: The Annotation Language Challenge",
652: booktitle = "7th Intl. Workshop on Worst-Case Execution Time (WCET)
653: Analysis",
654: year = "2007",
655: editor = "Christine Rochange",
656: publisher = "Internationales Begegnungs- und Forschungszentrum
657: f{"u}r Informatik (IBFI), Schloss Dagstuhl, Germany",
658: address = "Dagstuhl, Germany",
659: URL = "http://drops.dagstuhl.de/opus/volltexte/2007/1197",
660: annote = "Keywords: Worst-case execution time analysis, WCET,
661: path description, annotation language challenge,
662: expressiveness, convenience",
663: }
664:
665:
666: @InProceedings{knoop:DSP:2008:1575,
667: author = {Jens Knoop},
668: title = {Data-Flow Analysis for Multi-Core Computing Systems: A Reminder to Reverse Data-Flow Analysis},
669: booktitle = {Scalable Program Analysis},
670: year = {2008},
671: editor = {Florian Martin and Hanne Riis Nielson and Claudio Riva and Markus Schordan},
672: number = {08161},
673: series = {Dagstuhl Seminar Proceedings},
674: ISSN = {1862-4405},
675: publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
676: address = {Dagstuhl, Germany},
677: URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1575},
678: annote = {Keywords: Multi-core computing systems, scalable program analysis, reverse data-flow analysis, demand-driven data-flow analysis}
679: }
680:
681: @InProceedings{Gus:ISoLA2006,
682: author = {Jan Gustafsson},
683: title = {The {WCET} Tool Challenge 2006},
684: booktitle = {Preliminary Proc. 2nd International IEEE Symposium on Leveraging
685: Applications of Formal Methods, Verification and Validation},
686: year = {2006},
687: address = {Paphos, Cyprus},
688: month = {November},
689: pages = {248 - 249},
690: annote = {}
691: }
692:
693:
694: @inproceedings{Holsti:WCET2008,
695: Address = {Prague, Czech Republic},
696: Author = {Niklas Holsti and Jan Gustafsson and Guillem Bernat (eds.) and
697: Cl\'ement Ballabriga and Armelle Bonenfant and Roman Bourgade and
698: Hugues Cass\'e and Daniel Cordes and Albrecht Kadlec and
699: Raimund Kirner and Jens Knoop and Paul Lokuciejewski and
700: Nicholas Merriam and Marianne de Michiel and Adrian Prantl and
701: Bernhard Rieder and Christine Rochange and Pascal Sainrat and
702: Markus Schordan},
703: Booktitle = {Proc. 8th International Workshop on Worst-Case Execution Time Analysis (WCET 2008)},
704: Month = {July},
705: Title = {{WCET Tool Challenge 2008: Report}},
706: Year = {2008},
707: Pages = {149-171},
708: Publisher = {{\"Osterreichische Computer Gesellschaft}},
709: note = {ISBN: 978-3-85403-237-3},
710: URL = {http://costa.tuwien.ac.at/papers/wcet08-challenge.pdf}
711: }
712:
713: @Article{Wilhelm:TECS2008,
714: author = {Reinhard Wilhelm and Jakob Engblom and Andreas Ermedahl and Niklas Holsti and
715: Stephan Thesing and David Whalley and Guillem Bernat and Christian Ferdinand and
716: Reinhold Heckman and Tulika Mitra and Frank Mueller and Isabelle Puaut and
717: Peter Puschner and Jan Staschulat and Per Stenstrom},
718: title = {The Worst-Case Execution Time Problem - Overview of Methods
719: and Survey of Tools},
720: journal = {ACM Transactions on Embedded Computing Systems (TECS)},
721: year = {2008},
722: volume = {7},
723: number = {3},
724: OPTpages = {},
725: month = {Apr.},
726: annote = {http://www.artist-embedded.org/docs/Events/2007/MOTIVES/surveyTimingAnalysis_wilhelm.pdf}
727: }
728:
729: @InProceedings{XueK06,
730: title = "A Fresh Look at {PRE} as a Maximum Flow Problem",
731: author = "Jingling Xue and Jens Knoop",
732: bibdate = "2006-04-05",
733: bibsource = "DBLP,
734: http://dblp.uni-trier.de/db/conf/cc/cc2006.html#XueK06",
735: booktitle = "Compiler Construction, 15th International Conference,
736: {CC} 2006, Held as Part of the Joint European
737: Conferences on Theory and Practice of Software, {ETAPS}
738: 2006, Vienna, Austria, March 30-31, 2006, Proceedings",
739: publisher = "Springer",
740: year = "2006",
741: volume = "3923",
742: editor = "Alan Mycroft and Andreas Zeller",
743: ISBN = "3-540-33050-X",
744: pages = "139--154",
745: series = "Lecture Notes in Computer Science",
746: URL = "http://dx.doi.org/10.1007/11688839_13",
747: }
748:
749: @InProceedings{scholz04,
750: author = "Bernhard Scholz and Nigel Horspool and Jens Knoop",
751: title = "Optimizing for space and time usage with speculative
752: partial redundancy elimination",
753: booktitle = "LCTES '04: Proceedings of the 2004 ACM SIGPLAN/SIGBED
754: conference on Languages, Compilers, and Tools for Embedded Systems",
755: year = "2004",
756: ISBN = "1-58113-806-7",
757: pages = "221--230",
758: location = "Washington, DC, USA",
759: publisher = "ACM Press",
760: }
761:
762:
763: @InProceedings{HiKr03,
764: TITLE = "{VLIW} Operation Refinement for Reducing Energy Consumption",
765: AUTHOR = "Ulrich Hirnschrott and Andreas Krall",
766: BOOKTITLE = "International Symposium on System-on Chip",
767: PUBLISHER = "IEEE",
768: ADDRESS = "Tampere, Finland",
769: YEAR = "2003",
770: PAGES = "131--134",
771: }
772:
773: @Article{Krall+04micro,
774: author = {Andreas Krall and Ulrich Hirnschrott and Christian Panis and Ivan Pryanishnikov},
775: title = {x{DSP}core: {A} {C}ompiler-{B}ased {C}onfigureable {D}igital {S}ignal {P}rocessor},
776: journal = {IEEE Micro},
777: year = {2004},
778: OPTkey = {},
779: volume = {24},
780: number = {4},
781: pages = {67-78},
782: month = {July/August},
783: OPTnote = {},
784: OPTannote = {},
785: }
786:
787: @INPROCEEDINGS{FarKrStBrand06,
788: TITLE = {Effective Compiler Generation by Architecture Description},
789: AUTHOR = {Stefan Farfeleder and Andreas Krall and Edwin Steiner and Florian Brandner},
790: BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems},
791: EDITOR = {Koen De Bosschere},
792: PUBLISHER = {ACM},
793: PAGES = {145--152},
794: ADDRESS = {Ottawa},
795: MONTH = {June},
796: YEAR = {2006},
797: URL = {http://doi.acm.org/10.1145/1134650.1134671},
798: }
799:
800: @ARTICLE{PrKrHo06,
801: AUTHOR = {Ivan Pryanishnikov and Andreas Krall and Nigel Horspool},
802: TITLE = {Compiler Optimizations for Processors with {SIMD} Instructions},
803: JOURNAL = {Software---Practice and Experience},
804: PUBLISHER = {Wiley},
805: VOLUME = {37},
806: NUMBER = {1},
807: PAGES = {93--113},
808: YEAR = {2007},
809: URL = {http://www3.interscience.wiley.com/cgi-bin/fulltext/112783581/PDFSTART},
810: }
811:
812: @ARTICLE{FaKrHo07,
813: AUTHOR = {Stefan Farfeleder and Andreas Krall and Nigel Horspool},
814: TITLE = {Ultra Fast Cycle-Accurate Compiled Emulation of Inorder Pipelined Architectures},
815: JOURNAL = {Journal of Systems Architecture},
816: PUBLISHER = {Elsevier},
817: VOLUME = {53},
818: NUMBER = {8},
819: PAGES = {501--510},
820: YEAR = {2007},
821: }
822:
823: @INPROCEEDINGS{MeKr07,
824: TITLE = {Instruction Set Encoding Optimization for Code Size Reduction},
825: AUTHOR = {Michael Med and Andreas Krall},
826: BOOKTITLE = {International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation},
827: ADDRESS = {Samos, Greece},
828: PAGES = {9--17},
829: MONTH = {July},
830: YEAR = {2007}
831: }
832:
833: @INPROCEEDINGS{BrEbKr07,
834: TITLE = {Compiler Generation from Structural Architecture Descriptions},
835: AUTHOR = {Florian Brandner and Dietmar Ebner and Andreas Krall},
836: BOOKTITLE = {International Conference on Compilers, Architecture, and Synthesis for Embedded Systems},
837: ADDRESS = {Salzburg, Austria},
838: PAGES = {13--22},
839: MONTH = {September},
840: YEAR = {2007}
841: }
842:
843: @INPROCEEDINGS{EbBrSchKrWiKa08,
844: TITLE = {Generalized Instruction Selection using {SSA}-Graphs},
845: AUTHOR = {Dietmar Ebner and Florian Brandner and Bernhard Scholz and Andreas Krall and Peter Wiedermann and Albrecht Kadlec},
846: BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems},
847: EDITOR = {John Regehr},
848: PUBLISHER = {ACM},
849: PAGES = {31--40},
850: ADDRESS = {Tucson},
851: MONTH = {June},
852: YEAR = {2008},
853: }
854:
855: @INPROCEEDINGS{BrFeKrRi09,
856: TITLE = {Fast and Accurate Simulation using the LLVM Compiler Framework},
857: AUTHOR = {Florian Brandner and Andreas Fellnhofer and Andreas Krall and David Riegler},
858: BOOKTITLE = {Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO'09)},
859: EDITOR = {Smail Niar, Rainer Leupers, Olivier Temam},
860: PUBLISHER = {HiPEAC},
861: PAGES = {1--6},
862: ADDRESS = {Paphos, Cyprus},
863: MONTH = {January},
864: YEAR = {2009},
865: }
866:
867: @INCOLLECTION{BrHoKr09,
868: AUTHOR = {Florian Brandner and Nigel Horspool and Andreas Krall},
869: EDITOR = {Shuvra S. Bhattacharyya and Ed Deprettere and Rainer Leupers and Jarmo Takala},
870: BOOKTITLE = {Handbook on Signal Processing Systems},
871: TITLE = {DSP Instruction Set Simulation},
872: PUBLISHER = {Springer},
873: PAGES = {to appear},
874: MONTH = {December},
875: YEAR = {2009}
876: }
877:
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>
![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to res.bib CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [gforth] / res