Difference between revisions of "D45 Prover Enhancement"

From Event-B
Jump to navigationJump to search
imported>Tommy
imported>Leuschel
Line 21: Line 21:
 
{{TODO}} ''To be completed by Matthias Schmaltz''
 
{{TODO}} ''To be completed by Matthias Schmaltz''
 
== ProB Disprover ==
 
== ProB Disprover ==
{{TODO}} ''Daniel Plagge, Jens Bendiposto''  
+
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
 +
 
 +
 
 +
Mention work done for Siemens
 +
Rule-Base Validation, reading proof rule files automatically using Prolog parser, found several issues in Siemens rule base
 +
Awaiting new rule-base with explicit WD conditions
 +
 
 +
 
 +
Mention work using Kodkod here ?
 +
 
 
== SMT Solver Integration ==
 
== SMT Solver Integration ==
 
The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.
 
The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.

Revision as of 15:13, 10 February 2012

Overview

  • Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, 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.
  • TODO An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)
  • The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. TODO (Laurent Voisin, Yoann Guyot)

Motivations

New rewriting and inference rules

In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.

Advanced Preferences for Auto-tactics

The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a 'wrong' order - 'wrong' for a given PO - even though all needed tactics are present. Early version of Rodin provided preferences for automatic tactics that enabled to reorder them, but the ordering was lost at each change: one could not record a particular tactic order in order to reuse it later.

Another issue is to have more than one possibility to combine the tactics. Indeed, the only implicit combination of tactics available consisted in trying to apply them in turn for every open node of a proof. In the proving area, there exists a notion of tactic combinators, also called tacticals, that allow to combine tactics in various specific manners, thus providing a sort of tactic arithmetic.

The advanced preferences for auto-tactics solved these two issues.

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto


Mention work done for Siemens Rule-Base Validation, reading proof rule files automatically using Prolog parser, found several issues in Siemens rule base Awaiting new rule-base with explicit WD conditions


Mention work using Kodkod here ?

SMT Solver Integration

The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.

Choices / Decisions

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

Since Rodin 2.1, one can create his own tactic profiles. A tactic profile allows to set and record a particular order of chosen basic tactics. Furthermore, a profile can be applied either globally (as before), or specifically for a given project.

Since Rodin 2.3, tacticals and parameterization have been added to the profiles, thus increasing the potential of such proving feature. A tactic profile may now be composed of tacticals, that combine any number of basic tactics and other profiles. The parameterization allows for example to set a custom timeout on external provers such as AtelierB P1.

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

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. Technically, the plug-in classes extend the existing XProverCall, XProverInput, XProverReasoner, AbstractLazilyConstrTactic and ITacticParametizer classes which make it easy to integrate new tactics, reasoners and external prover calls.

Available Documentation

  • TODO Links for New rewriting and inference rules
  • TODO Links for Advanced Preferences for Auto-tactics
  • TODO Links for Isabelle Plug-in
  • TODO Links for ProB Disprover
  • TODO Links for SMT Solver Integration

Status

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

Advanced Preferences for Auto-tactics are functional in Rodin 2.3. This release provides a first set of tacticals and parameterization options.

Further releases may offer additional tacticals and options, according to user feedback.

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin & Yoann Guyot