| @article{Hoare, |
@article{Hoare03, |
| author = {Tony Hoare}, |
author = {Tony Hoare}, |
| title = {The verifying compiler: A grand challenge for computing research}, |
title = {The verifying compiler: A grand challenge for computing research}, |
| journal = {Journal of the ACM}, |
journal = {Journal of the ACM}, |
| address = {New York, NY, USA}, |
address = {New York, NY, USA}, |
| } |
} |
| |
|
| @article{1328444, |
@inproceedings{TristanLeroy09, |
| |
author = {Jean-Baptiste Tristan and Xavier Leroy}, |
| |
title = {Verified Validation of Lazy Code Motion}, |
| |
booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation}, |
| |
year = {2009}, |
| |
isbn = {978-1-60558-392-1}, |
| |
pages = {316--326}, |
| |
location = {Dublin, Ireland}, |
| |
doi = {http://doi.acm.org/10.1145/1542476.1542512}, |
| |
publisher = {ACM}, |
| |
address = {New York, NY, USA}, |
| |
} |
| |
|
| |
@inproceedings{Kundu+09, |
| |
author = {Sudipta Kundu and Zachary Tatlock and Sorin Lerner}, |
| |
title = {Proving Optimizations Correct using Parameterized Program Equivalence}, |
| |
booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation}, |
| |
year = {2009}, |
| |
isbn = {978-1-60558-392-1}, |
| |
pages = {327--337}, |
| |
location = {Dublin, Ireland}, |
| |
doi = {http://doi.acm.org/10.1145/1542476.1542513}, |
| |
publisher = {ACM}, |
| |
address = {New York, NY, USA}, |
| |
} |
| |
|
| |
@inproceedings{Necula00, |
| |
author = {George C. Necula}, |
| |
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}, |
| |
} |
| |
|
| |
@article{TristanLeroy08, |
| author = {Jean-Baptiste Tristan and Xavier Leroy}, |
author = {Jean-Baptiste Tristan and Xavier Leroy}, |
| title = {Formal verification of translation validators: a case study on instruction scheduling optimizations}, |
title = {Formal verification of translation validators: a case study on instruction scheduling optimizations}, |
| journal = {SIGPLAN Not.}, |
journal = {SIGPLAN Not.}, |
| address = {New York, NY, USA}, |
address = {New York, NY, USA}, |
| } |
} |
| |
|
| @article{1314860, |
@inproceedings{ZaksPnueli08, |
| |
author = {Anna Zaks and Amir Pnueli}, |
| |
title = {Program Analysis for Compiler Validation}, |
| |
booktitle = {PASTE '08: Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering}, |
| |
year = {2008}, |
| |
isbn = {978-1-60558-382-2}, |
| |
pages = {1--7}, |
| |
location = {Atlanta, Georgia}, |
| |
doi = {http://doi.acm.org/10.1145/1512475.1512477}, |
| |
publisher = {ACM}, |
| |
address = {New York, NY, USA}, |
| |
} |
| |
|
| |
@inproceedings{Pnueli98b, |
| |
author = {Amir Pnueli and Michael Siegel and Eli Singerman}, |
| |
title = {Translation Validation}, |
| |
booktitle = {TACAS '98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems}, |
| |
year = {1998}, |
| |
isbn = {3-540-64356-7}, |
| |
pages = {151--166}, |
| |
publisher = {Springer-Verlag}, |
| |
address = {London, UK}, |
| |
} |
| |
|
| |
@Article{Pnueli98a, |
| |
author = "Amir Pnueli and Ofer Shtrichman and Michael Siegel", |
| |
title = "The {Code Validation Tool (CVT)}: Automatic |
| |
verification of a compilation process", |
| |
journal = "International Journal on Software Tools for Technology |
| |
Transfer (STTT)", |
| |
volume = "2", |
| |
number = "2", |
| |
pages = "192--201", |
| |
month = "December", |
| |
year = "1998", |
| |
ISSN = "1433-2779 (print), 1433-2787 (electronic)", |
| |
} |
| |
|
| |
@article{GlesnerGoosZimmeermann04, |
| |
author = {Sabine Glesner and |
| |
Gerhard Goos and |
| |
Wolf Zimmermann}, |
| |
title = {Verifix: Konstruktion und Architektur verifizierender {\"U}bersetzer |
| |
(Verifix: Construction and Architecture of Verifying Compilers)}, |
| |
journal = {it - Information Technology}, |
| |
volume = {46}, |
| |
number = {5}, |
| |
year = {2004}, |
| |
pages = {265-276}, |
| |
ee = {http://dx.doi.org/10.1524/itit.46.5.265.44799}, |
| |
bibsource = {DBLP, http://dblp.uni-trier.de} |
| |
} |
| |
|
| |
@inproceedings{GoosZimmermann00, |
| |
author = {Gerhard Goos and Wolf Zimmermann}, |
| |
title = {Verifying Compilers and ASMs}, |
| |
booktitle = {Abstract State Machines}, |
| |
editor = {Yuri Gurevich and |
| |
Philipp W. Kutter and |
| |
Martin Odersky and |
| |
Lothar Thiele}, |
| |
year = {2000}, |
| |
pages = {177-202}, |
| |
publisher = {Springer}, |
| |
series = {Lecture Notes in Computer Science}, |
| |
volume = {1912}, |
| |
} |
| |
|
| |
@article{BlechPoetzsch07, |
| author = {Jan Olaf Blech and Arnd Poetzsch-Heffter}, |
author = {Jan Olaf Blech and Arnd Poetzsch-Heffter}, |
| title = {A Certifying Code Generation Phase}, |
title = {A Certifying Code Generation Phase}, |
| journal = {Electron. Notes Theor. Comput. Sci.}, |
journal = {Electron. Notes Theor. Comput. Sci.}, |
