View source for User:Nicolas/Collections/ADVANCE D3.4 Improvement of automated proof

== Overview ==

In a regular Event-B modelling activity, most of the time is spent on interactive proofs. Therefore, increasing the rate of automated proofs is a productivity booster which decreases the overall cost of formal modelling. Consequently, enhancing the automated prover has been a continuous task since the inception of the Rodin platform.

During the third period of the ADVANCE project, priority has been given to stability and improvement, and enhanced user experience.

== Motivations / Decisions ==
''' SMT Solvers'''

The SMT Solvers plug-in brings the glue that allows to use external SMT solvers for discharging proof obligations in the Rodin platform. The SMT plug-in stability has been improved by fixing several bugs. We have also added buttons to the Rodin proving interface in order to give direct access to SMT tactics. Finally, the translation to SMT solvers has been enhanced by supporting user-defined operators and passing them as uninterpreted functions.  This allows an SMT solver to be used on any proof obligation, even the ones that contain operators defined by the Theory plug-in (as far as the proof does not depend on the operator semantics, which is usually the case). AWE, an external user of Rodin, reported a 31% increase in automatic proof by using the SMT plugin.  See AWE presentation at the ADVANCE Industry Day <ref>http://www.advance-ict.eu/industry_days</ref>.

'''ProB as a Disprover / Prover'''

Usage of ProB as a disprover has been facilitated.
Counter-examples are now displayed in an easier to understand fashion.
Error messages have been cleared up.

A more in-depth empirical evaluation of using ProB as a prover has been performed <ref>http://www.stups.uni-duesseldorf.de/mediawiki/images/2/24/Pub-sets14.pdf</ref>, using a novel plug-in to compare the performance of different provers <ref>https://github.com/wysiib/ProverEvaluationPlugin</ref>.
As observed in the initial case studies, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.
For certain classes of proof obligations, i.e. those that heavily rely on enumerated or otherwise finite sets, ProB performs very favourably.

The disprover plug-in now offers the possibility to export proof obligations from inside Rodin into a custom (Prolog-based) format.
These files can then be used as test cases for the disprover.
We created several initial test cases that cover both provable as well as unprovable obligations.

Several other changes to the disprover plug-in have been made:
* As ProB itself, the disprover and prover are completely aware of theories. See the general information on ProB's theory support for details.
* Based on the empirical evaluation, several improvements have been made to ProB's kernel. While some of them also improve constraint solving in general, other are especially tailored for proof.
* A new setting has been introduced to allow ProB to react differently in animation / constraint solving and (dis-)proving. Mostly, this changes the treatment of well-definedness conditions during constraint solving.

== Available Documentation ==

Tactic profiles are described in the Rodin Handbook<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref>.

The user manual of the ''SMT Solvers'' plug-in is available on the Event-B wiki<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref>.

Information regarding the Disprover is collected on <ref>http://wiki.event-b.org/index.php/Disprover</ref>.

== Conclusion ==

During the last period of the ADVANCE project, we have been increasing the rate of automatically discharged proofs.
It has been achieved by improving existing provers, both internal and external ones.
Support for new external provers has been evaluated. Some of them have been rejected because of licence issue (''iProver''), lack of maturity (''Super Zenon''), or lack of evidence of result improvements (''CVC4''). However for ''CVC4'', more recent attempts with a different set of proof obligations tend to show otherwise, so its integration can be considered.

== References ==
<references/>

[[Category:ADVANCE D3.3 Deliverable]]