[PUBLIC HI-LITE] report on the 2nd annual meeting

Yannick Moy moy at adacore.com
Fri Jun 1 18:07:08 CEST 2012


We had a very successful meeting on Tuesday, with 25 people attending. I 
have put the slides of CEA and Astrium presentations, as well as those 
for the official consortium presentation to the authorities, on Hi-Lite 
website:

http://www.open-do.org/projects/hi-lite/progress/

- David Lesens (Astrium) and David Mentré (MERCE) reported on their use 
of gnatprove/gnattest tools. Both presentations emphasized the utility 
of IDE integration, and what needs to be done to support their 
industrial use cases (add support for some Ada features, better error 
locations, etc.)
- Julien Signoles (CEA-LIST) presented the current status of E-ACSL 
plugin in Frama-C, which is being completed currently to support the 
memory model predicates (such as \valid(p) denoting that pointer p is 
valid). He also gave a demo of the integration of analysis results 
coming from different tools in Frama-C, with the generation of a graph 
of explanations.
- Yannick Moy (AdaCore) gave a demo of the current capabilities of 
gnatprove inside the GPS development environment.
- Claude Marché (INRIA) gave a demo of the counterexample generation 
feature in Alt-Ergo, based on a labeling of the input formula.

We had several discussion sessions, for which I give main points here:
- mathematical vs executable semantics
    - one semantics is preferable to two (one for mathematical, one for 
executable)
    - a proposed solution was to use larger base types for arithmetic in 
assertions
    - see details and follow-up discussion on hi-lite-discuss mailing-list
- VC generation and proof
    - use of Why3 features was critical in gnatprove to gain efficiency 
(run time divided by 100)
    - generation of traces based on Why3 labels allows path 
visualization in IDE
    - need fast weakest preconditions (linear time) in Why3 soon, as 
done in Why2 and Frama-C WP
    - need cloning of modules in Why3
    - counterexamples from Alt-Ergo are very promising to help user 
understand why goals are not provable. This is already used in Frama-C.
- test and proof integration
    - results must be aggregated, either homogeneous (ex: subprogram 
proved when all VC proved) or heterogeneous (ex: subprogram ok when both 
tested and covered or proved)
    - API is desirable, to allow various usages
    - identification of source entities by slocs (source lines of code)
    - will also be used for merging proof results on Ada side and C 
side, for mixed applications
- user interaction
    - various levels of application of proof, subprogram is the most 
important
    - run time must allow interactive usage
    - need for control panel to maintain consistent view of results

As the tools gain in maturity, feel free to download and try them:
   - latest releases of Why3 and Alt-Ergo are available 
(http://why3.lri.fr/ and http://alt-ergo.lri.fr/)
   - E-ACSL is available with Frama-C Nitrogen 
(http://frama-c.com/download.html)
   - gnattest/gnatprove will be available this month with GPL 2012 
edition of GNAT and Hi-Lite, more info later
   - SPARK 2012 GPL edition will be available this month, more info later

-- 
Yannick Moy, Senior Software Engineer, AdaCore



More information about the Hi-lite-discuss mailing list