--- layout: fc_discuss_archives title: Message 129 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Debugging huge theories



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