--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2013 ---
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