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] Debugging huge theories

  • Subject: [Frama-c-discuss] Debugging huge theories
  • From: yegor.derevenets at gmail.com (Yegor Derevenets)
  • Date: Tue, 22 Dec 2009 04:50:17 +0300
Hello, All!

There is an implementation of hsearch function described here:
http://www.opengroup.org/onlinepubs/000095399/functions/hsearch.html

This implementation to be verified (with some ACSL code) is present here:
http://www.vsi.ru/~yegor/tmp/hsearch.c

In order to decrease the size of theory the hsearch function was split
into two functions: compute_hash and hsearch (the rest).

As you see, hsearch function has many behaviour cases with
complicated conditions in assumes and ensures clauses.

Originally verification was to be done completely in PVS, but it
seems to be whole life-consuming task to prove 21mb of lemmas
in PVS. Partially, because he almost dies for several hours garbage
collecting trying to parse files with hundreds of lemmas.

It looks like the only choice left is automatic provers.
Simplify proves about 87% of lemmas.
Alt-Ergo proves several of those not proved by Simplify.

Any ideas on proving what has left?
Here it's not the case, when one (or at least I) can have a look
at failed statement and understand why it's wrong.

My specification definitely misses variant and invariant for
do-while loop in hsearch(), but since Simplify generates
counter-examples, there are also false statements,
gWhy can show me them in beautiful GUI, but what's next?

Are there any approaches to debugging big not-very-obvious
theories like this?

-- 
Yegor Derevenets