TVOC

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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

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

  1. Namjoshi, Kedar S.; Xue, Anton: A self-certifying compilation framework for WebAssembly (2021)
  2. Barthe, Gilles; Crespo, Juan Manuel; Kunz, César: Product programs and relational program logics (2016)
  3. Barthe, Gilles; Crespo, Juan Manuel; Kunz, César: Beyond 2-safety: asymmetric product programs for relational program verification (2013)
  4. Blech, Jan Olaf; Grégoire, Benjamin: Certifying compilers using higher-order theorem provers as certificate checkers (2011)
  5. Siegel, Stephen F.; Zirkel, Timothy K.: FEVS: a functional equivalence verification suite for high-performance scientific computing (2011)
  6. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  7. Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin: Equality saturation: a new approach to optimization (2011)
  8. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  9. Tristan, Jean-Baptiste; Leroy, Xavier: A simple, verified validator for software pipelining (2010)
  10. Leroy, Xavier: A formally verified compiler back-end (2009)
  11. Saabas, Ando; Uustalu, Tarmo: Program and proof optimizations with type systems (2008)
  12. Tristan, Jean-Baptiste; Leroy, Xavier: Formal verification of translation validators, a case study on instruction scheduling optimizations (2008)
  13. Barrett, Clark; de Moura, Leonardo; Stump, Aaron: Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) (2007)
  14. Meyer, Thomas; Wolff, Burkhart: Tactic-based optimized compilation of functional programs (2006)
  15. 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)
  16. 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)
  17. Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore: TVOC: A translation validator for optimizing compilers (2005)
  18. Narasamdya, Iman; Voronkov, Andrei: Finding basic block and variable correspondence (2005)
  19. Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying: Translation and run-time validation of loop transformations (2005)
  20. Zuck, L.; Pnueli, A.; Fang, Y.; Goldberg, B.: Voc: a methodology for the translation validation of optimizingcompilers (2003) ioport