Search results

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

• 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
• D23 Pattern Plug-in
  ...model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is ...ncludes the achievements of the pattern and is correct without proving any proof obligation.
  6 KB (1,034 words) - 14:43, 27 January 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
• 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
• 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
• 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
• 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
• 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
• Rodin Workshop 2014
  ...rmalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns [http://wiki.event-b.org/images/ZGraja-RodinWorkshop2014.pdf] | || 14h40 || Program Development in Event-B with Proof Outlines
  8 KB (1,073 words) - 06:13, 24 June 2014
• D45 Scalability
  ...for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overc The idea of design patterns in software engineering is to have a general and reusable solution to commo
  13 KB (1,991 words) - 20:57, 20 April 2012
• Rodin Workshop 2009
  ...tp://wiki.event-b.org/images/Reasoned_modelling.pdf A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in] ...rg/images/Slides_matoussi_-Southampton-.pdf Expressing KAOS Goal Refinement Patterns with Event-B ]
  5 KB (766 words) - 09:59, 21 September 2011
• 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
• 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
• D45 General Platform Maintenance
  :*Possibility to highlight patterns in the Proving UI, * '''Possibility to highlight patterns in the Prover UI'''
  35 KB (5,228 words) - 10:12, 23 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 The contentExtension patterns correspond to the ids in the contentProvider and actionProvider extension-p
  20 KB (2,461 words) - 16:33, 24 May 2010