Difference between pages "ADVANCE D3.2 Improvement of automated proof" and "ADVANCE D3.2 Introduction"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Tommy
m
 
Line 1: Line 1:
−
= Overview =
+
The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.
−
In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.
 
−
Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g., SMT solvers).<br>
 
−
From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>
 
−
From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin as an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
 
  
−
= Motivations / Decisions =
+
The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref>.<br>
−
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in an unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in the tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.
+
Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
 +
* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,
 +
* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.
 +
These locations can be consulted from outside the Rodin tool.
  
−
Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the known capacity of such solvers in the field of arithmetics. Secondly, to extract some useful information from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.
+
The present document intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.
 +
It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).
  
−
= Available Documentation =
+
The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.
−
A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>
 
−
A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.
 
  
−
= Planning =
+
Note that each of these parts is describing the improvements made, and is structured as follows:
−
Enhancement to automated proof will continue during the ADVANCE project. This will be mainly achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.
+
* Overview. The involved partners are identified and an overview of the contribution is given.
 +
* Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.
 +
* Available documentation. Some pointers to the available documentation or related publications are listed.
 +
* Planning. The current status about the topic (as of July 2012), and an overview of the future plans are given.
  
−
Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.
+
== References ==
−
 
 
−
Finally, connecting other provers (such as Super Zenon and iProver) to the platform will be investigated.
 
−
 
 
−
= References =
 
 
<references/>
 
<references/>
  
 
[[Category:ADVANCE D3.2 Deliverable]]
 
[[Category:ADVANCE D3.2 Deliverable]]

Revision as of 12:54, 21 June 2012

The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

The Rodin platform can be downloaded from the SourceForge site[1].
Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :

  • the Event-B wiki[2],
  • the Rodin Handbook[3].

These locations can be consulted from outside the Rodin tool.

The present document intends to give a relevant overview of the work achieved within the work package 3: Methods and Tools for Model Construction and Proof, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives. It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project[4] from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).

The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.

Note that each of these parts is describing the improvements made, and is structured as follows:

  • Overview. The involved partners are identified and an overview of the contribution is given.
  • Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.
  • Available documentation. Some pointers to the available documentation or related publications are listed.
  • Planning. The current status about the topic (as of July 2012), and an overview of the future plans are given.

References

  1. ↑ http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform
  2. ↑ http://wiki.event-b.org
  3. ↑ http://handbook.event-b.org
  4. ↑ http://www.deploy-project.eu
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Improvement_of_automated_proof&oldid=200’