--- res/res.bib 2009/06/28 15:01:57 1.5 +++ res/res.bib 2009/06/29 06:50:40 1.6 @@ -1,3 +1,178 @@ + + @article{1328444, + author = {Jean-Baptiste Tristan and Xavier Leroy}, + title = {Formal verification of translation validators: a case study on instruction scheduling optimizations}, + journal = {SIGPLAN Not.}, + volume = {43}, + number = {1}, + year = {2008}, + issn = {0362-1340}, + pages = {17--27}, + doi = {http://doi.acm.org/10.1145/1328897.1328444}, + publisher = {ACM}, + address = {New York, NY, USA}, + } + +@inproceedings{KRS-pldi92, + author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, + title = {Lazy Code Motion}, + booktitle = "Proc. ACM SIGPLAN Conf. on + Prog. Lang. Design and Impl. + $($PLDI'92$)$", + series = {{ACM SIGPLAN} Not.}, + volume = {{\em 27},7}, + year = {1992}, + pages = {224 - 234} + } + +@inproceedings{KRS-retrolcm04, + author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, + title = {{\sc Retrospective}: Lazy Code Motion}, + booktitle = "``20 Years of the ACM SIGPLAN Conference on + Programming Language Design and + Implementation (1979 - 1999): A Selection''", + series = {{ACM SIGPLAN} Not.}, + volume = {{\em 39},4}, + year = {2004}, + pages = {460 - 461 \& 462 - 472} + } + +@inproceedings{KRS-pldi94, + author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, + title = {Partial Dead Code Elimination}, + booktitle = "Proc. ACM SIGPLAN Conf. on + Prog. Lang. Design and Impl. + $($PLDI'94$)$", + series = {{ACM SIGPLAN} Not.}, + volume = {{\em 29},6}, + year = {1994}, + pages = {147 - 158} + } + + + +@inproceedings{RKS-popl00, + author = {R\"uthing, O. and Knoop, J. and Steffen, B.}, + title = {Sparse Code Motion}, + booktitle = "Conf. Rec. 27th Annual + Symp. on Principles of Prog. Lang. + $($POPL'00$)$", + publisher = "ACM, NY", + year = {2000}, + pages = {170 - 183}, +} + +@book{MMO-lncs1283, + author = {M\"uller-Olm, M.}, + title = {Modular Compiler Verification}, + publisher = {LNCS 1283, Springer-V.}, + year = {1996}, +} + +@Misc{CompCert, + key = {CompCert}, + author = {Leroy, X.}, + title = {The Compcert verified compiler}}, + howpublished = {\url{http://compcert.inria.fr/doc/index.html}}, + year = {2005 - 2008}, + note = {CompCert is funded by ANR (grant number ANR-05-SSIA-0019), + as part of the ARA SSIA programme.} +} + +@inproceedings{Le-popl06, + author = {Leroy, X.}, + title = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant}, + booktitle = "Conf. Rec. 33rd Annual + Symp. on Principles of Prog. Lang. + $($POPL'06$)$", + publisher = "ACM, NY", + year = {2006}, +} + +@InProceedings{BDL-fm06, + author = "Blazy, S. and Dargaye, Z. and Leroy, X.", + title = {Formal verification of a C compiler front-end}, + booktitle = "{Formal Methods 2006}", + year = 2006, + volume = 4085, + series = {LNCS}, + publisher = springer +} + +@Article{Langmaack97a, + Author = {Langmaack, Hans}, + Title = {{Softwareengineering zur Zertifizierung von + Systemen: Spezifikations-, Implementierungs-, + \"Ubersetzerkorrektheit}}, + Journal = {Informationstechnik und Technische + Informatik it-ti}, + Pages = {41-47}, + Number = 3, + Volume = 97, + Publisher = {Oldenbourg Verlag}, + Year = 1997, +} + +@InProceedings{Goerigk-et-al:CC96, + Author = {W. Goerigk and A. Dold and T. Gaul and G. Goos and + A. Heberle and F. von Henke and U. Hoffmann and + H. Langmaack and H. Pfeifer and H. Ruess and W. Zimmermann}, + Title = "{C}ompiler {C}orrectness and {I}mplementation + {V}erification: {T}he {V}erifix {A}pproach", + BookTitle = {Proceedings of the Poster Session of CC'96 - + International Conference on Compiler Construction }, + Editor = {P. Fritzson}, + Publisher = {ida}, + Year = {1996}, + Note = {TR-Nr.: R-96-12}, + Pages = {65 -- 73}, +} + + +@Article{Langmaack96a, + Author = {Langmaack, H.}, + Title = {{The ProCoS Approach to Correct Systems}}, + Journal = {Real Time Systems}, + Volume = {13}, + Pages = {253-275}, + Publisher = {Kluwer Academic Publishers}, + Year = 1997 +} + + +@InProceedings{Goos:00:ASM, + author = "Gerhard Goos and + Wolf Zimmermann", + title = {Verifying Compilers and ASMs}, + booktitle = "{Abstract State Machines, Theory and Applications}", + year = 2000, + pages = {177-202}, + editor = {Yuri Gurevich and Philipp W. Kutter and + Martin Odersky and Lothar Thiele}, + volume = 1912, + series = {LNCS}, + publisher = springer +} + +@InCollection{Goos:99:verifix, + author = {Gerhard Goos and Wolf Zimmermann}, + title = {Verification of Compilers}, + booktitle = {Correct System Design}, + pages = {201-230}, + publisher = {Springer-Verlag}, + year = 1999, + editor = {Bernhard Steffen and Ernst Rüdiger Olderog}, + volume = 1710, + series = {LNCS} +} + +@book{Po-lncs124, + author = {Polak, W.}, + title = {Compiler Specification and Verification.}, + publisher = {LNCS 124, Springer-V.}, + year = {1981}, +} + @article{Hoare03, author = {Tony Hoare}, title = {The verifying compiler: A grand challenge for computing research}, @@ -64,6 +239,32 @@ publisher = {ACM}, address = {New York, NY, USA}, } + +@inproceedings{FNSG-tlfi07, + author = {Feng, Xinyu and Ni, Zhaozhong and Shao, Zhong and Guo, Yu}, + title = {An open framework for foundational proof-carrying code}, + booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation}, + year = {2007}, + isbn = {1-59593-393-X}, + pages = {67--78}, + location = {Nice, Nice, France}, + doi = {http://doi.acm.org/10.1145/1190315.1190325}, + publisher = {ACM}, + address = {New York, NY, USA}, + } + +@inproceedings{AF-popl00, + author = {Appel, Andrew W. and Felty, Amy P.}, + title = {A semantic model of types and machine instructions for proof-carrying code}, + booktitle = {POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + year = {2000}, + isbn = {1-58113-125-9}, + pages = {243--253}, + location = {Boston, MA, USA}, + doi = {http://doi.acm.org/10.1145/325694.325727}, + publisher = {ACM}, + address = {New York, NY, USA}, + } @inproceedings{ZaksPnueli08, author = {Anna Zaks and Amir Pnueli}, @@ -134,6 +335,7 @@ } @article{BlechPoetzsch07, + author = {Jan Olaf Blech and Arnd Poetzsch-Heffter}, title = {A Certifying Code Generation Phase}, journal = {Electron. Notes Theor. Comput. Sci.}, @@ -160,6 +362,77 @@ address = {New York, NY, USA}, } +@inproceedings{PSS-tacas98, + author = {Pnueli, A. and Siegel, M. and Singermann, E.}, + title = {Translation Validation}, + booktitle = {Proc. 4th Int. Conf. on Tools and + Algorithms for the Construction and Analysis of Systems + $($TACAS'98$)$}, + publisher = {Springer-V.}, + series = "LNCS 1384", + year = {1998}, + pages = {151 - 166} + } + +@inproceedings{Ne-popl97, + author = {Necula, G. C.}, + title = {Proof-Carrying Code}, + booktitle = "Conf. Rec. 24th Annual + Symp. on Principles of Prog. Lang. + $($POPL'97$)$", + publisher = "ACM, NY", + year = {1997}, + pages = {106 - 119}, +} + +@article{NL-pldi98, + author = {Necula, George C. and Lee, Peter}, + title = {The design and implementation of a certifying compiler}, + journal = {SIGPLAN Not.}, + volume = {33}, + number = {5}, + year = {1998}, + issn = {0362-1340}, + pages = {333--344}, + doi = {http://doi.acm.org/10.1145/277652.277752}, + publisher = {ACM}, + address = {New York, NY, USA}, + } + +@inproceedings{Colby-etal-pldi00, + author = {Colby, Christopher and Lee, Peter and Necula, George C. and Blau, Fred and Plesko, Mark and Cline, Kenneth}, + title = {A certifying compiler for Java}, + booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation}, + year = {2000}, + isbn = {1-58113-199-2}, + pages = {95--107}, + location = {Vancouver, British Columbia, Canada}, + doi = {http://doi.acm.org/10.1145/349299.349315}, + publisher = {ACM}, + address = {New York, NY, USA}, + } + +@inproceedings{Ne-pldi00, + author = {Necula, George C.}, + title = {Translation validation for an optimizing compiler}, + booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation}, + year = {2000}, + isbn = {1-58113-199-2}, + pages = {83--94}, + location = {Vancouver, British Columbia, Canada}, + doi = {http://doi.acm.org/10.1145/349299.349314}, + publisher = {ACM}, + address = {New York, NY, USA}, + } + +@book{Kn-lncs1428, + author = {Knoop, J.}, + title = {Optimal Interprocedural Program Optimization: A new Framework + and its Application.}, + publisher = {LNCS Tutorial 1428, Springer-V.}, + year = {1998}, +} + @INPROCEEDINGS{LeeShrivastava09a, TITLE = {Compiler-Managed Register File Protection for Energy-Efficient Soft Error Reduction}, AUTHOR = {Jongeun Lee and Aviral Shrivastava}, @@ -280,6 +553,17 @@ ISSN={0018-9529}, } PAGES = "288--292", } +@inproceedings{Prantl:WCET2009, + Address = {Dublin, Ireland}, + Author = {Adrian Prantl and Jens Knoop and Raimund Kirner and Albrecht Kadlec and Markus Schordan}, + Booktitle = {9th Intl. Workshop on Worst-Case Execution Time (WCET) + Analysis}, + Month = {June 30}, + Title = {From Trusted Annotations to Verified Knowledge}, + Year = {2009}, + URL = {http://costa.tuwien.ac.at/papers/wcet09.pdf} +} + @inproceedings{Prantl:WLPE2008, Address = {Udine, Italy}, Author = {Adrian Prantl and Jens Knoop and Markus Schordan and Markus Triska}, @@ -363,7 +647,55 @@ ISSN={0018-9529}, } annote = {Keywords: Multi-core computing systems, scalable program analysis, reverse data-flow analysis, demand-driven data-flow analysis} } -@InProceedings{conf/cc/XueK06, +@InProceedings{Gus:ISoLA2006, + author = {Jan Gustafsson}, + title = {The {WCET} Tool Challenge 2006}, + booktitle = {Preliminary Proc. 2nd International IEEE Symposium on Leveraging + Applications of Formal Methods, Verification and Validation}, + year = {2006}, + address = {Paphos, Cyprus}, + month = {November}, + pages = {248 - 249}, + annote = {} +} + + +@inproceedings{Holsti:WCET2008, + Address = {Prague, Czech Republic}, + Author = {Niklas Holsti and Jan Gustafsson and Guillem Bernat (eds.) and + Cl\'ement Ballabriga and Armelle Bonenfant and Roman Bourgade and + Hugues Cass\'e and Daniel Cordes and Albrecht Kadlec and + Raimund Kirner and Jens Knoop and Paul Lokuciejewski and + Nicholas Merriam and Marianne de Michiel and Adrian Prantl and + Bernhard Rieder and Christine Rochange and Pascal Sainrat and + Markus Schordan}, + Booktitle = {Proc. 8th International Workshop on Worst-Case Execution Time Analysis (WCET 2008)}, + Month = {July}, + Title = {{WCET Tool Challenge 2008: Report}}, + Year = {2008}, + Pages = {149-171}, + Publisher = {{\"Osterreichische Computer Gesellschaft}}, + note = {ISBN: 978-3-85403-237-3}, + URL = {http://costa.tuwien.ac.at/papers/wcet08-challenge.pdf} +} + +@Article{Wilhelm:TECS2008, + author = {Reinhard Wilhelm and Jakob Engblom and Andreas Ermedahl and Niklas Holsti and + Stephan Thesing and David Whalley and Guillem Bernat and Christian Ferdinand and + Reinhold Heckman and Tulika Mitra and Frank Mueller and Isabelle Puaut and + Peter Puschner and Jan Staschulat and Per Stenstrom}, + title = {The Worst-Case Execution Time Problem - Overview of Methods + and Survey of Tools}, + journal = {ACM Transactions on Embedded Computing Systems (TECS)}, + year = {2008}, + volume = {7}, + number = {3}, + OPTpages = {}, + month = {Apr.}, + annote = {http://www.artist-embedded.org/docs/Events/2007/MOTIVES/surveyTimingAnalysis_wilhelm.pdf} +} + +@InProceedings{XueK06, title = "A Fresh Look at {PRE} as a Maximum Flow Problem", author = "Jingling Xue and Jens Knoop", bibdate = "2006-04-05",