TVOC: A translation validator for optimizing compilers. We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule permute; the second phase verifies structure-preserving optimizations using the proof rule Validate. Verification conditions are validated using the automatic theorem prover CVC Lite.

References in zbMATH (referenced in 20 articles , 1 standard article )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Barthe, Gilles; Crespo, Juan Manuel; Kunz, César: Beyond 2-safety: asymmetric product programs for relational program verification (2013)
  2. Blech, Jan Olaf; Grégoire, Benjamin: Certifying compilers using higher-order theorem provers as certificate checkers (2011)
  3. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  4. Siegel, Stephen F.; Zirkel, Timothy K.: FEVS: a functional equivalence verification suite for high-performance scientific computing (2011)
  5. Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin: Equality saturation: a new approach to optimization (2011)
  6. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  7. Tristan, Jean-Baptiste; Leroy, Xavier: A simple, verified validator for software pipelining (2010)
  8. Leroy, Xavier: A formally verified compiler back-end (2009)
  9. Saabas, Ando; Uustalu, Tarmo: Program and proof optimizations with type systems (2008)
  10. Tristan, Jean-Baptiste; Leroy, Xavier: Formal verification of translation validators, a case study on instruction scheduling optimizations (2008)
  11. Aspinall, David; Beringer, Lennart; Momigliano, Alberto: Optimisation validation. (2007)
  12. Barrett, Clark; de Moura, Leonardo; Stump, Aaron: Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) (2007)
  13. Fang, Yi; Zuck, Lenore D.: Improved invariant generation for tvoc. (2007)
  14. Kanade, Aditya; Sanyal, Amitabha; Khedker, Uday P.: Structuring optimizing transformations and proving them sound. (2007)
  15. Meyer, Thomas; Wolff, Burkhart: Tactic-based optimized compilation of functional programs (2006)
  16. Arons, Tamarah; Elster, Elad; Fix, Limor; Mador-Haim, Sela; Mishaeli, Michael; Shalev, Jonathan; Singerman, Eli; Tiemeyer, Andreas; Vardi, Moshe Y.; Zuck, Lenore D.: Formal verification of backward compatibility of microcode (2005)
  17. Balakrishnan, G.; Reps, T.; Kidd, N.; Lal, A.; Lim, J.; Melski, D.; Gruian, R.; Yong, S.; Chen, C.-H.; Teitelbaum, T.: Model checking x86 executables with CodeSurfer/x86 and WPDS++ (2005)
  18. Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore: TVOC: A translation validator for optimizing compilers (2005)
  19. Narasamdya, Iman; Voronkov, Andrei: Finding basic block and variable correspondence (2005)
  20. Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying: Translation and run-time validation of loop transformations (2005)