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