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

imported>Laurent: /* Motivations / Decisions */

2014-11-21T16:46:09Z

Motivations / Decisions

← Older revision		Revision as of 16:46, 21 November 2014
Line 8:		Line 8:
	''' SMT Solvers'''		''' SMT Solvers'''

	The SMT Solvers plug-in brings the glue that allows to use external SMT solvers for discharging ~~proofs~~ 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>.		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'''		'''ProB as a Disprover / Prover'''

imported>Laurent: /* Motivations / Decisions */ Improve SMT description

2014-11-21T16:45:48Z

Motivations / Decisions: Improve SMT description

← Older revision		Revision as of 16:45, 21 November 2014
Line 6:		Line 6:

	== Motivations / Decisions ==		== Motivations / Decisions ==
	''' SMT ~~Provers~~'''		''' SMT Solvers'''

	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 ~~permits to use the~~ SMT solver 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).		The SMT Solvers plug-in brings the glue that allows to use external SMT solvers for discharging proofs 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'''		'''ProB as a Disprover / Prover'''

imported>Laurent: /* Overview */

2014-11-21T16:39:33Z

Overview

← Older revision		Revision as of 16:39, 21 November 2014
Line 1:		Line 1:
	== Overview ==		== Overview ==

	In a regular Event-B modelling activity, most of the time is spent on 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.		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.		During the third period of the ADVANCE project, priority has been given to stability and improvement, and enhanced user experience.

imported>Laurent: /* Overview */

2014-11-21T16:39:08Z

Overview

← Older revision		Revision as of 16:39, 21 November 2014
Line 1:		Line 1:
	== Overview ==		== Overview ==

	In a regular Event-B modelling activity, ~~more than 60%~~ of the time is spent on 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.		In a regular Event-B modelling activity, most of the time is spent on 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.		During the third period of the ADVANCE project, priority has been given to stability and improvement, and enhanced user experience.

imported>Laurent: /* Motivations / Decisions */

2014-11-06T15:34:10Z

Motivations / Decisions

← Older revision		Revision as of 15:34, 6 November 2014
Line 8:		Line 8:
	''' SMT Provers'''		''' SMT Provers'''

	SMT plug-in stability has been improved by fixing several bugs. We also added buttons in Rodin proving interface in order to ~~ease~~ access to SMT ~~tactic profiles~~. Finally, the translation to SMT solvers has been enhanced by supporting user-defined operators and passing them as uninterpreted functions. ~~{{TODO\|~~ Theory plug-in ~~extended support}}~~.		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 permits to use the SMT solver 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).

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

imported>Laurent: /* Motivations / Decisions */

2014-11-06T14:49:32Z

Motivations / Decisions

← Older revision		Revision as of 14:49, 6 November 2014
Line 8:		Line 8:
	''' SMT Provers'''		''' SMT Provers'''

	SMT plug-in stability has been improved by fixing several bugs. We also added buttons in Rodin proving interface in order to ease access to SMT tactic profiles.		SMT plug-in stability has been improved by fixing several bugs. We also added buttons in Rodin proving interface in order to ease access to SMT tactic profiles. Finally, the translation to SMT solvers has been enhanced by supporting user-defined operators and passing them as uninterpreted functions. {{TODO\| Theory plug-in extended support}}.

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

imported>Nicolas: /* Conclusion */

2014-11-03T16:34:59Z

Conclusion

← Older revision		Revision as of 16:34, 3 November 2014
Line 38:		Line 38:

	== Conclusion ==		== Conclusion ==
	~~{{TODO}}~~
			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 ==

imported>Nicolas: /* Available Documentation */

2014-11-03T15:46:43Z

Available Documentation

← Older revision		Revision as of 15:46, 3 November 2014
Line 30:		Line 30:

	== Available Documentation ==		== Available Documentation ==
	~~{{TODO}}~~
	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>.		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>.

imported>Nicolas at 15:46, 3 November 2014

2014-11-03T15:46:02Z

← Older revision		Revision as of 15:46, 3 November 2014
Line 3:		Line 3:
	In a regular Event-B modelling activity, more than 60% of the time is spent on 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.		In a regular Event-B modelling activity, more than 60% of the time is spent on 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 ~~thord~~ period of the ADVANCE project, priority has been given to stability improvement and enhanced user experience.		During the third period of the ADVANCE project, priority has been given to stability and improvement, and enhanced user experience.

	== Motivations / Decisions ==		== Motivations / Decisions ==
	''' SMT Provers'''		''' SMT Provers'''

	~~{{TODO}}~~		SMT plug-in stability has been improved by fixing several bugs. We also added buttons in Rodin proving interface in order to ease access to SMT tactic profiles.

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

imported>Nicolas at 15:25, 3 November 2014

2014-11-03T15:25:59Z

← Older revision		Revision as of 15:25, 3 November 2014
Line 1:		Line 1:
	== Overview ==		== Overview ==
	~~{{TODO}}~~
			In a regular Event-B modelling activity, more than 60% of the time is spent on 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 thord period of the ADVANCE project, priority has been given to stability improvement and enhanced user experience.

	== Motivations / Decisions ==		== Motivations / Decisions ==