Menu
▾
▴
rodin-b-sharp-devel — Development of the Rodin platform
You can subscribe to this list here.
| 2009 |
Jan
(1) |
Feb
(2) |
Mar
(7) |
Apr
(5) |
May
(3) |
Jun
(9) |
Jul
(3) |
Aug
(1) |
Sep
(3) |
Oct
(9) |
Nov
(9) |
Dec
(10) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2010 |
Jan
(25) |
Feb
(12) |
Mar
(7) |
Apr
(5) |
May
(3) |
Jun
|
Jul
(13) |
Aug
(2) |
Sep
(6) |
Oct
(8) |
Nov
(3) |
Dec
(2) |
| 2011 |
Jan
(9) |
Feb
(2) |
Mar
(10) |
Apr
(2) |
May
(16) |
Jun
(5) |
Jul
(8) |
Aug
(1) |
Sep
(6) |
Oct
(33) |
Nov
(16) |
Dec
(5) |
| 2012 |
Jan
(7) |
Feb
(8) |
Mar
(3) |
Apr
(11) |
May
(3) |
Jun
(1) |
Jul
(5) |
Aug
(2) |
Sep
(1) |
Oct
(4) |
Nov
|
Dec
(5) |
| 2013 |
Jan
(7) |
Feb
(6) |
Mar
(12) |
Apr
(10) |
May
(6) |
Jun
(1) |
Jul
(4) |
Aug
|
Sep
(3) |
Oct
(5) |
Nov
(2) |
Dec
(7) |
| 2014 |
Jan
(33) |
Feb
(14) |
Mar
(6) |
Apr
|
May
(2) |
Jun
(13) |
Jul
(16) |
Aug
(3) |
Sep
(3) |
Oct
(10) |
Nov
(10) |
Dec
(3) |
| 2015 |
Jan
(3) |
Feb
(5) |
Mar
(4) |
Apr
(20) |
May
|
Jun
|
Jul
(1) |
Aug
|
Sep
(1) |
Oct
|
Nov
|
Dec
(1) |
| 2016 |
Jan
|
Feb
(1) |
Mar
(2) |
Apr
|
May
|
Jun
(3) |
Jul
(1) |
Aug
|
Sep
|
Oct
(4) |
Nov
|
Dec
|
| 2017 |
Jan
(1) |
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(4) |
Sep
|
Oct
(3) |
Nov
(1) |
Dec
|
| 2018 |
Jan
|
Feb
|
Mar
|
Apr
(4) |
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(4) |
Nov
|
Dec
|
| 2019 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(2) |
Oct
(7) |
Nov
(5) |
Dec
|
| 2020 |
Jan
|
Feb
|
Mar
(2) |
Apr
(2) |
May
(1) |
Jun
|
Jul
|
Aug
(3) |
Sep
|
Oct
|
Nov
(13) |
Dec
(1) |
| 2021 |
Jan
|
Feb
|
Mar
(1) |
Apr
|
May
(4) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2022 |
Jan
|
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
(8) |
Oct
(1) |
Nov
(1) |
Dec
|
| 2023 |
Jan
|
Feb
(1) |
Mar
(1) |
Apr
(3) |
May
(4) |
Jun
|
Jul
|
Aug
(1) |
Sep
(3) |
Oct
|
Nov
|
Dec
(2) |
| 2024 |
Jan
|
Feb
(3) |
Mar
|
Apr
(2) |
May
|
Jun
(2) |
Jul
(2) |
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <177...@qq...> - 2024-07-31 14:43:32
|
I am using Rodin version 3.8.0. Regarding how to install the Atomicity Decomposition plugin, according to the Atomicity Decomposition Plug-in User Guide - Event-B, I installed the Epsilon tool suite, Epsilon Core (Incubation), Human Usable Textual Notation (Incubation), and Atomicity Decomposition. While creating Flow Diagrams, I followed the steps in the tutorial: open the machine in the Rose editor by right-clicking on the machine. However, when I right-click on the machine as per the tutorial, there is no "Flow Diagram" option. The first image is from the tutorial, showing the "Flow Diagram" option, and the second image is my interface after installing the relevant plugins, where there is no "Flow Diagram" option in the "New Child element" function. What version of Rodin or what other plugins do I need to install to use this functionality? |
|
From: <177...@qq...> - 2024-07-30 13:43:07
|
How to use this function, after installing the corresponding plug-in in accordance with the tutorial or not to use，this tutorial https://wiki.event-b.org/index.php/Atomicity_Decomposition_Plug-in_User_Guide.How to Creating Flow Diagrams |
|
From: Idir A. S. <idi...@ce...> - 2024-06-11 08:47:11
|
Dear All, I am glad to announce that Rodin 3.9 is available. You can either install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.9/) or use the update mechanism of Eclipse. Rodin 3.9 brings several bug fixes. It also upgrades the underlying Eclipse to 2023-12 (4.30), which can be run by Java 17 Runtimes. Rodin will work on macOS, Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin. ---- macOS caveats ---- The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag. ---- Important information ---- Please read the Rodin Platform release notes before proceeding with an upgrade. See https://wiki.event-b.org/index.php/Rodin_Platform_3.9_Release_Notes ---- Fixed Bugs and Implemented Features ---- bug #829: Autorewriter generates invalid proof rule bug #828: Trace debug/rodintypes/verbose doesn't work bug #827: Post-tactic applied after a tactic failure bug #826: NullPointerException in hypothesis page UI bug #824: Exception related to proof tree UI update bug #823: Do not allow prime in extension symbol bug #822: Error handling when loading formula extensions bug #821: Issues with proof tree filtering bug #819: "Prove Automatically" setting not persisted bug #818: Hypothesis hiding by eh/he Feature Requests —— FR #403: User provided names for fresh variables FR #400: Add factory method to check if symbol is valid FR #398: Rewrite rule for recursive exponentiation FR #396: New reasoners on inductive types FR #395: Manual application of compset simplification rules FR #394: Rule for functional image FR #393: Simplify set membership of min/max FR #392: Simplify bool(B=TRUE) to B FR #385: Better message for syntax errors in set comprehension FR #383: Additional inference rule for finiteness FR #368: Better simplification of identity This release would not have happened without the support from the Event-B Rodin Plus project funded by the French National Research Agency (ANR). Best Regards, --- Idir AIT SADOUNE Associate Professor CentraleSupelec - Computer Science Department LMF - Formal Methods Laboratory Paris-Saclay University www.idiraitsadoune.com <https://www.idiraitsadoune.com/> +33/0 1 75 31 78 46 |
|
From: Neeraj K. S. <nee...@to...> - 2024-06-03 12:50:49
|
The 11th Rodin User and Developer Workshop, 25th June, 2024, Bergamo, Italy Rodin Workshop 2024 Website <https://wiki.event-b.org/index.php/Rodin_Workshop_2024> The 11th Rodin workshop will be collocated with the ABZ 2024 Conference <https://abz-conf.org/site/2024/>. 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. If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to ro...@ec... <mailto:ro...@ec...> by 30th May 2024 indicating whether it is a tool usage or tool development presentation. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B. The proceedings of the workshop will be available as a technical report at the University of Southampton. Organisers Asieh Salehi Fathabadi, Senior Research Fellow, University of Southampton Guillaume Verdier, Université de Paris-Est Créteil Kristin Rutenkolk, Heinrich Heine University Düsseldorf Neeraj Kumar Singh, Associate Professor, INPT-ENSEEIHT / IRIT, University of Toulouse Sebastian Stock, Junior Researcher, Johannes Kepler University Laurent Voisin, R&D Manager, Systerel |
|
From: Idir A. S. <idi...@ce...> - 2024-04-23 11:26:45
|
Dear All, I am glad to announce that the first release candidate of Rodin 3.9 is available. You can install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.9-RC1/). This release is based on the latest Eclipse 2023-12 (4.30) and contains numerous bug fixes. Rodin will work on macOS (both x86_64 and aarch 64 architectures), Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin. We are interested in getting as much feedback as possible, especially about bugs or usage issues, before publishing the final release. Please do not hesitate to report anything that looks strange to you. Caution: This is a release candidate. This means that it has not been extensively tested and may contain many bugs, some being nasty. Please do not use it for anything important. macOS caveats ---- The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag. Note: If you open an existing workspace (set of projects) with this release, this workspace will not work anymore with prior releases of Rodin. We encourage you to duplicate your workspace to avoid any issue. Best Regards, --- Idir AIT SADOUNE Associate Professor CentraleSupelec - Computer Science Department LMF - Formal Methods Laboratory Paris-Saclay University www.idiraitsadoune.com <https://www.idiraitsadoune.com/> +33/0 1 75 31 78 46 |
|
From: Neeraj K. S. <nee...@to...> - 2024-04-16 11:02:55
|
The 11th Rodin User and Developer Workshop, 25th June, 2024, Bergamo, Italy Rodin Workshop 2024 Website <https://wiki.event-b.org/index.php/Rodin_Workshop_2024> The 11th Rodin workshop will be collocated with the ABZ 2024 Conference <https://abz-conf.org/site/2024/>. 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. If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to ro...@ec... <mailto:ro...@ec...> by 30th May 2024 indicating whether it is a tool usage or tool development presentation. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B. The proceedings of the workshop will be available as a technical report at the University of Southampton. Organisers Asieh Salehi Fathabadi, Senior Research Fellow, University of Southampton Guillaume Verdier, Université de Paris-Est Créteil Kristin Rutenkolk, Heinrich Heine University Düsseldorf Neeraj Kumar Singh, Associate Professor, INPT-ENSEEIHT / IRIT, University of Toulouse Sebastian Stock, Junior Researcher, Johannes Kepler University Laurent Voisin, R&D Manager, Systerel |
|
From: Michael L. <Mic...@un...> - 2024-02-07 12:13:20
|
Hi Guillaume, thanks a lot, that works very well. By the way, the nightly release of the ProB plugin now supports recursive datatypes and recursive operators from theories. Greetings, Michael > On 7 Feb 2024, at 11:56, Guillaume Verdier <Gui...@ir...> wrote: > > Hi Michael, > > Indeed, comments from the source are not copied to checked files. > > Elements in checked files have an org.eventb.core.source attribute that points to the unchecked element. > In Java, you can use the method getSource() on the ISCEvent object to get back the (unchecked) IEvent. Then, IEvent has the methods hasComment() and getComment(), which are shorter to use than the generic hasAttribute/getAttributeValue. > > Greetings, > Guillaume |
|
From: Guillaume V. <Gui...@ir...> - 2024-02-07 11:13:58
|
Hi Michael,
Indeed, comments from the source are not copied to checked files.
Elements in checked files have an org.eventb.core.source attribute that points to the unchecked element.
In Java, you can use the method getSource() on the ISCEvent object to get back the (unchecked) IEvent. Then, IEvent has the methods hasComment() and getComment(), which are shorter to use than the generic hasAttribute/getAttributeValue.
Greetings,
Guillaume
> On 7 Feb 2024, at 11:16, Michael Leuschel <Mic...@un...> wrote:
>
> Hi everybody,
>
> I would like to retrieve the comment attribute for certain objects like events and invariants in the Java code of the ProB plugin.
>
> In one method I have an object revent of type ISCEvent and I have tried the following piece of code as a test, but it seems that no event has the comment attribute :
>
> if (revent.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
> final String commentString = revent.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
> System.out.println("Description of event " + revent.getLabel() + ": "+ commentString);
> }
>
> I noticed that the M1.bum file of my model M1 contains the comment:
>
> <org.eventb.core.event name="var4" org.eventb.core.comment="update the AMAN display" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="display”>
>
> but the file M1.bcm file does not:
>
> <org.eventb.core.scEvent name="diplayedLabelu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="display" org.eventb.core.source="/STTT_AMAN_Corr_1_v19/M1.bum|org.eventb.core.machineFile#M1|org.eventb.core.event#var4”>
>
>
> I guess I somehow need to find the associated unchecked event object (IEvent??) and retrieve the comment there?
> Can somebody show me how this can be done?
>
> (Sorry, I am more of a Prolog programmer ;-))
>
> Greetings,
> Michael
>
> _______________________________________________
> Rodin-b-sharp-devel mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel
|
|
From: Michael L. <Mic...@un...> - 2024-02-07 10:33:24
|
Hi everybody,
I would like to retrieve the comment attribute for certain objects like events and invariants in the Java code of the ProB plugin.
In one method I have an object revent of type ISCEvent and I have tried the following piece of code as a test, but it seems that no event has the comment attribute :
if (revent.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
final String commentString = revent.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
System.out.println("Description of event " + revent.getLabel() + ": "+ commentString);
}
I noticed that the M1.bum file of my model M1 contains the comment:
<org.eventb.core.event name="var4" org.eventb.core.comment="update the AMAN display" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="display”>
but the file M1.bcm file does not:
<org.eventb.core.scEvent name="diplayedLabelu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="display" org.eventb.core.source="/STTT_AMAN_Corr_1_v19/M1.bum|org.eventb.core.machineFile#M1|org.eventb.core.event#var4”>
I guess I somehow need to find the associated unchecked event object (IEvent??) and retrieve the comment there?
Can somebody show me how this can be done?
(Sorry, I am more of a Prolog programmer ;-))
Greetings,
Michael
|
|
From: Guillaume V. <Gui...@ir...> - 2023-12-14 10:44:42
|
Dear Michael,
The representation in static-checked and deployed theory files is related to the way datatypes are built within Rodin core.
The documentation of org.eventb.core.ast.datatype.IConstructorBuilder states: “[…] the datatype type parameters are represented as GivenTypes with the type parameter name and the datatype type is represented as a GivenType using the datatype name (without any reference to its type parameters). E.g.: for the list datatype, List(S), reference to S must be done using the given type S and reference to List(S) using the given type List.”
This leads to the behaviour you observed, where the type of cdr is just a bare MyList without its type parameters: it is exactly the form required by the datatype builder, so data read from .tcf or .dtf files can be fed directly to this builder.
No information is lost, since the type parameters are listed in the datatype declaration, in <org.eventb.theory.core.scTypeArgument> elements, before the <org.eventb.theory.core.scDatatypeConstructor> elements.
Basically, in the Theory plug-in, recreating an IDatatype from data in a .tcf/.dtf is just something like this:
List<GivenType> typeArguments = new ArrayList<GivenType>();
for (ISCTypeArgument scTypeArg : definition.getTypeArguments()) {
typeArguments.add(scTypeArg.getSCGivenType(factory));
}
IDatatypeBuilder dtBuilder = factory.makeDatatypeBuilder(definition.getIdentifierString(), typeArguments, origin);
for (ISCDatatypeConstructor cons : definition.getConstructors()) {
IConstructorBuilder consBuilder = dtBuilder.addConstructor(cons.getIdentifierString());
for (ISCConstructorArgument dest : cons.getConstructorArguments()) {
consBuilder.addArgument(dest.getIdentifierString(), dest.getType(factory));
}
}
return dtBuilder.finalizeDatatype();
Best regards,
Guillaume
|
|
From: Michael L. <Mic...@un...> - 2023-12-12 10:30:35
|
Hi,
following yesterday’s discussion at the EBRP meeting, I was just checking that ProB still works with operators defined recursively on inductive data types (defined in the theory plugin).
I found out that I had problems with parameterized inductive datatypes (even for examples where ProB did work in the past).
I wrote a simple List example with a constructor CONS (see below).
In the file MyList.tuf I have this declaration:
<org.eventb.theory.core.datatypeConstructor name=")" org.eventb.core.identifier="CONS">
<org.eventb.theory.core.constructorArgument name="'" org.eventb.core.identifier="car" org.eventb.theory.core.type="T"/>
<org.eventb.theory.core.constructorArgument name="(" org.eventb.core.identifier="cdr" org.eventb.theory.core.type="MyList(T)"/>
</org.eventb.theory.core.datatypeConstructor>
Observe the type of the destructor cdr is MyList(T).
However, in the file MyList.dtf the type parameter is now gone and the type is just written as MyList, which results in parsing errors in our ProB translator:
<org.eventb.theory.core.scDatatypeConstructor name="CONS" org.eventb.core.source="/TestInductiveDatatypes/MyList.tuf|org.eventb.theory.core.theoryRoot#MyList|org.eventb.theory.core.datatypeDefinition#'|org.eventb.theory.core.datatypeConstructor#)">
<org.eventb.theory.core.scConstructorArgument name="car" org.eventb.core.source="/TestInductiveDatatypes/MyList.tuf|org.eventb.theory.core.theoryRoot#MyList|org.eventb.theory.core.datatypeDefinition#'|org.eventb.theory.core.datatypeConstructor#)|org.eventb.theory.core.constructorArgument#'" org.eventb.core.type="T"/>
<org.eventb.theory.core.scConstructorArgument name="cdr" org.eventb.core.source="/TestInductiveDatatypes/MyList.tuf|org.eventb.theory.core.theoryRoot#MyList|org.eventb.theory.core.datatypeDefinition#'|org.eventb.theory.core.datatypeConstructor#)|org.eventb.theory.core.constructorArgument#(" org.eventb.core.type="MyList"/>
</org.eventb.theory.core.scDatatypeConstructor>
Is this intended behvaviour or a bug?
Greetings,
Michael
|
|
From: Laurent V. <lau...@sy...> - 2023-09-08 13:38:02
|
Dear Michael, I have just checked in the parser. This is even more restricted. The oftype operator can only occur: Just after the definition of a bound identifier (i.e., in a quantification), Just after a generic atomic expression (`id`, `prj1`, `prj2`, the empty set or an extended atomic operator). It is followed by a type formula which is parsed greedily (that is until the next token cannot be part of a type formula). Cheers, Laurent. > Le 8 sept. 2023 à 12:49, Laurent Voisin via Rodin-b-sharp-devel <rod...@li...> a écrit : > > Dear Michael, > > If I remember well, it is the highest priority on the left, it should apply only to the preceding token. On the right, I should take any type formula (not an expression). Most often, it is surrounded with parentheses to limit the range on the right-hand side. > > I will check later in the source code of the parser to give you a more precise definition. > > Cheers, > Laurent. > >> Le 8 sept. 2023 à 09:58, Michael Leuschel <Mic...@un...> a écrit : >> >> Hi, >> Do you know what the priority of the oftype operator is? >> In the kernel_lang_20.pdf it is not yet mentioned and neither the Rodin Handbook nor https://wiki.event-b.org/index.php/Rodin_Keyboard_User_Guide contains operator priorities. >> >> Greetings, >> Michael >> >> _______________________________________________ >> Rodin-b-sharp-devel mailing list >> Rod...@li... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel > > > > _______________________________________________ > Rodin-b-sharp-devel mailing list > Rod...@li... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel |
|
From: Laurent V. <lau...@sy...> - 2023-09-08 11:34:32
|
Dear Michael, If I remember well, it is the highest priority on the left, it should apply only to the preceding token. On the right, I should take any type formula (not an expression). Most often, it is surrounded with parentheses to limit the range on the right-hand side. I will check later in the source code of the parser to give you a more precise definition. Cheers, Laurent. > Le 8 sept. 2023 à 09:58, Michael Leuschel <Mic...@un...> a écrit : > > Hi, > Do you know what the priority of the oftype operator is? > In the kernel_lang_20.pdf it is not yet mentioned and neither the Rodin Handbook nor https://wiki.event-b.org/index.php/Rodin_Keyboard_User_Guide contains operator priorities. > > Greetings, > Michael > > _______________________________________________ > Rodin-b-sharp-devel mailing list > Rod...@li... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel |
|
From: Michael L. <Mic...@un...> - 2023-09-08 08:13:55
|
Hi, Do you know what the priority of the oftype operator is? In the kernel_lang_20.pdf it is not yet mentioned and neither the Rodin Handbook nor https://wiki.event-b.org/index.php/Rodin_Keyboard_User_Guide contains operator priorities. Greetings, Michael |
|
From: Cheng-Hao C. <che...@mo...> - 2023-08-04 06:16:19
|
The ICFEM Doctoral Symposium is an international forum for PhD students studying all areas related to formal methods for software, hardware and system development. This forum is an excellent opportunity bringing together PhD students and well-known established researchers from the formal methods community. It will also provide PhD students with fruitful feedback and advice on their research approach and enable them to interact with other PhD students in order to stimulate the exchange of ideas and the sharing of experiences among participants. In summary, the PhD forum will provide PhD students with an ideal opportunity to present, share and discuss their research in a constructive and critical scientific atmosphere. We seek submissions from PhD students who have either determined the direction of their thesis research (probably with some preliminary results already published), but who still have substantial work to complete; or PhD student participants who are in the early stages of their dissertations. It is not required to have a paper accepted at the main conference in order to participate in the ICFEM Doctoral Symposium. Submissions to the Doctoral Symposium should include: Title of the research, the author name (single name) and affiliation; Context and motivation; Problem statement and related work; Proposed solutions and current research efforts, their significance, methodology, results and analysis, and future work. The paper should be prepared using the LNCS format ( https://www.springer.com/gp/computer-science/lncs/new-latex-templates-available/15634678) and submitted in PDF format via easychair. https://easychair.org/my/conference?conf=icfem2023. We accept two types of submissions: (a) 2-page extended abstracts which will not be included in the ICFEM proceedings; and (b) 6-page papers which will be published in the LNCS volume of Springer as part of the main ICFEM proceedings. Authors with accepted submissions are expected to attend the Doctoral Symposium in person to present their work. A discounted registration fee for Doctoral Symposium participants will be announced later. Important Dates: Submission deadline: 25 Aug 2023 (AoE) Notification: 30 Aug 2023 Camera-ready Due: 5 Sep 2023 Doctoral Symposium: 22 Nov 2023 Thanks for your participation! Best regards, ICFEM 2023 Program Committee |
|
From: Cheng-Hao C. <che...@mo...> - 2023-05-20 15:34:39
|
Dear colleagues, As requested by some of you, we have extended the deadline for abstract and paper submission by one week. The new dates are Important Dates --------------------- - Abstract Submission: May 21, 2023 (AOE) - Paper Submission: May 28, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 Below is the rest of the call for papers: looking forward to your submissions. Best regards, ICFEM 2023 PC Co-Chairs Sofiene Tahar, Concordia University Yi Li, Nanyang Technological University *24th International Conference on Formal Engineering Methods (ICFEM 2023**)* https://formal-analysis.com/icfem/2023/ *Overview* ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023. *Topics of Interest* Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to: - Abstraction, refinement and evolution - Formal specification and modelling - Formal verification and analysis - Model checking and equivalence checking - Automated and interactive theorem proving - Formal approaches to software testing and inspection - Formal methods for self-adaptive systems - Formal methods for object-oriented systems - Formal methods for component-based systems - Formal methods for concurrent and real-time systems - Formal methods for cloud computing - Formal methods for cyber-physical systems - Formal methods for hardware and embedded systems - Formal methods for software safety and security - Formal methods for software reliability and dependability - Development, integration and experiments involving verified systems - Formal certification of products under international standards - Formal model-based development and code generation *Important Dates* - Abstract Submission: May 14, 2023 (AOE) - Paper Submission: May 21, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/ *Submission Instructions * Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=icfem2023 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details here <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines> ). *Organizing Committee* General Co-Chairs - Jin Song Dong, NUS and Griffith University, Singapore/Australia - Guangdong Bai, The University of Queensland, Australia Program Co-Chairs - Yi Li, Nanyang Technological University, Singapore - Sofiene Tahar, Concordia University, Canada Finance Chair - Zhe Hou, Griffith University, Australia Publicity Chair - Cheng-Hao Cai, Monash University at Suzhou, China - Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France - Xiaodong Qi, Nanyang Technological University, Singapore Workshop Chair - Xiaofei Xie, Singapore Management University, Singapore Publication Chair - Xiaodong Qi, Nanyang Technological University, Singapore |
|
From: Cheng-Hao C. <che...@mo...> - 2023-05-08 05:42:50
|
CFP: 28th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2023) --------------- CALL FOR PAPERS --------------- PRDC 2023 is the 28th event in a series of symposia started in 1989 devoted to dependable and fault-tolerant computing; it encompasses fundamental theoretical approaches, practical experimental projects, and commercial components and systems. This symposium is recognized as the main event in the Pacific Rim area, and it provides a forum for countries around the world to exchange ideas for improving the dependability of computing systems. https://prdc.dependability.org/PRDC2023 ------------------------------ Venue ------------------------------ Singapore Management University, Singapore ------------------------------ Important Dates (Anywhere on Earth) ------------------------------ Abstract submission: 15 July 2023 Paper submission: 21 July 2023 Rebuttal: 23 - 25 Aug 2023 Author notification: 5 Sept 2023 Camera-ready version: 20 Sept 2023 Conference: 24 - 27 Oct 2023 ------------------------------ Scope ------------------------------ Topics of interest include (but not limited to): Software and hardware reliability, resilience, safety, security, testing, verification, and validation Dependability measurement, modeling, evaluation, and tools Self-healing, self-protecting, and fault-tolerant systems Architecture and system design for dependability Prognostics in Complex Systems Reliability analysis of Complex Systems Fault-tolerant algorithms and protocols Cloud computing resiliency, security and privacy Software defined networks architectures and protocols Dependability issues in computing systems (e.g. computer networks and communications, high performance computing, real-time systems, storage and databases systems, cyber-physical systems, socio-technical systems, and blockchain and smart contracts). Emerging technologies (autonomous systems including autonomous vehicles, human machine teaming, smart devices/Internet of Things) ------------------------------ Main Track Submission ------------------------------ Manuscripts may be submitted in IEEE double-column format to one of the following two categories: (i) Regular Papers and (ii) Practical Experience Reports. Regular Papers (10 pages, excluding references and appendices) should describe original research. Case Studies (6 pages, excluding references and appendices) should describe an experience or a case study, such as the design and deployment of a system or actual failure and recovery field data. All submissions must be made electronically (in PDF format) on the submission website. https://prdc2023.hotcrp.com/ Please note that all submissions will undergo a double-blind review. ------------------------------ Industry Track Submission ------------------------------ The Industry Track provides a forum for researchers and practitioners from industry to present and debate R&D challenges, practical solutions, case studies, and share field reliability data. Papers should be in the IEEE double-column format. The Industry Track at PRDC 2023 is soliciting industry papers in two categories: Regular paper submission consisting of 6 pages (excluding references). Position paper submission consisting of 2 pages (excluding references). https://prdc2023-industry.hotcrp.com/ ------------------------------ Fast Abstract Track Submission ------------------------------ Fast Abstracts are lightly-reviewed manuscripts 2 pages in IEEE double-column format (excluding references and appendices) describing unpublished, in-progress, novel work, opinions or ideas. The submitted Fast Abstracts must be in .pdf format and completely ready for printing. To upload your paper, please use the submission site. https://prdc2023-fast.hotcrp.com/ ------------------------------ Publication ------------------------------ Accepted papers from all tracks will be published by the IEEE Computer Society Press (EI Indexed). Submission of a contribution indicates agreement to have one author present the work, if accepted, at the conference. ------------------------------ Journal Special Issue ------------------------------ Selected papers will be invited to publish in IEEE Transactions on Dependable and Secure Computing (TDSC) and a special issue of Formal Aspects of Computing (FAC). ------------------------------ Paper Awards ------------------------------ Outstanding papers will be selected to receive the following awards: 2023 IEEE Distinguished Contribution Award on Dependable Computing 2023 IEEE Distinguished Industrial Contribution Award on Dependable Computing 2023 IEEE Distinguished Visionary Poster Award on Dependable Computing ------------------------------ Organising Committee ------------------------------ Honorary General Chair Jin Song Dong, National University of Singapore, Singapore General Co-Chairs Jun Sun, Singapore Management University, Singapore Yang Liu, Nanyang Technological University, Singapore Program Co-Chairs Yun Lin, Shanghai Jiao Tong University, China Zhe Hou, Griffith University, Australia Publicity Co-chairs Naipeng Dong, University of Queensland, Australia David Sanan, Singapore Institute of Technology, Singapore Xiaoning Du, Monash University, Australia Industry Track Co-chairs Yan Liu, Runtime Verification, Australia Peng Di, Ant Group, China Fast Abstract Track Co-chairs Babu Pillai, Southern Cross University, Australia Ruitao Feng, University of New South Wales, Australia Jie Zhang, King’s College London, UK Local Arrangement Chair Xiaofei Xie, Singapore Management University, Singapore Web Chair Jian Wang, Nanyang Technological University, Singapore Steering Committee Dan Dongseong Kim, The University of Queensland (Chair) Yennun Huang, Academia Sinica Nobuyasu Kanekawa, Hitachi Research Lab Jin Song Dong, National University of Singapore Karthik Pattabiraman, University of British Columbia Gernot Heiser, University of New South Wales Sy-Yen Kuo, National Taiwan University Zhi Jin, Peking University Jin Hong, University of Western Australia Hyoungshick Kim, Sungkyunkwan University Thanks! Best regards, -------------- Cheng-Hao Cai Monash Suzhou Research Institute Faculty of Information Technology Monash University |
|
From: Neeraj K. S. <ns...@en...> - 2023-05-05 14:21:30
|
***************************************************************************************** 24th International Conference on Formal Engineering Methods (ICFEM 2023) https://formal-analysis.com/icfem/2023/ ***************************************************************************************** ## Overview ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023. ##Topics of Interest Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to: - Abstraction, refinement and evolution - Formal specification and modelling - Formal verification and analysis - Model checking and equivalence checking - Automated and interactive theorem proving - Formal approaches to software testing and inspection - Formal methods for self-adaptive systems - Formal methods for object-oriented systems - Formal methods for component-based systems - Formal methods for concurrent and real-time systems - Formal methods for cloud computing - Formal methods for cyber-physical systems - Formal methods for hardware and embedded systems - Formal methods for software safety and security - Formal methods for software reliability and dependability - Development, integration and experiments involving verified systems - Formal certification of products under international standards - Formal model-based development and code generation ##Important Dates - Abstract Submission: May 14, 2023 (AOE) - Paper Submission: May 21, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/ Submission Instructions Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=icfem2023 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines). ## Organizing Committee General Co-Chairs - Jin Song Dong, NUS and Griffith University, Singapore/Australia - Guangdong Bai, The University of Queensland, Australia Program Co-Chairs - Yi Li, Nanyang Technological University, Singapore - Sofiene Tahar, Concordia University, Canada Finance Chair - Zhe Hou, Griffith University, Australia Publicity Chair - Cheng-Hao Cai, Monash University at Suzhou, China - Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France Workshop Chair - Xiaofei Xie, Singapore Management University, Singapore > |
|
From: Cheng-Hao C. <che...@mo...> - 2023-05-02 14:23:32
|
https://formal-analysis.com/icfem/2023/ Important Dates - Abstract Submission: May 14, 2023 (AOE) - Paper Submission: May 21, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/ Overview ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023. Topics of Interest Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to: - Abstraction, refinement and evolution - Formal specification and modelling - Formal verification and analysis - Model checking and equivalence checking - Automated and interactive theorem proving - Formal approaches to software testing and inspection - Formal methods for self-adaptive systems - Formal methods for object-oriented systems - Formal methods for component-based systems - Formal methods for concurrent and real-time systems - Formal methods for cloud computing - Formal methods for cyber-physical systems - Formal methods for hardware and embedded systems - Formal methods for software safety and security - Formal methods for software reliability and dependability - Development, integration and experiments involving verified systems - Formal certification of products under international standards - Formal model-based development and code generation Submission Instructions Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=icfem2023 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details here). Organizing Committee General Co-Chairs - Jin Song Dong, NUS, Singapore - Guangdong Bai, The University of Queensland, Australia Program Co-Chairs - Yi Li, Nanyang Technological University, Singapore - Sofiene Tahar, Concordia University, Canada Finance Chair - Zhe Hou, Griffith University, Australia Publicity Chair - Cheng-Hao Cai, Monash University at Suzhou, China - Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France Workshop Chair - Xiaofei Xie, Singapore Management University, Singapore Thanks! Best regards, ----------------- Cheng-Hao Cai Monash Suzhou Research Institute Faculty of Information Technology Monash University |
|
From: Dana D. <D.D...@so...> - 2023-04-17 11:20:19
|
The 10th Rodin User and Developer Workshop, 30th May, 2023, Nancy, France Rodin Workshop 2023 Website<http://wiki.event-b.org/index.php/Rodin_Workshop_2023> The 10th Rodin workshop will be collocated with the ABZ 2023 Conference<https://abz2023.loria.fr/>. 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. If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to ro...@ec...<mailto:ro...@ec...?subject=%5BRodinWorkshop2023%5D%20Contribution> by 28th April 2023 indicating whether it is a tool usage or tool development presentation. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B. The proceedings of the workshop will be available as a technical report at the University of Southampton. Organisers Dana Dghaym, University of Southampton Laurent Voisin, Systerel Fabian Vu, Heinrich Heine University Düsseldorf Neeraj Kumar Singh, INPT-ENSEEIHT / IRIT, Univeristy of Toulouse |
|
From: Cheng-Hao C. <che...@mo...> - 2023-04-06 07:21:38
|
*CFP: 24th International Conference on Formal Engineering Methods (ICFEM 2023) please help disseminate!* https://formal-analysis.com/icfem/2023/ *Overview* ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023. *Topics of Interest* Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to: - Abstraction, refinement and evolution - Formal specification and modelling - Formal verification and analysis - Model checking and equivalence checking - Automated and interactive theorem proving - Formal approaches to software testing and inspection - Formal methods for self-adaptive systems - Formal methods for object-oriented systems - Formal methods for component-based systems - Formal methods for concurrent and real-time systems - Formal methods for cloud computing - Formal methods for cyber-physical systems - Formal methods for hardware and embedded systems - Formal methods for software safety and security - Formal methods for software reliability and dependability - Development, integration and experiments involving verified systems - Formal certification of products under international standards - Formal model-based development and code generation *Important Dates* - Abstract Submission: May 14, 2023 (AOE) - Paper Submission: May 21, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/ *Submission Instructions * Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=icfem2023 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details here <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines> ). *Organizing Committee* General Co-Chairs - Jin Song Dong, NUS and Griffith University, Singapore/Australia - Guangdong Bai, The University of Queensland, Australia Program Co-Chairs - Yi Li, Nanyang Technological University, Singapore - Sofiene Tahar, Concordia University, Canada Finance Chair - Zhe Hou, Griffith University, Australia Publicity Chair - Cheng-Hao Cai, Monash University at Suzhou, China - Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France Workshop Chair - Xiaofei Xie, Singapore Management University, Singapore -------------- Cheng-Hao Cai Monash Suzhou Research Institute Monash University |
|
From: Idir A. S. <idi...@ce...> - 2023-04-04 10:51:33
|
Dear All, I am glad to announce that Rodin 3.8 is available. You can either install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.8/) or use the update mechanism of Eclipse. Rodin 3.8 brings several bug fixes. It also upgrades the underlying Eclipse to 2022-03 (4.23), which can be run by Java 11 Runtimes. Rodin will work on macOS, Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 11 or later) installed on your computer to run Rodin. ---- macOS caveats ---- The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag. ---- Important information ---- Please read the Rodin Platform release notes before proceeding with an upgrade. See https://wiki.event-b.org/index.php/Rodin_Platform_3.8_Release_Notes ---- Fixed Bugs and Implemented Features ---- 701: Translation occurs unexpectedly 778: Bad presentation of tactic profiles 802: refresh Project Explorer 803: rule DATATYPE_INDUCTION is unsound 804: FormulaExtensionProviderRegistry does not catch exceptions 805: IAE when loading proof 806: Missing UI indicator when running post tactic 807: Proof information view text cut off 809: store options files in binary plug-ins 811: hypothesis text cut off after instantiation input 812: dropdown arrow invisible in Event-B editor on macOS 813: Missing translation in input area of Proof control 814: ArrayIndexOutOfBounds when typing extended predicates 816: ConcurrentModificationException in editor 817: Exception when using external provers with theory... Feature Requests 170: Bijection and cardinality 292: Make FiniteHypBoundedGoal smarter 339: Add auto tactic for not empty set 343: Generalized Modus Ponens on natural integers 342: Generalized Modus Ponens on Boolean expressions 365: Proof rule for finiteness of generalized union 367: extend IParent in ISCContext 371: apply equality and hide it 372: Proof by case on union membership 376: Min and max definitions 377: Apply modus ponens after instantiation 382: Get free identifiers from a type environment This release would not have happened without the support from the Event-B Rodin Plus project funded by the French National Research Agency (ANR). Best Regards, Idir |
|
From: <ns...@en...> - 2023-03-31 07:00:02
|
***************************************************************************************** 24th International Conference on Formal Engineering Methods (ICFEM 2023) https://formal-analysis.com/icfem/2023/ ***************************************************************************************** ## Overview ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023. ##Topics of Interest Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to: - Abstraction, refinement and evolution - Formal specification and modelling - Formal verification and analysis - Model checking and equivalence checking - Automated and interactive theorem proving - Formal approaches to software testing and inspection - Formal methods for self-adaptive systems - Formal methods for object-oriented systems - Formal methods for component-based systems - Formal methods for concurrent and real-time systems - Formal methods for cloud computing - Formal methods for cyber-physical systems - Formal methods for hardware and embedded systems - Formal methods for software safety and security - Formal methods for software reliability and dependability - Development, integration and experiments involving verified systems - Formal certification of products under international standards - Formal model-based development and code generation ##Important Dates - Abstract Submission: May 14, 2023 (AOE) - Paper Submission: May 21, 2023 (AOE) - Author Notification: July 30, 2023 - Camera-ready versions: Aug 13, 2023 - Conference: Nov 21-24, 2023 More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/ Submission Instructions Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=icfem2023 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines). ## Organizing Committee General Co-Chairs - Jin Song Dong, NUS and Griffith University, Singapore/Australia - Guangdong Bai, The University of Queensland, Australia Program Co-Chairs - Yi Li, Nanyang Technological University, Singapore - Sofiene Tahar, Concordia University, Canada Finance Chair - Zhe Hou, Griffith University, Australia Publicity Chair - Cheng-Hao Cai, Monash University at Suzhou, China - Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France Workshop Chair - Xiaofei Xie, Singapore Management University, Singapore |
|
From: Idir A. S. <idi...@ce...> - 2023-02-22 12:09:54
|
Dear All, I am glad to announce that the first release candidate of Rodin 3.8 is available. You can install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.8-RC1/). This release is based on the latest Eclipse 2022-03 (4.23) and contains numerous bug fixes. Rodin will work on macOS (both x86_64 and aarch 64 architectures), Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 11 or later) installed on your computer to run Rodin. We are interested in getting as much feedback as possible, especially about bugs or usage issues, before publishing the final release. Please do not hesitate to report anything that looks strange to you. Caution: This is a release candidate. This means that it has not been extensively tested and may contain many bugs, some being nasty. Please do not use it for anything important. macOS caveats ---- The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag. Note: If you open an existing workspace (set of projects) with this release, this workspace will not work anymore with prior releases of Rodin. We encourage you to duplicate your workspace to avoid any issue. Best Regards, -- *Idir AIT SADOUNE* Associate Professor CentraleSupelec - Computer Science Department LMF - Formal Methods Laboratory Paris-Saclay University www.idiraitsadoune.com <https://www.idiraitsadoune.com> +33/0 1 69 85 14 88 |
|
From: yk y. <yy...@ho...> - 2022-11-01 16:26:40
|
Hi Rodin development team,
I’m sending this mail regarding the automated proving capability of Robin’s prover.
I’m a personal developer from China. Recently I knew about formal method and its software engeneering which is really amazing. So I tried some tools like CZT, Atelier B(both stopped updating) and finally Event-B on Robin v3.7. I should say Rodin is what I want. Easy to use, excellent GUI (with iUML-B plug-in)... Thanks for your effort on it.
But I still got a bit confused about the automated proving capability of the integrated prover. At most time it works fine, but sometimes it fails to prove theroms like “1+1 ∈ {1,2,3,4}” which is obviously true, and some others. I read the v2.8 handbook and added prover like P0 & ML to my profile and the problem remained. As a beginner I don’t know how to proceed.
I get the info from the wiki that there used to be a Isabelle plug-in which was said better than newPP in automated proving perspective. But that plug-in was not updated since ~ten years ago.
I also checked the release date and it shows some improvement about the prover from v3.0 to v3.3, not for later version since v3.4.
I just wonder about whether the prover was still in the development plan?
1. There is a plan to improve the integrated prover in the future.
2. There is a plan to develop another plug-in to introduce other external provers. (As I know Isabelle2022 has vscode client support, maybe a simillar one?)
3. The integrated prover is good enough (almost as good as Isablelle now?), no plan to improve it.
Which could be the answer? Sorry to disturb you and look forward to your reply. Thanks!
|
5 messages has been excluded from this view by a project administrator.