Re: [isabelle] 3 Papers Available
Am 15.03.2012 um 13:39 schrieb Thomas Genet:
> Dear all,
> Le 14/03/12 18:39, Burkhart Wolff a écrit :
> > Dear all,
> > here are 3 new papers concerning "Isabelle and Testing/Refinement":
> maybe this is naive question, but how do HOL-testgen behaves w.r.t. quickcheck and nitpick tools of Isabelle/HOL?
HOL-TestGen follows a completely independent symbolic approach to test-case generation (via normalization)
and test data selection. It has nothing to do with nitpick (essentially: counter-example generation for finitized
interpretations of a formula), but uses potentially quickcheck and smt (i.e. Z3) in the test data selection phase.
> Is it likely to succeed to find a counterexample where a typical
> quickcheck [tester=narrowing]
> call fails?
That depends from the application domain.
I can not make any statistical guessing here.
For the problems we are mostly using it -
model-based testing in security related domains -
there is no hope that the finitized interpretation method
does any good, though.
This archive was generated by a fusion of
Pipermail (Mailman edition) and