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 21 articles )

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

1 2 next

  1. Haxthausen, Anne E.; Peleska, Jan; Kinder, Sebastian: A formal approach for the construction and verification of railway control systems (2011)
  2. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  3. Tristan, Jean-Baptiste; Leroy, Xavier: A simple, verified validator for software pipelining (2010)
  4. Tristan, Jean-Baptiste; Leroy, Xavier: Formal verification of translation validators, a case study on instruction scheduling optimizations (2008)
  5. Clarke, Edmund; Jain, Himanshu; Kroening, Daniel: Verification of SpecC using predicate abstraction (2007)
  6. Fang, Yi; Zuck, Lenore D.: Improved invariant generation for tvoc. (2007)
  7. Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
  8. Glesner, Sabine; Forster, Simone; Jäger, Matthias: A program result checker for the lexical analysis of the GNU C compiler. (2005)
  9. Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying: Translation and run-time validation of loop transformations (2005)
  10. Barrett, Clark W.; Goldberg, Benjamin; Zuck, Lenore D.: Run-time validation of speculative optimizations using CVC. (2003)
  11. Cousot, Patrick; Cousot, Radhia: Systematic design of program transformation frameworks by abstract interpretation (2002)
  12. Glesner, Sabine; Geiß, Rubino; Boesler, Boris: Verified code generation for embedded systems. (2002)
  13. Pnueli, Amir; Rodeh, Yoav; Strichman, Ofer; Siegel, Michael: The small model property: How small can it be? (2002)
  14. Zuck, Lenore D.; Pnueli, Amir; Fang, Yi; Goldberg, Benjamin: VOC: A translation validator for optimizing compilers. (2002)
  15. Zuck, Lenore D.; Pnueli, Amir; Fang, Yi; Goldberg, Benjamin; Hu, Ying: Translation and run-time validation of optimized code. (2002)
  16. Cousot, Patrick; Cousot, Radhia: A case study in abstract interpretation based program transformation: Blocking command elimination. (2001)
  17. Cousot, Patrick; Cousot, Radhia: A case study in abstract interpretation based program transformation: blocking command elimination (2001)
  18. Goos, Gerhard; Zimmermann, Wolf: Verifying compilers and ASMs or ASMs for uniform description of multistep transformations (2000)
  19. Traverso, Paolo; Bertoli, Piergiorgio: Mechanized result verification: An industrial application (2000)
  20. Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer; Siegel, Michael: Deciding equality formulas by small domains instantiations (1999)

1 2 next