Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] z3 failure


Le 09/10/2013 14:30, cok at frontiernet.net a ?crit :
> *** So I would encourage anyone working with model checking/SW
> verification/theorem proving tools to submit translations of their
> problems into SMT as new benchmarks. ***

I understand that my initial comment was a bit harsh and polemic, but
I'm glad to see that it generates an interesting discussion.

I unfortunately had a bad experience in sending a collection of
benchmarks a few years ago. I took the complete set of files that were
generated by Frama-C/Jessie/Why (Why2 at that time) in SMT (v1) format
and proposed that as is. This amounted to thousands of examples, but
most of them were "trivial": indeed, in practice a lot of VCs are
generated and a lot of them are simple. Then, during the next
competition, something like 10 files were selected from this set, and of
course all of them were trivial so useless to compare provers.

Thus proposing a collection of benchmarks is not a matter of sending all
the files you can keep on your computer as is, a selection must be made.
But how to do that ? And whatever the criteria chosen, filtering the
files will be a time-consuming effort...

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |