ADVANCE D3.3 Improvement of automated proof - Revision history

imported>Nicolas: /* Planning */

2013-10-08T10:05:15Z

Planning

← Older revision		Revision as of 10:05, 8 October 2013
Line 46:		Line 46:
	As concerns the SMT solver integration plug-in, we will benchmark it on the case study models and investigate the integration of new solvers such as CVC4.		As concerns the SMT solver integration plug-in, we will benchmark it on the case study models and investigate the integration of new solvers such as CVC4.

	Finally, as concerns external provers, we plan to ~~integrate~~ ''Super Zenon'' once it is made open source. We will also check regularly for public releases of new provers that could be integrated.		Finally, as concerns external provers, we plan to work on ''Super Zenon'' integration once it is made open source. We will also check regularly for public releases of new provers that could be integrated.

	We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic tests to ensure that we don't regress.		We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic tests to ensure that we don't regress.

imported>Nicolas: /* Planning */

2013-10-08T10:02:52Z

Planning

← Older revision		Revision as of 10:02, 8 October 2013
Line 46:		Line 46:
	As concerns the SMT solver integration plug-in, we will benchmark it on the case study models and investigate the integration of new solvers such as CVC4.		As concerns the SMT solver integration plug-in, we will benchmark it on the case study models and investigate the integration of new solvers such as CVC4.

	Finally, as concerns external provers, we ~~do not~~ plan to ~~continue this task because of the lack of available~~ open-source ~~provers~~. We will ~~nevertheless~~ check regularly for public releases of new provers that could be integrated.		Finally, as concerns external provers, we plan to integrate ''Super Zenon'' once it is made open source. We will also check regularly for public releases of new provers that could be integrated.

	We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic tests to ensure that we don't regress.		We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic tests to ensure that we don't regress.

imported>Nicolas: /* Motivations / Decisions */ Fix spelling of plug-in

2013-10-07T13:38:41Z

Motivations / Decisions: Fix spelling of plug-in

← Older revision		Revision as of 13:38, 7 October 2013
Line 25:		Line 25:

	'''ProB as a Disprover / Prover'''		'''ProB as a Disprover / Prover'''
	We reactivated a ~~plugin~~ for Rodin, that uses the ProB animator and model-checker to generate counterexamples for proof obligations. Searching for a counterexample can be done effortlessly and without user interaction. If successful, the futility of a manual proof attempt is detected early. Furthermore, the counterexample itself provides an insight into the problem and aids in debugging the model.		We reactivated a plug-in for Rodin, that uses the ProB animator and model-checker to generate counterexamples for proof obligations. Searching for a counterexample can be done effortlessly and without user interaction. If successful, the futility of a manual proof attempt is detected early. Furthermore, the counterexample itself provides an insight into the problem and aids in debugging the model.

	Additionally, we investigated the use of ProB as a prover. By observing the number and quality of occurring enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is discharged. An initial empirical evaluation was performed. For certain proof obligations containing variables with finite data types, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.		Additionally, we investigated the use of ProB as a prover. By observing the number and quality of occurring enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is discharged. An initial empirical evaluation was performed. For certain proof obligations containing variables with finite data types, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.

imported>Nicolas: /* Motivations / Decisions */

2013-09-27T12:33:02Z

Motivations / Decisions

← Older revision		Revision as of 12:33, 27 September 2013
Line 30:		Line 30:

	'''Other external provers'''		'''Other external provers'''
	We initially planned to connect the ''Super Zenon''<ref>http://cedric.cnam.fr/~delahaye/super-zenon/</ref> and the ''iProver''<ref>http://www.cs.man.ac.uk/~korovink/iprover/</ref> external provers to the Rodin platform. The development of ''iProver'' seems to have gone closed source : there is no development anymore on the Google project, although a new version 1.0 has been presented to the latest CASC-24 competition. Consequently, we could not make any progress with this prover. ''Super Zenon'' sources have not yet been made publicly available, but it is planned to be released under a GPL license by the end of 2013. We will then work on an integration into Rodin.		We initially planned to connect the ''Super Zenon''<ref>http://cedric.cnam.fr/~delahaye/super-zenon/</ref> and the ''iProver''<ref>http://www.cs.man.ac.uk/~korovink/iprover/</ref> external provers to the Rodin platform. The development of ''iProver'' seems to have gone closed source : there is no development anymore on the Google project, although a new version 1.0 has been presented to the latest CASC-24 competition. Consequently, we could not make any progress with this prover. ''Super Zenon'' sources have not yet been made publicly available, but it is planned to be released under a GPL license by the end of 2013. We will then work on its integration into Rodin.

	== Available Documentation ==		== Available Documentation ==

imported>Nicolas: /* Motivations / Decisions */

2013-09-27T12:31:45Z

Motivations / Decisions

← Older revision		Revision as of 12:31, 27 September 2013
Line 30:		Line 30:

	'''Other external provers'''		'''Other external provers'''
	We initially planned to connect the ''Super Zenon''<ref>http://cedric.cnam.fr/~delahaye/super-zenon/</ref> and the ''iProver''<ref>http://www.cs.man.ac.uk/~korovink/iprover/</ref> external provers to the Rodin platform. ~~However, ''Super Zenon'' is still not available publicly while the~~ development of ''iProver'' seems to have gone closed source : there is no development anymore on the Google project, although a new version 1.0 has been presented to the latest CASC-24 competition. Consequently, we could not make any progress in this ~~direction~~.		We initially planned to connect the ''Super Zenon''<ref>http://cedric.cnam.fr/~delahaye/super-zenon/</ref> and the ''iProver''<ref>http://www.cs.man.ac.uk/~korovink/iprover/</ref> external provers to the Rodin platform. The development of ''iProver'' seems to have gone closed source : there is no development anymore on the Google project, although a new version 1.0 has been presented to the latest CASC-24 competition. Consequently, we could not make any progress with this prover. ''Super Zenon'' sources have not yet been made publicly available, but it is planned to be released under a GPL license by the end of 2013. We will then work on an integration into Rodin.

	== Available Documentation ==		== Available Documentation ==

imported>Nicolas: /* Motivations / Decisions */ Took M. Butler remarks into account

2013-09-20T13:10:32Z

Motivations / Decisions: Took M. Butler remarks into account

← Older revision		Revision as of 13:10, 20 September 2013
Line 25:		Line 25:

	'''ProB as a Disprover / Prover'''		'''ProB as a Disprover / Prover'''
	We reactivated a plugin for Rodin, that uses the ProB animator and model-checker to generate counterexamples for proof obligations. Searching for a counterexample can be done ~~effortless~~ and without user interaction. If successful, the futility of a manual proof attempt is detected early. Furthermore, the counterexample itself provides an insight into the problem and aids in debugging the model.		We reactivated a plugin for Rodin, that uses the ProB animator and model-checker to generate counterexamples for proof obligations. Searching for a counterexample can be done effortlessly and without user interaction. If successful, the futility of a manual proof attempt is detected early. Furthermore, the counterexample itself provides an insight into the problem and aids in debugging the model.

	Additionally, we investigated the use of ProB as a prover. By observing number and quality of occurring enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is discharged. An initial empirical evaluation was performed. For certain proof obligations containing variables with finite data types, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.		Additionally, we investigated the use of ProB as a prover. By observing the number and quality of occurring enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is discharged. An initial empirical evaluation was performed. For certain proof obligations containing variables with finite data types, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.

	'''Other external provers'''		'''Other external provers'''

imported>Nicolas: /* Planning */

2013-09-17T08:57:04Z

Planning

← Older revision		Revision as of 08:57, 17 September 2013
Line 48:		Line 48:
	Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.		Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.

	We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic ~~test~~ to ensure that we don't regress.		We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic tests to ensure that we don't regress.

	== References ==		== References ==

imported>Laurent: /* Planning */

2013-09-16T17:21:09Z

Planning

← Older revision		Revision as of 17:21, 16 September 2013
Line 48:		Line 48:
	Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.		Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.

	We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic test to ensure that we don't regress.		We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic test to ensure that we don't regress.

	~~{{TODO\|Finalise plans}}~~

	== References ==		== References ==

imported>Jens: /* Planning */

2013-09-16T08:32:42Z

Planning

← Older revision		Revision as of 08:32, 16 September 2013
Line 47:		Line 47:

	Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.		Finally, as concerns external provers, we do not plan to continue this task because of the lack of available open-source provers. We will nevertheless check regularly for public releases of new provers that could be integrated.

			We will evaluate the ProB Disprover in particular with respect to correctness. We will also prepare a set of automatic test to ensure that we don't regress.

	{{TODO\|Finalise plans}}		{{TODO\|Finalise plans}}

imported>Jens: /* Motivations / Decisions */

2013-09-10T17:09:28Z

Motivations / Decisions

← Older revision		Revision as of 17:09, 10 September 2013
Line 23:		Line 23:
	'''SMT Solvers'''<br/>		'''SMT Solvers'''<br/>
	At the beginning of the ADVANCE project, an initial version of the ''SMT solvers'' plug-in was available. However, this early version was still very fragile and most of the times was producing proofs that could not be saved, rendering it useless. During the first and second period of the project, as a background task, this plug-in has been strengthened and brought to industrial grade. Version 1.0 of the plug-in has been released in June 2013.		At the beginning of the ADVANCE project, an initial version of the ''SMT solvers'' plug-in was available. However, this early version was still very fragile and most of the times was producing proofs that could not be saved, rendering it useless. During the first and second period of the project, as a background task, this plug-in has been strengthened and brought to industrial grade. Version 1.0 of the plug-in has been released in June 2013.

			'''ProB as a Disprover / Prover'''
			We reactivated a plugin for Rodin, that uses the ProB animator and model-checker to generate counterexamples for proof obligations. Searching for a counterexample can be done effortless and without user interaction. If successful, the futility of a manual proof attempt is detected early. Furthermore, the counterexample itself provides an insight into the problem and aids in debugging the model.

			Additionally, we investigated the use of ProB as a prover. By observing number and quality of occurring enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is discharged. An initial empirical evaluation was performed. For certain proof obligations containing variables with finite data types, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers.

	'''Other external provers'''		'''Other external provers'''