Institut National des Sciences Appliquéees Inrialpes
Aoraï plug-in (Aka LTL to ACSL)

The Aoraï plug-in for Frama-C provides a method to automatically annotate a C program according to an LTL formula F such that, if the annotations are verified, then we ensure that the program respects F.

The classical method to validate annotations is to use the Jessie plug-in and the Why tool.


The plug-in source code is available in the resources section. In order to install this plug-in, you need to have the Frama-C framework.

If you want to use LTL syntax for properties, then you have to install the ltl2ba tool in your current path. This tool is distributed under the GPL licence and converts a LTL formula into a Büchi automaton. You can find this tool on the homepage of its author Paul Gastin (ENS Cachan).


The plug-in is activated with one of the following command lines:

frama-c file.c -aorai-ltl file.ltl
frama-c file.c -aorai-automata file.ya
These two commands differ only by the syntax used to express to property to verify: .ltl files are described in a ltl like syntax, while .ya are description of automata in a yacc-like syntax.

Options are:

Gives some information during computation, such as used/produced files and heuristics applied
Displays, at the end of the process, the computed specification of each operation, in terms of Büchi states and transitions.
Generates a dot file of the Büchi automaton. Dot is a graph format used by the GraphViz tool.
if set, considers acceptation states (Only on finite traces). If not, only the safty is verified.
Gives the whole list of options
Ressources (Last update: 25-02-2011 - 15:40:44)
Known Restrictions

Currently, the switch statement is not supported and only the safety part of the LTL formula is check. The variant generation is a future for the implementation.


For any questions, remarks or suggestions, please contact   (CITI Labs, AMAZONES team).

End Note: to the question "Why this name: Aoraï ?" my answer is: why not ? Aoraï is the name of the taller reachable mount in the Tahiti island and its reachability is not always obvious.

Valid HTML 4.01!   Any browser!   Valid CSS!