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

From Event-B
< User:Nicolas
Revision as of 15:19, 3 November 2014 by imported>Nicolas (→‎Motivations / Decisions)
Jump to navigationJump to search

Overview

TODO

Motivations / Decisions

SMT Provers

TODO

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 [1], using a novel plug-in to compare the performance of different provers [2]. 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

TODO Tactic profiles are described in the Rodin Handbook[3].

The user manual of the SMT Solvers plug-in is available on the Event-B wiki[4].

Information regarding the Disprover is collected on [5].

Conclusion

TODO

References

  1. ↑ http://www.stups.uni-duesseldorf.de/mediawiki/images/2/24/Pub-sets14.pdf
  2. ↑ https://github.com/wysiib/ProverEvaluationPlugin
  3. ↑ http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic
  4. ↑ http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in
  5. ↑ http://wiki.event-b.org/index.php/Disprover
Retrieved from ‘https://wiki.event-b.org/index.php?title=User:Nicolas/Collections/ADVANCE_D3.4_Improvement_of_automated_proof&oldid=10884’