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] Using frama-c to verify coding patterns of concurrent sw

Hello,

2013/7/1 Teig, Oyvind              CCS <Oyvind.Teig at autronicafire.no>:

>
> ?        Is it possible to set up an ACSL specification that would be able
> to verify that certain combinations of local state variables _now_ and
> certain other combinations _later_ on will sooner or later arrive?
>
> ?        Even more than that: I will need to verify more than two steps!
>
> www.teigfam.net/oyvind/home/ (also work-related)

I think that you might be interested by the Aora? plug-in
(http://frama-c.com/aorai.html and
http://amazones.gforge.inria.fr/aorai/), that generate ACSL
specifications from an automaton describing the sequences of function
calls that are authorized for the program. Be aware though that it is
still a quite experimental plug-in. Some extensions might be devised
inside the FP7 project Stance and the ITEA project OpenETCS, but as
usual, we'd be happy to start further collaborations around the
subject.

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