Search results

From Event-B
Jump to navigationJump to search

Create the page "Proof" on this wiki! See also the search results found.

Page title matches

  • Induction proof
    The proof key is the following theorem: The proof of the previous theorem is given by instantiating the key theorem with : <m
    711 bytes (121 words) - 14:11, 30 October 2008
  • Proof Hints
    1. '''Description''': A brief description of the proof hints with the situation where this can be helpful. ...to select these hypotheses automatically when generating the corresponding proof obligation.
    4 KB (545 words) - 22:17, 5 March 2010
  • Proof Manager
    ...le for constructing proofs and maintaining existing proofs associated with proof obligations. Proof obligations are generated by the proof obligation generator and have the form of ''[http://handbook.cobra.cs.uni-d
    9 KB (1,478 words) - 10:33, 27 October 2011
  • Proof Purger
    #REDIRECT [[Proof Purger Design]]
    33 bytes (4 words) - 15:59, 6 January 2009
  • Proof Simplification
    ...development aims at getting rid of this kind of needless data contained in proof files. ...t the structure of proof trees, one can have a look at the [[Proof_Manager|Proof Manager]] page.
    3 KB (496 words) - 12:58, 12 August 2009
  • Proof Skeleton
    #REDIRECT [[Proof Skeleton Design]]
    35 bytes (4 words) - 16:56, 6 January 2009
  • Proof Trees
    ''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components: 2. '''rule''' A proof rule (possibly ''null'')
    2 KB (365 words) - 12:52, 12 August 2009
  • Accessing Proof Obligations
    *IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps. *IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.
    3 KB (443 words) - 12:53, 12 August 2009
  • Extension Proof Rules
    2 KB (307 words) - 15:38, 29 November 2019
  • New Proof Rules
    [[Category:Proof]]
    4 KB (738 words) - 12:53, 12 August 2009
  • Proof Contextual Information
    ...) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, * rule-based prover needs to know whether the rules in a proof are still valid (reusable)
    4 KB (600 words) - 14:09, 15 December 2010
  • Proof Obligation Commands
    In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: ...rer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an ele
    3 KB (457 words) - 10:43, 18 March 2010
  • Proof Purger Design
    ...sed proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging. Integration of the proof purger as a popup menu is achieved in the manifest through the ''org.eclips
    3 KB (505 words) - 12:54, 12 August 2009
  • Proof Purger Interface
    Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However,
    2 KB (400 words) - 10:20, 27 October 2011
  • Proof Skeleton Design
    This document aims at helping developers getting into the code of the proof skeleton viewer. ...eleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a conve
    2 KB (254 words) - 12:54, 12 August 2009
  • Proof Skeleton View
    ...can be used on any proof, independently of the presence of a corresponding proof obligation. Furthermore, this view allows user to see together proof rules and corresponding sequents.
    2 KB (299 words) - 12:50, 27 September 2011
  • Rodin Proof Tactics
    This page contains descriptions of the available proof tactics within the RODIN Platform. ...ails explanation of the tactic, when it is applicable, give the associated proof rule. See [[Inference Rules|Inference rules]] list and [[All Rewrite Rules
    57 KB (6,150 words) - 17:25, 21 February 2012
  • Extending the Proof Manager
    ...le for constructing proofs and maintaining existing proofs associated with proof obligations. There are two ways for extending the Proof Manager:
    3 KB (400 words) - 10:27, 27 October 2011
  • Proof Dependencies and Reasoner Conflicts
    ..., proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for ...e proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.
    1 KB (175 words) - 14:49, 6 June 2011
  • ADVANCE D3.2 Improvement of automated proof
    ...h could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactic ...time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
    4 KB (596 words) - 13:21, 18 July 2012
  • ADVANCE D3.3 Improvement of automated proof
    ...e the diversity of predicates and increase the automated proofs of trivial proof obligations often encountered in degenerated cases (that is not interesting The proportion of automatically discharged proof obligations heavily depends on the auto-tactic configuration. Sometimes, th
    7 KB (1,145 words) - 10:05, 8 October 2013
  • Current Proof Tree Node in UI
    ...e Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 these view do not always display t ...w does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
    4 KB (683 words) - 18:33, 16 December 2011
  • Proof Obligation Names (Rodin User Manual)
    Next is a table describing the names of context proof obligations: Next is a table showing the name of machine proof obligations:
    4 KB (575 words) - 15:09, 15 September 2011
  • Extending the Proof Obligation Generator(How to extend Rodin Tutorial)
    ...[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|Generating the proof obligations]]}} ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand
    13 KB (1,774 words) - 13:57, 5 September 2013
  • Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
    ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand ...oof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
    13 KB (1,755 words) - 07:19, 7 September 2010

Page text matches

  • Proof Skeleton View
    ...can be used on any proof, independently of the presence of a corresponding proof obligation. Furthermore, this view allows user to see together proof rules and corresponding sequents.
    2 KB (299 words) - 12:50, 27 September 2011
  • Proof Trees
    ''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components: 2. '''rule''' A proof rule (possibly ''null'')
    2 KB (365 words) - 12:52, 12 August 2009
  • Proof Dependencies and Reasoner Conflicts
    ..., proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for ...e proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.
    1 KB (175 words) - 14:49, 6 June 2011
  • Proof Skeleton Design
    This document aims at helping developers getting into the code of the proof skeleton viewer. ...eleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a conve
    2 KB (254 words) - 12:54, 12 August 2009
  • All Rewrite Rules
    ==[[Extension Proof Rules]]== {{:Extension Proof Rules}}
    739 bytes (98 words) - 13:29, 26 April 2013
  • Prover Diagrams
    ...ation to begin to understand the structural relationships within the RODIN proof tool. The diagrams were produced as an aid to visualising these relationshi Image:ProofStatus.png|Proof Status Diagram
    726 bytes (102 words) - 12:02, 12 August 2009
  • Proof Purger Interface
    Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However,
    2 KB (400 words) - 10:20, 27 October 2011
  • How Rodin Deviates from Abrial's Book
    On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</m === Proof Calculus ===
    1 KB (188 words) - 11:10, 25 January 2012
  • Extension Rewrite Rules
    #REDIRECT [[Extension Proof Rules]]
    35 bytes (4 words) - 10:23, 9 September 2010
  • Proof Purger
    #REDIRECT [[Proof Purger Design]]
    33 bytes (4 words) - 15:59, 6 January 2009
  • Proof Skeleton
    #REDIRECT [[Proof Skeleton Design]]
    35 bytes (4 words) - 16:56, 6 January 2009
  • Purging Unused Proofs
    #REDIRECT [[Proof Purger Interface]]
    36 bytes (4 words) - 16:04, 6 January 2009
  • Teamwork Requirements
    == Merging of proof files == ...eat if two people work independtly on different proofs that the discharged proof obligations could be merged. A first version of
    1,010 bytes (157 words) - 10:00, 22 October 2009
  • Current Proof Tree Node in UI
    ...e Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 these view do not always display t ...w does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
    4 KB (683 words) - 18:33, 16 December 2011
  • Proof Simplification
    ...development aims at getting rid of this kind of needless data contained in proof files. ...t the structure of proof trees, one can have a look at the [[Proof_Manager|Proof Manager]] page.
    3 KB (496 words) - 12:58, 12 August 2009
  • Accessing Proof Obligations
    *IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps. *IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.
    3 KB (443 words) - 12:53, 12 August 2009
  • Induction proof
    The proof key is the following theorem: The proof of the previous theorem is given by instantiating the key theorem with : <m
    711 bytes (121 words) - 14:11, 30 October 2008
  • Proof Obligation Names (Rodin User Manual)
    Next is a table describing the names of context proof obligations: Next is a table showing the name of machine proof obligations:
    4 KB (575 words) - 15:09, 15 September 2011
  • Proof Hints
    1. '''Description''': A brief description of the proof hints with the situation where this can be helpful. ...to select these hypotheses automatically when generating the corresponding proof obligation.
    4 KB (545 words) - 22:17, 5 March 2010
  • Proof Contextual Information
    ...) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, * rule-based prover needs to know whether the rules in a proof are still valid (reusable)
    4 KB (600 words) - 14:09, 15 December 2010
  • Extending the Proof Manager
    ...le for constructing proofs and maintaining existing proofs associated with proof obligations. There are two ways for extending the Proof Manager:
    3 KB (400 words) - 10:27, 27 October 2011
  • Scenarios for Merging Proofs
    == Proof structure == With respect to the merging objective, a proof is made of:
    6 KB (1,046 words) - 10:34, 27 October 2011
  • Generic Instantiation
    ...xtending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development r ...n the instantiation. In that sense our approach avoids re-proof of pattern proof obligations in the instantiation. The reusability of a development is expre
    2 KB (232 words) - 15:23, 4 July 2013
  • Proof Purger Design
    ...sed proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging. Integration of the proof purger as a popup menu is achieved in the manifest through the ''org.eclips
    3 KB (505 words) - 12:54, 12 August 2009
  • Proof Manager
    ...le for constructing proofs and maintaining existing proofs associated with proof obligations. Proof obligations are generated by the proof obligation generator and have the form of ''[http://handbook.cobra.cs.uni-d
    9 KB (1,478 words) - 10:33, 27 October 2011
  • Proof Obligation Commands
    In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: ...rer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an ele
    3 KB (457 words) - 10:43, 18 March 2010
  • Refactoring Framework Release History
    ...). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem ** Renaming of proofs would not save the proof files after renaming
    2 KB (357 words) - 12:18, 8 June 2010
  • SMT Plug-in Performance
    Performance is measured by running the SMT solvers on a set of proof obligations coming from some Event-B projects. Each solver is run in the ex :contains proof obligations to test, organized in Event-B projects
    4 KB (652 words) - 08:48, 6 June 2014
  • D23 Improvements to Existing Provers
    ...html One point rule], arithmetic rules), have been added to discharge more proof obligations more easily. * Reducing proof storage space.
    5 KB (789 words) - 11:41, 27 January 2010
  • Modeling Feedback
    Real goal is to obtain a proof, not a model. The model is only our mean of choice to obtain a proof.
    1 KB (153 words) - 13:44, 28 October 2008
  • Disprover
    or proofs for a given proof obligation. ...ult. In this cases, the absence of a counter-example will be reported as a proof.
    1 KB (155 words) - 13:34, 2 May 2016
  • Revisiting Feasibility POs
    in the Proof Obligation Generator (POG) of Rodin 2.3 where one could have an event-B project containing two machines where all proof obligations are
    8 KB (1,284 words) - 18:33, 30 January 2012
  • How to read Rodin projects and elements programmatically
    ==How to read Proof Obligations== For information on reading proof obligations, have a look at [[Accessing Proof Obligations]].
    3 KB (314 words) - 14:12, 30 May 2009
  • Dagstuhl Seminar 2009
    * Proof automation * Proof reuse
    1 KB (150 words) - 13:31, 3 November 2009
  • ADVANCE D3.2 Language extension
    ...with these additional notations, the user can also define new proof rules (proof extensions). ..., validating and using extensions while exploiting the benefits brought by proof obligations.
    4 KB (642 words) - 08:33, 29 June 2012
  • Versioned Reasoners
    ...This entails potential problems: what happens if we try to reuse/replay a proof rule serialized by the old reasoner implementation ? There might be unexpec ...en trying to reuse them. Rather than adding yet another xml attribute into proof files, it has been decided to concatenate the version to the reasoner name,
    2 KB (308 words) - 17:01, 20 November 2009
  • Flows
    ...as writing and maintaining deadlock-freedom and relative deadlock freedom proof obligations. Its core functionality is concerned with the verification of t ...rs and thus there will be always some delays between saving a diagram and proof status update.
    4 KB (630 words) - 22:31, 22 January 2011
  • Language of an Event-B Component
    As concerns generated files (e.g., statically checked files and proof obligation files), they contain formulas in the same language as the compon Proof status files do not contain any formula and are therefore independent on th
    4 KB (692 words) - 15:06, 20 November 2013
  • SMT 1.4 Performance Results
    This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually. ...provers have individually improved their rate of automatically discharged proof obligations.
    2 KB (281 words) - 15:57, 11 September 2017
  • ADVANCE D3.3 Language extension
    ...with these additional notations, the user can also define new proof rules (proof extensions). ..., validating and using extensions while exploiting the benefits brought by proof obligations.
    4 KB (648 words) - 14:52, 7 October 2013
  • Flows Plug-in
    ...the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of t ...isprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.
    4 KB (699 words) - 17:36, 3 December 2010
  • D23 Flow Plug-in
    ...of the Flows plug-in. The primary reason to offer such a weak guarantee is proof effort required for stronger types of connectives. ...and the proof obligations related to flow appear in the list of the model proof obligations.
    4 KB (609 words) - 11:37, 8 January 2010
  • ADVANCE D3.2 Improvement of automated proof
    ...h could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactic ...time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
    4 KB (596 words) - 13:21, 18 July 2012
  • Developer Documentation
    * [[Accessing Proof Obligations]] * [[Extending the Proof Manager]]
    2 KB (179 words) - 09:17, 20 November 2013
  • Single View Design
    ...''Obligation Explorer'' displays the proof obligations together with their proof state. ...original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of th
    5 KB (842 words) - 18:35, 26 March 2010
  • Event-B
    ...resent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
    306 bytes (47 words) - 09:57, 4 March 2009
  • Development of a flash-based filestore
    ...s an open and extensible toolset for Event-B specification, refinement and proof. The flash file system is a complex system that is challenging to specify a === Modelling and proof of a Tree-structured File System===
    4 KB (656 words) - 13:06, 18 November 2010
  • Rodin
    ...[Event-B]] that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is f
    491 bytes (67 words) - 14:18, 19 September 2011
  • Past Developments
    ...owing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position. ====Fixing Proof Obligations====
    6 KB (915 words) - 16:57, 27 February 2014
  • Rodin Platform
    [[Rodin Proof Tactics]]
    310 bytes (38 words) - 10:51, 27 October 2011
  • Plug-in Tutorial
    ...ow_to_extend_Rodin_Tutorial)|8 Generating proof obligations (Extending the Proof Obligation Generator)}}
    4 KB (487 words) - 14:27, 5 September 2013
  • Rodin Plug-ins
    === Theory and Proof === * [[Isabelle for Rodin]]: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
    5 KB (757 words) - 16:19, 13 February 2020
  • Event-B Qualitative Probability User Guide
    ** New proof obligations: '''PRV''', '''BND''', '''FINACT'''. === Proof Obligations ===
    6 KB (749 words) - 17:54, 21 March 2018
  • Isabelle for Rodin
    This plug-in provides an automated proof tactic based on the theorem prover [http://isabelle.in.tum.de/index.html Is It also allows users to export proof obligations to Isabelle theories for later inspection with Isabelle.
    9 KB (1,317 words) - 10:07, 29 April 2013
  • Rodin Platform 1.3.1 Release Notes
    Bug 2999977: Can not save proof after functional image simplification
    651 bytes (84 words) - 18:41, 22 February 2011
  • Context Diagram
    ...(given properties about the constants) and Theorems (assertions requiring proof) may be attached to the ClassTypes. ClassTypes either define ‘carrier’
    606 bytes (84 words) - 20:27, 10 September 2008
  • Group refinement
    ...ive laws result in a more natural and compact model with fewer and simpler proof obligations. ...sequential composition through refinement steps may result in unmanageable proof obligations. It is also more difficult to conduct subsequent refinement of
    5 KB (777 words) - 23:20, 6 December 2010
  • ADVANCE D3.3 Introduction
    ...within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the second period of the ADVANCE project (Sept 2012 - Sept 2013), ...work package tasks: general platform maintenance, improvement of automated proof, model checking, language extension, model composition and decomposition.
    2 KB (325 words) - 17:32, 29 November 2013
  • D23 Rule-based Prover
    ...ule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs. *Theory construct, where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied
    5 KB (796 words) - 11:44, 8 January 2010
  • ADVANCE D3.3 Revised Roadmap
    ...et shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of th ...out in WP4. However, they may require some evolution of the modelling and proof tools to be performed within WP3.
    4 KB (677 words) - 16:41, 2 December 2013
  • Predicate Variables Extension
    The aim of this extension is to allow defining proof rules for the Rule Based Prover using meta-variables as predicate placehold For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.
    3 KB (431 words) - 15:14, 18 February 2010
  • Rodin Platform Welcome Page
    ...formal method and provides natural support for refinement and mathematical proof. To improve your proof experience, please install the third-party provers from Atelier B. This is
    2 KB (322 words) - 16:45, 20 April 2010
  • Rodin Developer Support
    * [[Proof Purger Design|Proof Purger]] allows to delete unused proofs. * [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
    8 KB (1,260 words) - 12:45, 30 July 2015
  • Theory Plug-in
    ...ent to define rewrite rules to a versatile platform to define and validate proof and language extensions. ...n be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
    7 KB (958 words) - 14:53, 14 June 2021
  • D32 Mathematical Extensions
    ...types. Along with these additional notations, the user can also define new proof rules (prover extensions). ...es and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. W
    7 KB (1,095 words) - 14:40, 21 December 2010
  • ADVANCE D3.2 Introduction
    ...within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011) ...ed into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decompositio
    2 KB (371 words) - 16:27, 13 July 2012
  • Maplet Overriding in Goal
    ...imes the expression ''x''. If this expression is big, then it can make the proof rule hard to read. ...te of the conjunction is provable. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writ
    5 KB (824 words) - 16:05, 18 March 2014
  • D32 General Platform Maintenance
    * Proof replay on undischarged POs (since release 1.3) ...e slightly changed and need to be discharged again. However, replaying the proof for these POs could most of the time be enough to discharge it. Hence, a co
    9 KB (1,423 words) - 16:28, 14 November 2011
  • Generic Instantiation Plug-in User Guide
    ...from the instantiated machines where it is avoided the re-proof of pattern proof obligations. Afterwards <math>GI_n</math> can be further refined to <math>P
    5 KB (720 words) - 15:20, 4 July 2013
  • Datatype Rules
    The resulting proof step is The resulting proof step is
    8 KB (1,199 words) - 13:37, 7 September 2010
  • Rodin File Types
    |<tt>.bpo</tt> || {{class|IPORoot}} || Event-B Proof Obligations || Event-B Core |<tt>.bps</tt> || {{class|IPSRoot}} || Event-B Proof Statuses || Event-B Core
    3 KB (449 words) - 14:55, 12 March 2019
  • Rodin Workshop 2012
    ...et for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A ran * How to create and use custom/parameterized proof tactics (Systerel/Jean-Raymond Abrial), 30 mins
    4 KB (530 words) - 15:34, 23 March 2012
  • Scenarios for Team-based Development
    ...instance that if we change an invariant, that not the whole prooftree of a proof is invalidated, but only a subtree. ...sions.) There are, however, still issues with how to manage the individual proof files in case of changes to the model (renaming of some files, deletion of
    4 KB (670 words) - 14:38, 29 January 2009
  • D32 Teamwork
    ...ected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also refe ...be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable deco
    5 KB (780 words) - 11:22, 21 December 2010
  • How To Evolve Reasoners
    ...volve in time, to fix bugs or modify the behaviour, or to match additional proof rules, even after the old implementation was used to prove models. This lea ...ion will be left unnoticed. Thus, if we clean a project in order to update proof statuses, these proofs will be considered reusable (in the sense of org.eve
    4 KB (642 words) - 10:29, 27 October 2011
  • ADVANCE Deliverable D3.3
    ...the ADVANCE Deliverable D3.3 (Methods and tools for model construction and proof II) which will be delivered to the European Commission at month 24 (2013-09 #to provide expert formal proof support to the industrial partners;
    6 KB (830 words) - 13:21, 7 October 2013
  • Group refinement plugin
    ...tract variables and events retained solely for the needs of the refinement proof and those preserved as an integral part of an overall specification in the ...by auxiliary variables) but rather taken into the account when generating proof obligations.
    7 KB (1,109 words) - 15:33, 31 August 2010
  • Rodin Platform 2.2.2 Release Notes
    ...nc=detail&aid=3370087&group_id=108850&atid=651669 Bug 3370087: Cannot save proof with ae] :fixed proof loading (and replay) problems
    4 KB (515 words) - 08:41, 1 August 2011
  • D23 Pattern Plug-in
    ...ncludes the achievements of the pattern and is correct without proving any proof obligation. ...he current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects i
    6 KB (1,034 words) - 14:43, 27 January 2010
  • Rodin Platform 3.3 Release Notes
    ...'' reasoner no longer considers hidden hypotheses. This avoids leading the proof to a dead-end. === Better proof reuse ===
    7 KB (1,079 words) - 13:54, 12 July 2017
  • Rewriting rules for event model decomposition
    ...Event-B assignments. Two actions are considered as being equivalent if the proof obligations generated for these actions are logically equivalent. ...o be proved (see the section related to the [[Event_Model_Decomposition#po|proof obligations]] in the event model decomposition).
    10 KB (1,604 words) - 09:19, 27 October 2011
  • D32 Introduction
    ...sh the soundness of provers and improve the generation of well-definedness proof obligations,
    3 KB (415 words) - 17:03, 24 November 2010
  • Modularisation Plug-in Release Notes
    * There is a bug in showing interface proof obligations - these are not refreshed automtically in the project explorer. * No proof obligations are generated to ensure deadlock freeness of event groups reali
    4 KB (601 words) - 23:58, 13 October 2009
  • Old Flow Plug in page
    ...tronger types of connectives. Let us see what it means to provide a formal proof for the various cases of sequential event composition. ...g "immediately after" <math>m</math> times there would be <math>m*n</math> proof obligations. Even if only a small fraction of these result in interactive p
    11 KB (1,869 words) - 23:48, 21 January 2011
  • Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
    ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand ...oof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
    13 KB (1,755 words) - 07:19, 7 September 2010
  • Rodin Workshop 2023
    effective support for modelling and automated proof. The platform is open * Proof automation for Event-B theories — ''P. Rivière, N. K. Singh, Y. Aït-Ame
    3 KB (375 words) - 15:36, 26 May 2023
  • Rodin Platform 3.1 Release Notes
    ...valid reasoner (old version or not installed) is properly displayed in the Proof Skeleton View. ...been used; running 'Proof Replay on Undischarged POs' will replay the old proof with the current version of the reasoner.
    6 KB (909 words) - 13:48, 17 December 2014
  • Event-B Mathematical Language
    *A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as [ftp://ftp.inf.ethz.ch/pub/publica
    1 KB (203 words) - 11:28, 23 January 2014
  • Adding Reasoners(How to extend Rodin Tutorial)
    ..._Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index) ...I that paint their applications in red on formulas) in case of interactive proof.<br>
    13 KB (2,012 words) - 15:43, 21 September 2021
  • ADVANCE D3.3 Improvement of automated proof
    ...e the diversity of predicates and increase the automated proofs of trivial proof obligations often encountered in degenerated cases (that is not interesting The proportion of automatically discharged proof obligations heavily depends on the auto-tactic configuration. Sometimes, th
    7 KB (1,145 words) - 10:05, 8 October 2013
  • Sequent Prover Developer Guide
    ...uent prover is a plug-in for the Eclipse platform which provides different proof rules to be used within the Rodin Tool. The following sections discuss the == Proof Rules ==
    17 KB (2,378 words) - 09:48, 17 June 2010
  • Rodin Platform 3.8 Release Notes
    805 IAE when loading proof 807 Proof information view text cut off
    5 KB (775 words) - 12:00, 4 April 2023
  • D32 Provers
    ...domains and observed that his tactic significantly increases the number of proof obligations proved automatically. ...nstruction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions
    11 KB (1,699 words) - 15:25, 27 January 2011
  • D23 Decomposition
    ...to deal with a growing number of events, state variables, and consequently proof obligations. ...management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
    6 KB (825 words) - 13:27, 27 January 2010
  • Theory Release History
    ** A proof obligation is generated for the well-definedness condition of recursive ope ** Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
    8 KB (1,015 words) - 13:50, 1 April 2022
  • Refactoring Framework
    ...renaming an element doesn't modify their existing proof state (no loss of proof). Since there are proof obligations associated with Event-B files, while renaming the goal would be
    11 KB (1,773 words) - 07:41, 12 January 2016
  • Rodin Proving Perspective
    When proof obligations (POs) are not discharged automatically the user can attempt to ...es, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views
    27 KB (4,348 words) - 08:56, 26 September 2011
  • The Proving Perspective (Rodin User Manual)
    When proof obligations (POs) are not discharged automatically the user can attempt to ...es, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views
    27 KB (4,348 words) - 18:45, 28 September 2011
  • Extending the Proof Obligation Generator(How to extend Rodin Tutorial)
    ...[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|Generating the proof obligations]]}} ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand
    13 KB (1,774 words) - 13:57, 5 September 2013
  • Event-B Examples
    ...ns the abstract Event-B development, however the implementation refinement proof is ongoing. The slides outline the use of Rodin in the proof of Well-ordering theorem. The archive contains the
    9 KB (1,283 words) - 13:58, 5 July 2017
  • Relevance Filter Plug-in
    select relevant hypotheses for a proof as opposed to the user doing this the proof control, or automatically as part of the auto tactic.
    4 KB (569 words) - 07:04, 1 August 2011
  • D32 Modes and Fault Tolerance
    ...ted Event-B model is enforced to implement the mode diagram by a number of proof obligations. ...ts the main development with an orthogonal set of documents and additional proof obligations.
    5 KB (816 words) - 17:37, 3 December 2010
  • File Root Separation
    * <tt>IPOFile</tt>: proof obligation file * <tt>IPRFile</tt>: proof file
    6 KB (897 words) - 11:47, 29 January 2009
  • Generic Instantiation Proposal
    Consequently, if we drop the maximality axiom, we have to generate additional proof obligations for showing that every instantiation of a constant belongs to t ...above. However, all these adjustments would be made under the control of proof, rather than performed by a tool. Moreover, the user would have the opportu
    4 KB (704 words) - 10:17, 5 December 2012
  • Google Summer of Code 2009
    ...resent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. You can know more of Event ...or Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is f
    10 KB (1,629 words) - 12:50, 12 August 2009
  • B2C plugin
    ...The manipulations are done within Event-B where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliabili
    1 KB (232 words) - 20:27, 8 February 2010
  • Generic Instantiation User Guide
    # Proof of Obligation integration to Generic Instantiation file:<br>Axiom replaceme
    2 KB (206 words) - 01:40, 18 August 2014
  • Rodin Platform 1.2 Release Notes
    ...See also [[Proof_Skeleton_View#Copy.2FPaste_to_Proof_Tree | Copy/Paste to Proof Tree]]. FR 2844800: Copy from Proof Skeleton to Proof Tree
    11 KB (1,488 words) - 10:06, 28 July 2010
  • Tool Development Roadmap
    |rowspan="9"|'''Automated Proof and Model-checking'''<br/>[Systerel / Düsseldorf / Southampton] |Develop enabledness-preservation proof obligations
    4 KB (584 words) - 09:50, 12 September 2013
  • D23 ProB
    * Using proof information to improve model checking. ...rder to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 pro
    17 KB (2,580 words) - 15:55, 28 January 2010
  • Rodin Platform 1.3 Release Notes
    ...go through all undischarged POs, just to see them in turn be proved. The "Proof Replay on Undischarged POs" command does it in a single step. It is accessi :See also: [[Proof Obligation Commands]]
    12 KB (1,642 words) - 13:21, 28 July 2010
  • Inference Rules
    ...o write the set corresponding to <math>T</math> in the editing area of the Proof Control Window || M ...the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M
    36 KB (5,611 words) - 10:22, 1 February 2024
  • Rodin Platform 2.1 Release Notes
    ...0 automatic rewriting rules have been added, making it easier to discharge proof obligations. [[Image:Rodin_Performances_Editor_perf_simplev2.png|850px|Rodin Proof Editor Performances]]
    10 KB (1,277 words) - 13:45, 26 July 2011
  • Rodin Platform 2.2 Release Notes
    ...a reference to a IPRReasoner, a newly introduced proof element type. See [[Proof Dependencies and Reasoner Conflicts]]. Bug 3243479: Font is not updated in proof skeleton view
    10 KB (1,354 words) - 13:31, 1 July 2011
  • User Documentation Overhaul
    * Consider adding the proof tactics: [[Rodin Proof Tactics]]
    5 KB (720 words) - 11:28, 15 September 2011
  • Tracking Memory Leaks
    plug-in. While looking for a proof, it was allocating megabytes of memory, and upon cancellation the memory wa
    2 KB (337 words) - 11:03, 10 November 2008
  • Rodin Workshop 2020
    ...upport for modelling and tool-assisted reasoning, in particular, automated proof. The platform is open source and can be extended with plug-ins. A range of
    2 KB (303 words) - 14:32, 19 May 2020
  • Rodin Platform 2.0 Release Notes
    ::- Navigating through proof tree nodes is faster (useless refreshings of search hypotheses where remove ...rily complicated lemmas.Some old proofs could appear as undischarged, the "Proof Replay on Undischarged POs" commmand will discharge these proofs.
    15 KB (2,008 words) - 15:34, 10 January 2011
  • Membership in Goal
    ...and with fewer needed hypotheses which makes proof rules more legible and proof replay less sensitive to modifications of the models. ...create, internally to the reasoner, a small proof tree built from internal proof rules (implemented in class Rules). Each rule contains one predicate and an
    19 KB (3,362 words) - 13:50, 5 June 2014
  • D45 Prover Enhancement
    ...h could be customized and parameterized tactics to discharge some specific proof obligations.<br> ...n proof obligations. ProB has also been used for finding count examples to proof rules of the industrial partner Siemens.<br>
    21 KB (3,334 words) - 21:20, 20 April 2012
  • D32 Scalability
    ...the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of t ...ive laws result in a more natural and compact model with fewer and simpler proof obligations. The method and the tool were development by Newcastle Universi
    19 KB (2,944 words) - 15:28, 27 January 2011
  • Rodin Workshop 2018 CFP
    automated proof. The platform is open source and can be extended with
    2 KB (294 words) - 09:58, 16 October 2017
  • Rodin Platform 3.0 Release Notes
    The tactic profiles are now quickly available while proving: from Proof Control, click the green triangle dropdown list and choose the profile, it ...simulated before). This avoids strange behaviors that could happen when a proof obligation changes several times.
    8 KB (1,195 words) - 16:35, 9 July 2014
  • Rodin Platform 1.1 Release Notes
    # [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule] * Proof obligations
    9 KB (1,298 words) - 10:06, 28 July 2010
  • SMT Solvers Plug-in
    We give an example of Event-B model of which proof obligation can be discharged using an SMT solver: ...into the Rodin Platform, the SMT tactic button is now accessible in the ''Proof Control'' bar.
    17 KB (2,538 words) - 15:41, 2 October 2017
  • Rodin Platform 2.3 Release Notes
    Bug 3370087: Cannot save proof with ae Bug 3415433: NPE on proof saving
    11 KB (1,401 words) - 09:39, 8 November 2011
  • D32 Model Animation
    ...es) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger and more rec ...always easy to see for an user if this is caused by the complexity of the proof or by an error.
    16 KB (2,553 words) - 15:12, 27 January 2011
  • Rodin Platform 3.7 Release Notes
    797 ClassCastException when saving proof 361 Add show info and next subgoals buttons to proof tree view
    5 KB (703 words) - 14:37, 29 April 2022
  • Rodin Workshop 2018
    automated proof. The platform is open source and can be extended with
    2 KB (356 words) - 12:46, 24 May 2018
  • Rodin Workshop 2024
    effective support for modelling and automated proof. The platform is open
    3 KB (368 words) - 12:49, 15 April 2024
  • Rodin Platform 2.4 Release Notes
    ...w''': this new view shows the type environment for the current node of the proof (free identifiers and their type). It is accessible through "Window > Show :'''Proof Simplification''': once proofs are complete, they can be automatically simp
    11 KB (1,542 words) - 08:35, 1 March 2012
  • Pattern
    ...n of a refinement of the problem at hand is correct by construction and no proof obligation needs to be generated. ...ction of reusing a pattern within a development to be correct (without any proof), the pattern and the development have to be matched. This means the elemen
    17 KB (2,670 words) - 15:07, 24 January 2012
  • Railway Interlocking Feedback
    exhibited seem to come from nowhere (in fact, proof obligations of the the proof of the model, as event guards become more and more complex
    6 KB (967 words) - 12:57, 28 October 2008
  • Rule-based Prover Plug-in
    ...ified, only the validated ones are available. By validated, we mean "whose proof obligations are either dischared or reviewed".
    2 KB (338 words) - 17:11, 9 July 2010
  • Parallel Composition using Event-B
    ...m (using Event-B notation) and study the concerns, properties, conditions, proof obligations, advantages and disadvantages when create/analysing system spec ...ed machine invariant should be visible to the composed machine or not (for proof optimization).
    7 KB (1,161 words) - 11:02, 4 July 2013
  • Rodin Platform 2.5 Release Notes
    ...PI simplification''': some operations of the user support work only on the proof tree in main memory. Therefore, they cannot raise any RodinDBException, as Bug 3054228: Proof simplification too slow
    11 KB (1,478 words) - 17:32, 2 May 2012
  • Rodin Platform 2.2.1 Release Notes
    ...nc=detail&aid=3370087&group_id=108850&atid=651669 Bug 3370087: Cannot save proof with ae]
    3 KB (398 words) - 15:31, 22 July 2011
  • IUML-B Modelling a control system
    12. While developing refinements (in order to discharge proof obligations) we add invariants to states about a) states of other component
    3 KB (420 words) - 22:08, 30 September 2020
  • UML-B - Modelling a control system
    12. While developing refinements (in order to discharge proof obligations) we add invariants to states about a) states of other component
    3 KB (420 words) - 22:10, 30 September 2020
  • Event-B Language
    [[Proof Hints]]
    3 KB (351 words) - 11:30, 23 January 2014
  • Rodin Platform 2.7 Release Notes
    Bug 3565590: Can't open a proof Bug 2957980: Proof Skeleton View : \n displayed as squares
    10 KB (1,301 words) - 07:11, 29 August 2013
  • D23 Introduction
    ...enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
    3 KB (399 words) - 11:20, 27 January 2010
  • Team-based development
    * commit the shared project (note that no model/proof files should appear for commit at this stage)
    3 KB (445 words) - 07:03, 1 August 2011
  • Exporting and importing archives containing theories
    ...this case we chose to only put the .tuf (theory unchecked file) and .bpr (proof file) into the archive, because other files (.tcf, .bpo, .bps) are generate
    3 KB (539 words) - 14:57, 14 June 2021
  • D45 Introduction
    ...Solvers'' which both help to raise the number of automatically discharged proof obligations.
    3 KB (500 words) - 09:18, 23 April 2012
  • Rodin Platform 3.2 Release Notes
    743 Error while running tool (Automatic Proof Obligation Manager) 739 Opening a proved proof - prune the proof
    9 KB (1,317 words) - 11:09, 6 July 2017
  • Rodin Platform 2.6 Release Notes
    Bug 2957980: Proof Skeleton View : \n displayed as squares Bug 3112539: Proof status after theory change
    10 KB (1,328 words) - 16:14, 3 August 2012
  • Modus Ponens generalized
    ...checked. But it is still worthy because it may simplify a lot, and so make proof obligations simpler and more legible to users. #Finally, the proof rule is made. There are 5 cases :
    10 KB (1,784 words) - 16:04, 18 March 2014
  • Modularisation Integration Issues
    ...component configurations (a configuration is a set of static checking and proof generation rules). Currently one can add new bag of rules alongside an exis
    3 KB (518 words) - 11:34, 6 September 2010
  • Improved WD Lemma Generation
    [[Category:Developer documentation]][[Category:Proof]]
    4 KB (617 words) - 09:43, 19 June 2012
  • D23 Code Generation
    ...project. Instead an aim is to develop a sufficient framework to act as a proof-of-concept to enable code generation for the Bosch and SSF pilots. A furth ...real-time embedded systems from code-oriented models. A refinement-based proof method for code-oriented models will be defined and incorporated into the R
    11 KB (1,725 words) - 18:07, 7 December 2009
  • Rodin Proof Tactics
    This page contains descriptions of the available proof tactics within the RODIN Platform. ...ails explanation of the tactic, when it is applicable, give the associated proof rule. See [[Inference Rules|Inference rules]] list and [[All Rewrite Rules
    57 KB (6,150 words) - 17:25, 21 February 2012
  • Mathematical Extensions
    * Proof Obligation Generator === Proof Obligation Generator requirements ===
    19 KB (2,883 words) - 18:20, 17 March 2014
  • Rodin Platform Releases
    * The compatibility is preserved upwardly throught model and proof upward compatibility. However, this compatibility is ensured on models and
    4 KB (532 words) - 06:51, 4 April 2023
  • Modularisation Plug-in
    * Decomposing proof effort: splitting helps to split verification effort. It also helps to reus ...ts and actions contained in them is linearly proportional to the number of proof obligations.
    18 KB (2,784 words) - 10:57, 6 September 2010
  • State-Machines and Code Generation
    ...ransitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example fra
    4 KB (659 words) - 09:47, 17 May 2012
  • Event Model Decomposition
    === <font id="po">Generation of the proof obligations</font> === ...[http://handbook.event-b.org/current/html/generated_proof_obligations.html proof obligations] (PO) have been handled successfully.
    43 KB (6,950 words) - 09:48, 27 October 2011
  • Extended Operator Translation
    ...uite annoying, especially when the extension does not play any role in the proof, but is just in the way of the prover.
    4 KB (660 words) - 16:36, 18 March 2014
  • Shared Event Composition Release History
    **Added proof obligations: WD and INV for (composition) invariants and INV, SIM and GRD f
    4 KB (550 words) - 10:39, 25 November 2014
  • Mode/FT Views
    ...the model. The tool statically checks the views and generates a number of proof obligations. ...he start and terminal modes which do not have names. The names are used in proof obligations.
    21 KB (3,472 words) - 20:32, 26 June 2015
  • Rodin Workshop 2009
    ...tp://wiki.event-b.org/images/Reasoned_modelling.pdf A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in]
    5 KB (766 words) - 09:59, 21 September 2011
  • Rodin Workshop 2021
    effective support for modelling and automated proof. The platform is open
    4 KB (595 words) - 09:41, 29 June 2021
  • Event-B to SMT-LIB
    ...l ones added. Unfortunately, veriT has one restriction: it does not handle proof obligations which contain sets of sets.
    5 KB (797 words) - 10:29, 24 October 2011
  • Rodin Workshop 2013
    * Adisak Intana, Michael R. Poppleton, and Geoff V. Merrett: ''Proof-based formal methods for WSN development with Simulation Approach''
    4 KB (521 words) - 13:15, 13 June 2013
  • Industrial Projects
    ...castle University, Swansea University, Invensys Rail) works on integrating proof-based reasoning about time in state-based models, exemplified by Event-B an
    5 KB (718 words) - 11:40, 23 October 2015
  • Rodin Platform 3.5 Release Notes
    781 Problem with the Rodin proof generator 771 Proof view: unreadable formulas (white on white)
    8 KB (1,249 words) - 13:09, 11 September 2020
  • D45 General Platform Maintenance
    ...types. Along with these additional notations, the user can also define new proof rules (prover extensions). ...es and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. W
    35 KB (5,228 words) - 10:12, 23 April 2012
  • New Proof Rules
    [[Category:Proof]]
    4 KB (738 words) - 12:53, 12 August 2009
  • Rodin Workshop 2010
    :Extending the proof obligation generator : [http://wiki.event-b.org/images/Modelling-verification-proof.pdf Transcript] of a subsequent e-mail discussion between Ken Robinson and
    5 KB (716 words) - 09:28, 22 November 2010
  • New Tactic Providers
    ...owing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
    7 KB (746 words) - 13:00, 12 October 2009
  • Extending the Static Checker (How to extend Rodin Tutorial)
    ..._Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]]}} ...after our extension. The Static Checker (SC) is one dedicated part of the Proof Obligation (PO) generation process. Indeed, the POs are generated from the
    18 KB (2,534 words) - 13:53, 5 September 2013
  • Rodin Workshop 2016
    effective support for modelling and automated proof. The platform is open
    5 KB (664 words) - 18:29, 6 June 2016
  • ADVANCE D3.2 Model Composition and Decomposition
    *Proof obligation were added: Well-Definedness (WD) and Invariant preservation (IN
    6 KB (891 words) - 17:21, 11 December 2012
  • Extending Refinement Actions
    ...d massage the latter so that it statically checks and does not produce any proof obligation.
    5 KB (764 words) - 15:49, 19 April 2011
  • Current Developments
    The instantiation leads to proof obligations approach employed by Event-B: generating proof obligations. We, initially, focus on adding the facility to specify
    12 KB (1,869 words) - 16:35, 18 March 2014
  • D23 Modularisation Plug-in
    * Decomposing proof effort: splitting helps to split verification effort. It also helps to reus
    6 KB (921 words) - 11:43, 8 January 2010
  • Rodin Platform 3.4 Release Notes
    771 Proof view: unreadable formulas (white on white)
    5 KB (758 words) - 16:28, 7 March 2018
  • Mathematical Language Evolution Design
    ! scope=row |Proof ...arget every assignment, expression or predicate in any context, machine or proof file and upgrade their contents to the new language version.<br />
    14 KB (2,104 words) - 09:40, 11 May 2009
  • ADVANCE D3.3 Model Checking
    ...ome properties (like temporal logic ones), that have currently no matching proof support.
    6 KB (1,016 words) - 10:41, 23 September 2013
  • Developer FAQ
    * [[Accessing Proof Obligations|How to access Proof Obligations]].
    15 KB (2,372 words) - 16:29, 19 May 2015
  • Rodin Workshop 2014
    | || 14h40 || Program Development in Event-B with Proof Outlines
    8 KB (1,073 words) - 06:13, 24 June 2014
  • Rodin Platform 3.5.0 External Plug-ins
    ...:green"> available </span> || ?.x.x || || || Improves chance of automatic proof by selecting relevant hypotheses
    9 KB (1,244 words) - 13:52, 1 April 2022
  • Details for Maintaining Main Rodin Update Site
    A goal to be achieved is to rename proof obligations when a refactory occurs (not available in this version).
    39 KB (4,626 words) - 08:33, 6 April 2012
  • Modularisation Plug-in Tutorial
    There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done
    8 KB (1,166 words) - 20:58, 10 November 2009
  • Code Generation Activity
    ...tp://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño. ...Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, th
    17 KB (2,568 words) - 09:03, 19 October 2015
  • Rodin Performances
    Test Builder = SC + POG + POM, no proof attempt is performed.
    7 KB (787 words) - 08:43, 17 June 2011
  • UML-B - Statemachine Animation
    ...intended transition in the refinement. The bug could not be discovered by proof since the bug resulted in a valid refinement, however, the behaviour was ce
    7 KB (1,130 words) - 14:39, 28 January 2010
  • D23 TEXT
    ...ther plug-ins will be able to extend the text editor as well. And last, a proof-of-concept prototype had been put together very quickly.
    8 KB (1,257 words) - 15:56, 28 January 2010
  • DEPLOY Plenary Workshop 2009
    * Jens Bendisposto and Michael Leuschel - Proof Assisted Model Checking for B
    7 KB (1,003 words) - 20:08, 12 October 2009
  • Tasking Event-B Overview
    ...n since it has no guard of its own. In a future enhancement we can produce proof obligations to show that the branch is disjoint and guard coverage is compl
    9 KB (1,528 words) - 08:43, 2 September 2013
  • ADVANCE D3.2 General Platform Maintenance
    ...nd requests were collected along. At the same time, the Event-B models and proof got bigger and bigger, in the same way as the experience of the users invol ...ava heap size which is, for example, extensively used during the automated proof. After a phase of testing and despite the drawbacks of assembling and maint
    20 KB (3,030 words) - 13:18, 18 July 2012
  • UML-B Tutorial
    ...ject oriented style for guards and actions but is not as easy to relate to proof goals in the Event-B prover.''
    11 KB (1,713 words) - 20:07, 18 April 2010
  • Documentation Overhaul DoW
    * Proof Tactics
    9 KB (1,421 words) - 12:41, 8 December 2011
  • ADVANCE D3.2 Model Checking
    ...ome properties (like temporal logic ones), that have currently no matching proof support.
    11 KB (1,711 words) - 09:47, 26 June 2012
  • Generic Event-B EMF extensions
    ...be placed at position 1 whereas a theorem or invariant included purely for proof purposes might be placed at position -10.
    13 KB (1,988 words) - 11:01, 30 May 2020
  • Structured Types
    Regardless of whether the closing axiom is introduced, some feasibility proof obligations arising from the use of the
    18 KB (2,643 words) - 12:41, 12 August 2009
  • D45 Code Generation
    ...de generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as
    12 KB (1,818 words) - 08:31, 20 April 2012
  • Extending the project explorer
    ...ts (''ModelProjects'') where the root file contains elements that can have proof obligations associated (in that case they should extends the abstract class
    20 KB (2,461 words) - 16:33, 24 May 2010
  • Rodin Index Design
    ...for the event-B tools when defining the granularity of static checking and proof obligation generation.
    14 KB (2,204 words) - 12:58, 12 October 2009
  • D45 Scalability
    [[Image:Rodin_Performances_Editor_perf_simplev2_nos.png|850px|Rodin Proof Editor Performances]]
    13 KB (1,991 words) - 20:57, 20 April 2012
  • Variations in HYP, CNTR and GenMP
    The point of this enhancement is therefore to increase the proof power of the considered reasoners by having them consider variations of the ...isplayed : "Project: Number of POs discharged/Number of POs". Finally, the proof files are strored into a directory named "Results" at the same level as the
    11 KB (1,594 words) - 07:08, 8 July 2014
  • Extending the Static Checker
    ...modules are used by the static checker. Similarly, it can be used for the proof obligation generator (POG).
    24 KB (3,013 words) - 16:24, 5 July 2011
  • D32 Code generation
    ...he provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more
    15 KB (2,298 words) - 15:08, 27 January 2011
  • Rodin 3.0 Plug-in Migration Guide
    ...'Theory Plug-in reasoners''', that depend on the mathematical language and proof rules defined in theories, which change over time. Thus, these reasoners sh
    17 KB (2,614 words) - 16:25, 14 February 2014
Retrieved from ‘https://wiki.event-b.org/index.php/Special:Search’