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 MHonArc.