Difference between pages "Theory Release History" and "Rodin Workshop 2021"

Revision as of 14:59, 14 June 2021

9th Rodin User and Developer Workshop

The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)

The proceedings of the workshop is now available as a [technical report] at the University of Southampton.

The programme now available on the ABZ2021 website and below (with texts).

Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset 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 range of plug-ins have already been developed.

The 9th Rodin workshop will be collocated with the ABZ 2021 Conference.

The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.

Programme

09:00 - 10:30

Domain knowledge as Ontology-based Event-B Theories - I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque (pdf, slides)
OntoEventB: A Generator of Event-B contexts from Ontologies - Idir Ait-Sadoune (pdf, slides)
EVBT — an Event-B tool for code generation and documentation - Fredrik Öhrström (pdf, slides)
Scenario Checker: An Event-B tool for validating abstract models - Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

10:30 - 11:00 Break

11:00--12:30

Context instantiation plug-in: a new approach to genericity in Rodin - Guillaume Verdier, Laurent Voisin (pdf, slides)
Examples of using the Instantiation Plug-in - Dominique Cansell, Jean-Raymond Abrial (pdf, slides)
Data-types definitions: Use of Theory and Context instantiations Plugins - Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh (pdf, slides)
Towards CamilleX 3.0 - Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

12:30--13:30 Lunch

13:30--15:00

Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - Jonathan Hammond, Capgemini Engineering (slides)
Large Scale Biological Models in Rodin - Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre (pdf, slides)
Formal Verification of EULYNX Models Using Event-B and RODIN - Abdul Rasheeq, Shubhangi Salunkhe (pdf, slides)

Organisers

Chair: Asieh Salehi Fathabadi, University of Southampton, UK

Co-chair: Thai Son Hoang, University of Southampton, UK

Co-chair: Colin Snook, University of Southampton, UK

Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France

@@ Line 1: / Line 1: @@
-Back to [[Theory Plug-in]].
+==9th Rodin User and Developer Workshop==
-Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.
+The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
-===News===
+''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
-* ''4th June 2021'': [[#Version_4.0.2|Version 4.0.2]] is released. It requires Rodin 3.5.
-* ''22th December 2020'': [[#Version_4.0.1|Version 4.0.1]] is released. It requires Rodin 3.5.
-* ''19th December 2014'': [[#Version_3.0.0|Version 3.0.o]] is released. It requires Rodin 3.1.
-* ''10th July 2014'': [[#Version_2.0.2|Version 2.0.2]] is released. It requires Rodin 2.8.
-* ''24th June 2014'': [[#Version_2.0.1|Version 2.0.1]] is released. It requires Rodin 2.8.
-* ''30th April 2014'': [[#Version_2.0.0|Version 2.0.0]] is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
-* ''20th April 2012'': [[#Version_1.3.2|Version 1.3.2]] is released. It requires Rodin 2.4.
-* ''15th August 2011'': [[#Version_1.2|Version 1.2]] is released. It requires Rodin 2.2.2.
-* ''6th August 2011'': [[#Version_1.1|Version 1.1]] is released. It requires Rodin 2.2.2.
-* ''8th July 2011'': [[#Version_1.0|Version 1.0]] is released. It requires Rodin 2.2.
-* ''22nd May 2011'': [[#Version_0.8|Version 0.8]] released. It is based on Rodin 2.1.1.
-* ''11th April 2011'': [[#Version_0.7|Version 0.7]] released. It is based on Rodin 2.1.1.
-* ''6th January 2011'': [[#Version_0.6|Version 0.6]] released. It is based on Rodin 2.0.1.
-* ''28th October 2010'': [[#Version_0.5|Version 0.5]] released. It is based on Rodin 2.0.
-===Releases===
+The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
-===== Version 4.0.2 =====
-''4th June 2021''
-Release target: Rodin 3.5
+Event-B is a formal method for system-level modelling and analysis. The
-* Bug fixes:
+Rodin Platform is an Eclipse-based toolset for Event-B that provides
-** Datatypes that have several type parameters are now serialized in the right order; it fixes some issues with proofs and proof replay.
+effective support for modelling and automated proof. The platform is open
-** Manually applied inference and rewrite rules are now replayed correctly (in some cases, their replay was displayed as uncertain).
+source and is further extendable with plug-ins. A range of plug-ins have
+already been developed.
-===== Version 4.0.1 =====
+The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].
-''22th December 2020''
-Release target: Rodin 3.5
+The purpose of this workshop  is to bring together existing and potential
-* Bug fixes:
+users and developers of the Rodin  toolset and to foster a broader community
-** The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
+of Rodin users and developers.
-** The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
-** The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
-** Manually applying an inference rule no longer throws a NullPointerException.
-** It is now possible to rename theories.
-** The TheoryPath creation dialog box has been simplified.
-* Optimizations:
-** The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
-** The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
-===== Version 4.0.0-RC1 =====
+For Rodin users the workshop will provide an opportunity to share tool
-''10th April 2017''
+experiences and to gain an understanding of on-going tool developments.
+For plug-in developers the workshop will provide an opportunity to showcase
+their tools and to achieve better coordination of tool development effort.
-Release target: Rodin 3.2
-* AST Extensions (4.0.0) Major API change.
-** Compatibility upgrade to Rodin 3.2
-** Support for get operator position for INFIX extended predicate operators.
-** Improve pattern matching for associative operators.
-* Theory plug-in Branding (0.0.1) Initial version
-* Theory Core (4.0.0) Internal implementation changes.
-** Compatibility upgrade to Rodin 3.2
-** Support for INFIX extended predicate operators.
-** Various bugs fixed.
-* Theory help (2.0.0) User documentations.
-* Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
-** Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
-* Theory Rule-based Prover (4.0.0)
-** Reasoners' input does not contain the proof-obligation context.
-** Use the current sequent's origin to get the proof-obligation context.
-** Bug fixed: translate formula to ensure they have the same formula factory.
-** Added version numbers for reasoners.
-** Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
-* Theory UI (3.0.0)
-===== Version 3.0.0 =====
+=== Programme ===
-''17th December 2014''
-Release target : Rodin 3.1
+'''09:00 - 10:30'''
-* migration changes to Rodin 3.1
+* Domain knowledge as Ontology-based Event-B Theories - ''I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque'' ([[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories.pdf|pdf]], [[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories_slides.pdf|slides]])
+* OntoEventB: A Generator of Event-B contexts from Ontologies - ''Idir Ait-Sadoune'' ([[Media:RodinWorkshop2021_OntoEventB.pdf|pdf]], [[Media:RodinWorkshop2021_OntoEventB_slides.pdf|slides]])
+* EVBT — an Event-B tool for code generation and documentation - ''Fredrik Öhrström'' ([[Media:RodinWorkshop2021_EVBT.pdf|pdf]], [[Media:RodinWorkshop2021_EVBT_slides.pdf|slides]])
+* Scenario Checker: An Event-B tool for validating abstract models - ''Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Scenario Checker.pdf|pdf]], [[Media:RodinWorkshop2021_Scenario Checker_slides.pdf|slides]])
-===== Version 2.0.2 =====
+'''10:30 - 11:00''' ''Break''
-''10th July 2014''
-Release target : Rodin 2.8
+'''11:00--12:30'''
-* bug fixes.
+* Context instantiation plug-in: a new approach to genericity in Rodin - ''Guillaume Verdier, Laurent Voisin'' ([[Media:RodinWorkshop2021_Context instantiation plug-in.pdf|pdf]], [[Media:RodinWorkshop2021_Context instantiation plug-in_slides.pdf|slides]])
+* Examples of using the Instantiation Plug-in - ''Dominique Cansell, Jean-Raymond Abrial'' ([[Media:RodinWorkshop2021_Examples of using the Instantiation Plug-in.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Examples of using the Instantiation Plug-in_slides.jpg|slides]])
+* Data-types definitions: Use of Theory and Context instantiations Plugins - ''Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh'' ([[Media:RodinWorkshop2021_Data-types_definitions.pdf|pdf]], [[Media:RodinWorkshop2021_Data-types_definitions_slides.pdf|slides]])
+* Towards CamilleX 3.0 - ''Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Towards CamilleX 3.0.pdf|pdf]], [[Media:RodinWorkshop2021_Towards CamilleX 3.0_slides.pdf|slides]])
-===== Version 2.0.1 =====
+'''12:30--13:30''' ''Lunch''
-''24th June 2014''
-Release target : Rodin 2.8
+'''13:30--15:00'''
-* bug fixes.
+* Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - ''Jonathan Hammond, Capgemini Engineering'' ([[Media:RodinWorkshop2021_Safety and Security Case Study Experiences with Event-B and Rodin.pdf|slides]])
+* Large Scale Biological Models in Rodin - ''Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre'' ([[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin.pdf|pdf]], [[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin_slides.pptx|slides]])
+* Formal Verification of EULYNX Models Using Event-B and RODIN - ''Abdul Rasheeq, Shubhangi Salunkhe'' ([[Media:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN_slides|slides]])
-===== Version 2.0.0 =====
+=== Organisers ===
-''30th April 2014''
+<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
+<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
-Release target : Rodin 2.8
+<p>Co-chair: Colin Snook, University of Southampton, UK</p>
-* Major changes in the usability.
+<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>
-* Important bug fixes.
-===== Version 1.3.2 =====
-''20th April 2012''
-Release target : Rodin 2.4
-* Important bug fixes.
-* Improvement of deployment and un-deployment wizards
-===== Version 1.2 =====
-''15th August 2011''
-Release target : Rodin 2.2.2
-* Bug fixes.
-* Added capability to instantiate multiple theorems at once.
-* Added automatic tactic for expanding operator definitions RbPxd·
-===== Version 1.1 =====
-''6th August 2011''
-Release target : Rodin 2.2.2
-* Theory library first version.
-* Bug fixes.
-* Improved UI.
-===== Version 1.0 =====
-''8th July 2011''
-Release target : Rodin 2.2
-* Bug fixes.
-* Added import relationships between theories.
-* Added experimental support for recursive definitions.
-* Improved project as well as workspace scope for mathematical and prover extensions.
-* Added tactic (xd) to expand all definitions.
-* Fixed support for polymorphic theorems.
-===== Version 0.8 =====
-''22nd May 2011''
-Release target : Rodin 2.1.1
-* Bug fixes.
-* Added import relationships between theories.
-* Added experimental support for recursive definitions.
-* Added project as well as workspace scope for mathematical and prover extensions.
-===== Version 0.7 =====
-''11th April 2011''
-Bug fixes. Fixed for Rodin 2.1.1.
-===== Version 0.6 =====
-''6th January 2011''
-Minor bug fixes and improvements to theories pretty printer.
-===== Version 0.5 =====
-''28th October 2010''
-This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.
-===Features Requests and Bugs===
-Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.
-[[Category:Theory Plug-in]]

Difference between pages "Theory Release History" and "Rodin Workshop 2021"

Revision as of 14:59, 14 June 2021

9th Rodin User and Developer Workshop

Programme

Organisers

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools