The code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully automatic tool for code validation, i.e., verifying that the target code produced by a code-generator (equivalently, a compiler or a translator) is a correct implementation of the source specification. This approach is a viable alternative to a full formal verification of the code-generator program, and has the advantage of not “freezing” the code generator design after verification. CVT was developed in the context of the ESPRIT project SACRES, and validates the translation from StateMate/Sildex mixed specification into C. The use of novel techniques based on uninterpreted functions and their analysis over a BDD-represented small model enables us to validate source specifications of several thousand lines, which represents a typical industrialsize safety-critical application.

References in zbMATH (referenced in 15 articles )

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

  1. Deng, Chaoqiang; Namjoshi, Kedar S.: Securing a compiler transformation (2018)
  2. Haxthausen, Anne E.; Peleska, Jan; Kinder, Sebastian: A formal approach for the construction and verification of railway control systems (2011)
  3. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  4. Tristan, Jean-Baptiste; Leroy, Xavier: A simple, verified validator for software pipelining (2010)
  5. Tristan, Jean-Baptiste; Leroy, Xavier: Formal verification of translation validators, a case study on instruction scheduling optimizations (2008)
  6. Clarke, Edmund; Jain, Himanshu; Kroening, Daniel: Verification of SpecC using predicate abstraction (2007)
  7. Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
  8. Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying: Translation and run-time validation of loop transformations (2005)
  9. Cousot, Patrick; Cousot, Radhia: Systematic design of program transformation frameworks by abstract interpretation (2002)
  10. Pnueli, Amir; Rodeh, Yoav; Strichman, Ofer; Siegel, Michael: The small model property: How small can it be? (2002)
  11. Cousot, Patrick; Cousot, Radhia: A case study in abstract interpretation based program transformation: blocking command elimination (2001)
  12. Goos, Gerhard; Zimmermann, Wolf: Verifying compilers and ASMs or ASMs for uniform description of multistep transformations (2000)
  13. Traverso, Paolo; Bertoli, Piergiorgio: Mechanized result verification: An industrial application (2000)
  14. Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer; Siegel, Michael: Deciding equality formulas by small domains instantiations (1999)
  15. Pnueli, A.; Shtrichman, O.; Siegel, M.: The code validation tool (CVT). Automatic verification of a compilation process (1998)