Verification tool are used to check some important property of
critical applications. However, when a tool answers that the property
holds, the criticality has only been shifted from the the application
to the verification tool. We considered the general case of a fixpoint
computation for a transition system R. The fixpoint Phi
is computed by a tool that possibly contains bugs. Then, our goal is
to ensure the correctness of the result, independantly of the
correctness of the tool. Thus, we prove that Phi is a fixpoint of R:
forall s,s':States, Phi(s) /\ R(s,s') ==> Phi(s')
In order to guaranty that this property holds, it is far from being
possible to prove the correctness of the implementation of the
fixpoint computation. However, for a given fixpoint Phi and
transition system R, it is amenable to generate a correctness
proof for a proofchecker like COQ or PVS. Then, the correctness of
the answer no more depends on the verification tool but on the
proofchecker.
Assuming that the proof trees use inference rules of a mathematical
inference system that has been proved correct, the confidence only
depends on the implementation of the proofchecker. Its task  the
utlimate verification  consists in cehcking that the applications of
the rules respects the syntactical constraints of wellformedness of
the tree.
Most of the automatic verification tool compute a fixpoint, based on
which it concludes that the property is satisfied or not.
By instrumenting the verification tool, it is possible to
automatically provide a proof that the stable point reached is
actually a fixpoint.
We run one more time the fixpoint computation starting with the
current fixpoint and we generate the proof that the states reached by
R already appear in the fixpoint.
This approach has been successfully used in the case of HERMES, a
verification tool for secrecy properties in cryptographic protocols
