D45 Prover Enhancement

From Event-B
Revision as of 17:25, 18 November 2011 by imported>Tommy (→‎Overview)
Jump to navigationJump to search

Overview

Two tasks concerned the prover performance from core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics.

  • TODO An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)
  • TODO An overview of the contribution about the SMT Solver Integration (Laurent Voisin)

Motivations

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

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

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

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