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] 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