|
72773.
|
|
|
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
|
|
|
Why est une interface de générateur de vérification de conditions (VCG[nbsp] : verification conditions generator) pour d'autres outils de vérification. Il utilise un langage puissant incluant des fonctions d'ordre supérieur, le polymorphisme, les références, les tableaux et les exceptions. Il construit des obligations de preuve pour plusieurs systèmes[nbsp] : les assistants de preuve Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar et les procédures de décision Simplify, Alt-Ergo, Yices, CVC Lite et haRVey.
|