Difference between pages "D45 Model Checking" and "D45 Prover Enhancement"
From Event-B
(Difference between pages)
Jump to navigationJump to searchimported>Leuschel |
imported>Nicolas |
||
| Line 1: | Line 1: | ||
= Overview = | = Overview = | ||
| − | {{TODO}} An overview of the | + | * 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 == |
| − | + | Sometimes, the automatic prover fails because the order of the applied tactics doesn't lead to discharge the proof obligation. Previously the ordering of tactics was lost at each change. Another issue is to have more than one possibility to combine the tactics. Indeed, various combinators called ''tacticals'' allow to combine tactics in a specific manner, thus providing a sort of tactic arithmetic. The advanced preferences for auto-tactics solved these two issues. | |
| − | |||
| − | = | + | == Isabelle Plug-in == |
| − | {{TODO}} To be completed | + | {{TODO}} ''To be completed by Matthias Schmaltz'' |
| − | + | == ProB Disprover == | |
| + | {{TODO}} ''Daniel Plagge, Jens Bendiposto'' | ||
| + | == SMT Solver Integration == | ||
| + | {{TODO}} ''Laurent Voisin'' & ''Yoann Guyot'' | ||
= Choices / Decisions = | = Choices / Decisions = | ||
| − | {{TODO}} To be completed | + | == New rewriting and inference rules == |
| − | + | {{TODO}} ''To be completed by Laurent Voisin'' | |
| − | + | == Advanced Preferences for Auto-tactics == | |
| − | + | {{TODO}} ''To be completed by Nicolas Beauger'' | |
| − | + | Since Rodin 2.1, simple tactic profiles have been added. They allow to persiste and set specifically for some project various ordered ways to apply the basic tactics. Since Rodin 2.3, tacticals and parameterisation have been added to the profiles increasing even more the potential of such proving feature. The combinators allow for exemple to loop on a subset of tactics, including existing profiles, and the parameterisation allows for example to set a 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 == | ||
| + | {{TODO}} ''Laurent Voisin'' & ''Yoann Guyot'' | ||
= Available Documentation = | = Available Documentation = | ||
| − | {{TODO}} | + | * {{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 = | = Status = | ||
| − | {{TODO}} To be completed | + | == New rewriting and inference rules == |
| − | + | {{TODO}} ''To be completed by Laurent Voisin'' | |
| − | + | == Advanced Preferences for Auto-tactics == | |
| − | + | {{TODO}} ''To be completed by Nicolas Beauger'' | |
| − | + | == 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'' | ||
[[Category:D45 Deliverable]] | [[Category:D45 Deliverable]] | ||
Revision as of 10:36, 24 November 2011
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
Sometimes, the automatic prover fails because the order of the applied tactics doesn't lead to discharge the proof obligation. Previously the ordering of tactics was lost at each change. Another issue is to have more than one possibility to combine the tactics. Indeed, various combinators called tacticals allow to combine tactics in a specific manner, 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
SMT Solver Integration
TODO Laurent Voisin & Yoann Guyot
Choices / Decisions
New rewriting and inference rules
TODO To be completed by Laurent Voisin
Advanced Preferences for Auto-tactics
TODO To be completed by Nicolas Beauger Since Rodin 2.1, simple tactic profiles have been added. They allow to persiste and set specifically for some project various ordered ways to apply the basic tactics. Since Rodin 2.3, tacticals and parameterisation have been added to the profiles increasing even more the potential of such proving feature. The combinators allow for exemple to loop on a subset of tactics, including existing profiles, and the parameterisation allows for example to set a 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
TODO Laurent Voisin & Yoann Guyot
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
TODO To be completed by Nicolas Beauger
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
