Re: [Valgrind-developers] V-Bit Verification

[Julian S. <js...@ac...>]

> improved and and the add rules are sound. We are currently working on
> verifying the rest of the rules as well. Verifying rules involves first
> converting the rules to SMT and then using a SMT solver to prove its
> correctness against the model.

Is it possible to use your machinery to generate sets of test cases, maybe
pseudo-random, that can be used to test the code?  As I mentioned before,
formal proofs are nice, but by themselves are of limited usefulness in the
scenario where the validated code base is in a state of change / maintenance.

J