--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of linked list



Hello,

2015-03-10 5:05 GMT+01:00 Wenrui Meng <wenrui at seas.upenn.edu>:
>
> I didn't find much related examples resource for beginner. Can any one point
> out examples by WP plug?
>

I forgot that I had been mad enough to attempt such a thing, but you
can find here
https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial:lifo-2014

the material of the seminar that I gave at Orl?ans University last
October, which includes a example on a search on binary trees. Note
that the intermediate lemmas cannot currently be proved, as WP
generates an incomplete axiomatization of the inductive predicates.

** Disclaimer: what follows here is quite technical, you can skip it
in a first reading**
More precisely, WP does not take into account the fact that such
predicates are least fixpoints, in the sense that to establish that
P(x) is true, one of the cases in the inductive definition has to
hold. Reportedly, generating such inversion axioms tends to confuse
automated theorem provers, but the Coq output could be enhanced to
take inductive predicates fully into account. Failing that, it is not
possible to complete the proof (writing explicitely the missing axioms
will be needed at some point).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile