--- layout: fc_discuss_archives title: Message 129 from Frama-C-discuss on December 2009 ---
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