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
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
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! |
From: Guillaume V. <Gui...@ir...> - 2022-10-14 14:51:50
|
Dear Michael, I looked into the bugs you reported. Sadly, I could not find a way to isolate them and fix them quickly for a bug-fix release. I keep working on the next major version of the Theory plug-in that should fix lots of bugs, including the ones you encountered. I also created tickets in the feature requests tracker for new literals (strings and real numbers) and operator overloading. However, after discussing it with Laurent, it seems that this will require quite some work to integrate in the parser, so it will probably not be implemented very soon. Best regards, Guillaume |
From: Laurent V. <lau...@sy...> - 2022-09-29 13:08:27
|
Dear Ilya, A very warm thank you for sharing all that, and moreover for taking the time to explain in great details what you have done and why (rather than just dumping the code without any explanation). After a quick glance, it does not seem that we can integrate all of it to the Rodin platform yet, but it gives us a very good base for implementing your ideas in a more robust way. Thank you again for your very interesting contribution to the Rodin ecosystem. I hope that your new job will allow you to continue using the Rodin platform, and possibly suggest plenty of other improvements. Cheers, Laurent. > Le 28 sept. 2022 à 12:20, Ilya Shchepetkov <ily...@gm...> a écrit : > > Hello everyone! > > A year ago I was working on some changes to the Rodin platform. I had two goals: to increase the number of automatically discharged proof obligations, and to try to parallelize the whole proving process in order to significantly speed it up. The work is not fully finished and currently unmaintained, since I work at a different company now, but I had some success and would like to share the results. Hope it will be of some use! > > First, I’ve made “Retry Auto Provers”, “Recalculate Auto Status” and “Proof Replay on Undischarged POs” actions to run in parallel, so now they are able to process several POs at once. It resulted in approximately 6 times speedup on the Intel machine with 4 CPU cores, and the proving process for some of my models now takes minutes and not hours. The main issue here: I’ve achieved this by removing some locks in the code, which likely introduced some new race conditions. This needs to be investigated and addressed, plus currently there is a bug: with large models, GUI window “Applying Auto Provers…” can disappear long before the proving is complete. > > Second, I’ve created a new combinator tactic called “First Successful”, which allows to run several tactics in parallel. It finishes when either one of the tactic finds the necessary proof, or when they all fail. For example, if you run “First Successful” on 6 different provers and SMT solvers with 1 second timeout for each, then at worst you will need to wait 1 second instead of 6, but at best — only a fraction of that time. > > Using this combinator tactic, I’ve developed a tactic profile especially for interactive proofs: “Default Interactive tactic with SMT”. Its goal is to heavily reduce the waiting time during interactive proofs: every time you choose to run auto provers, it is guaranteed to finish within 1 second. Since you usually do it multiple times per proof, the total time savings are quite significant. In practice, I found this new interactive tactic more valuable, then simple parallelization of “Retry Auto Provers”, “Recalculate Auto Status” and “Proof Replay on Undischarged POs” actions. > > Third, there are a few more small additions: > * There are a few rewrite rules that I often use during interactive proofs, but are absent from the tactic profile editor (Event-B -> Sequent Prover -> Auto/Post Tactic -> Profiles). I’ve added them to the list of available tactics, so now they can be used to automate some common boring proofs. > * By default, in the “Default Automatic tactic with SMT” SMT solvers are executed only after “Lasso” action. I’ve noticed that in some cases SMT solvers are capable to find a proof before “Lasso”, but unable to do it after. With “First successful” it is easy to create a workaround for this: you can run all solvers in parallel, before and after “Lasso”, and still get result within 1 second. > * One of our students added "Axiom of empty set” somewhere to the code of the SMT Solvers plug-in: it helped with automating some proofs as well. > > You can find all these changes here (branch ispras): > * https://github.com/17451k/rodin-b-sharp-smt <https://github.com/17451k/rodin-b-sharp-smt> > * https://github.com/17451k/rodincore <https://github.com/17451k/rodincore> > > Full changelog and artifacts are available here: https://github.com/17451k/rodincore/releases <https://github.com/17451k/rodincore/releases> > > Again: hope this will be useful for someone! > > Best regards, > ~ Ilya Shchepetkov > > > _______________________________________________ > Rodin-b-sharp-devel mailing list > Rod...@li... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel |
From: Ilya S. <ily...@gm...> - 2022-09-28 10:21:14
|
Hello everyone! A year ago I was working on some changes to the Rodin platform. I had two goals: to increase the number of automatically discharged proof obligations, and to try to parallelize the whole proving process in order to significantly speed it up. The work is not fully finished and currently unmaintained, since I work at a different company now, but I had some success and would like to share the results. Hope it will be of some use! First, I’ve made “Retry Auto Provers”, “Recalculate Auto Status” and “Proof Replay on Undischarged POs” actions to run in parallel, so now they are able to process several POs at once. It resulted in approximately 6 times speedup on the Intel machine with 4 CPU cores, and the proving process for some of my models now takes minutes and not hours. The main issue here: I’ve achieved this by removing some locks in the code, which likely introduced some new race conditions. This needs to be investigated and addressed, plus currently there is a bug: with large models, GUI window “Applying Auto Provers…” can disappear long before the proving is complete. Second, I’ve created a new combinator tactic called “First Successful”, which allows to run several tactics in parallel. It finishes when either one of the tactic finds the necessary proof, or when they all fail. For example, if you run “First Successful” on 6 different provers and SMT solvers with 1 second timeout for each, then at worst you will need to wait 1 second instead of 6, but at best — only a fraction of that time. Using this combinator tactic, I’ve developed a tactic profile especially for interactive proofs: “Default Interactive tactic with SMT”. Its goal is to heavily reduce the waiting time during interactive proofs: every time you choose to run auto provers, it is guaranteed to finish within 1 second. Since you usually do it multiple times per proof, the total time savings are quite significant. In practice, I found this new interactive tactic more valuable, then simple parallelization of “Retry Auto Provers”, “Recalculate Auto Status” and “Proof Replay on Undischarged POs” actions. Third, there are a few more small additions: * There are a few rewrite rules that I often use during interactive proofs, but are absent from the tactic profile editor (Event-B -> Sequent Prover -> Auto/Post Tactic -> Profiles). I’ve added them to the list of available tactics, so now they can be used to automate some common boring proofs. * By default, in the “Default Automatic tactic with SMT” SMT solvers are executed only after “Lasso” action. I’ve noticed that in some cases SMT solvers are capable to find a proof before “Lasso”, but unable to do it after. With “First successful” it is easy to create a workaround for this: you can run all solvers in parallel, before and after “Lasso”, and still get result within 1 second. * One of our students added "Axiom of empty set” somewhere to the code of the SMT Solvers plug-in: it helped with automating some proofs as well. You can find all these changes here (branch ispras): * https://github.com/17451k/rodin-b-sharp-smt * https://github.com/17451k/rodincore Full changelog and artifacts are available here: https://github.com/17451k/rodincore/releases Again: hope this will be useful for someone! Best regards, ~ Ilya Shchepetkov |
From: Guillaume V. <Gui...@ir...> - 2022-09-27 07:45:31
|
Dear Michael, Thanks for all these details. When I updated the library, I did not try to use every theory and missed all these issues with Real. To answer your previous question, there is a bug tracker for Theory plug-in bugs at https://sourceforge.net/p/rodin-b-sharp/theoriesbugs/ <https://sourceforge.net/p/rodin-b-sharp/theoriesbugs/> I fill tickets for bugs reported by mail, but I was a bit busy yesterday and did not yet fill the bugs you reported. We will see what we can do about all these bugs. If we can fix some of them quickly, we will try to release another small version to make the plug-in more usable while waiting for the big v5 release… Thanks, Guillaume |
From: Michael L. <Mic...@un...> - 2022-09-27 07:19:36
|
Hi Guillaume, another update: I deleted all axioms except for axioms axm1 to axm10 from the RealTheory and then the error disappeared. I had also previously deleted all proof rules (but the error persisted). I also renamed REAL to FLOAT in Real.tuf and Real.bpr using a text editor, to be able to use the theory. As mentioned, Rodin 3.7 will change REAL to the unicode R, it is thus currently not possible to use the standard Real Theory in a context or machine when using a standard Rodin editor (as you get type errors, the unicode R is not a valid type). Alternatively, one would have to replace all uses of REAL by unicode R in Real.tuf and Real.bpr. > On 27 Sep 2022, at 08:40, Michael Leuschel <Mic...@un...> wrote: > > > I have tried creating a fresh workspace and importing StandardTheory0.2.1.zip, > but the problems with the static checker and the ArrayIndexOutOfBoundsException persist: Greetings, Michael |
From: Michael L. <Mic...@un...> - 2022-09-27 06:40:47
|
Hi Guillaume, I actually was not able yet to use the new RealTheory in any machine or context. Is the standard theory working for somebody else using Rodin 3.7? (Side question: which issue tracker do you use for the Theory plugin?) I tried several restarts/cleans without success thus far. Here is a screenshot with the Rodin editor when trying to open a freshly created (empty) context in the project that imports the theory. In the Workspace log; there are many more entries complaining about problems “while deserializing rule of reasoner”. I have tried creating a fresh workspace and importing StandardTheory0.2.1.zip, but the problems with the static checker and the ArrayIndexOutOfBoundsException persist: The Rodin Problems view contains: Description Resource Path Location Type Error while running tool (Theory Static Checker) Real.tuf /RealTheory Unknown Rodin Build Problem Marker On the console I got this error message: !ENTRY org.rodinp.core 4 4 2022-09-27 08:34:45.346 !MESSAGE while running tool org.eventb.theory.core.theorySC on /RealTheory/Real.tuf !STACK 0 java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 2 at org.eventb.core.ast.BoundIdentifier.getDeclaration(BoundIdentifier.java:102) at org.eventb.core.ast.BoundIdentifier.typeCheck(BoundIdentifier.java:159) at org.eventb.core.ast.ExtendedPredicate.typeCheck(ExtendedPredicate.java:255) at org.eventb.core.ast.ExtendedPredicate.synthesizeType(ExtendedPredicate.java:220) at org.eventb.core.ast.Predicate.solveType(Predicate.java:58) at org.eventb.core.ast.AssociativePredicate.solveChildrenTypes(AssociativePredicate.java:210) at org.eventb.core.ast.Predicate.solveType(Predicate.java:57) at org.eventb.core.ast.BinaryPredicate.solveChildrenTypes(BinaryPredicate.java:190) at org.eventb.core.ast.Predicate.solveType(Predicate.java:57) at org.eventb.core.ast.QuantifiedPredicate.solveChildrenTypes(QuantifiedPredicate.java:303) at org.eventb.core.ast.Predicate.solveType(Predicate.java:57) at org.eventb.core.ast.Formula.typeCheck(Formula.java:1677) at org.eventb.theory.core.util.CoreUtilities.parseAndCheckPredicate(CoreUtilities.java:249) at org.eventb.theory.core.sc.modules.AxiomaticBlockAxiomsFilterModule.accept(AxiomaticBlockAxiomsFilterModule.java:45) at org.eventb.core.sc.SCProcessorModule.filterModules(SCProcessorModule.java:132) at org.eventb.theory.core.sc.modules.AxiomaticBlockAxiomsModule.fetchAxioms(AxiomaticBlockAxiomsModule.java:96) at org.eventb.theory.core.sc.modules.AxiomaticBlockAxiomsModule.process(AxiomaticBlockAxiomsModule.java:41) at org.eventb.core.sc.SCProcessorModule.processModules(SCProcessorModule.java:162) at org.eventb.theory.core.sc.modules.AxiomaticDefinitionsBlockModule.processBlocks(AxiomaticDefinitionsBlockModule.java:61) at org.eventb.theory.core.sc.modules.AxiomaticDefinitionsBlockModule.process(AxiomaticDefinitionsBlockModule.java:52) at org.eventb.core.sc.SCProcessorModule.processModules(SCProcessorModule.java:162) at org.eventb.theory.core.sc.modules.TheoryModule.process(TheoryModule.java:95) at org.eventb.core.sc.StaticChecker.runProcessorModules(StaticChecker.java:94) at org.eventb.core.sc.StaticChecker.run(StaticChecker.java:223) at org.rodinp.internal.core.builder.FileRunnable.run(FileRunnable.java:37) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2313) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2338) at org.rodinp.internal.core.BatchOperation.executeOperation(BatchOperation.java:44) at org.rodinp.internal.core.RodinDBOperation.run(RodinDBOperation.java:701) at org.rodinp.core.RodinCore.run(RodinCore.java:397) at org.rodinp.core.RodinCore.run(RodinCore.java:358) at org.rodinp.internal.core.builder.Graph.runTool(Graph.java:343) at org.rodinp.internal.core.builder.Graph.topSortStep(Graph.java:551) at org.rodinp.internal.core.builder.Graph.topSortNodes(Graph.java:530) at org.rodinp.internal.core.builder.Graph.builderBuildGraph(Graph.java:196) at org.rodinp.internal.core.builder.RodinBuilder.buildGraph(RodinBuilder.java:245) at org.rodinp.internal.core.builder.RodinBuilder.fullBuild(RodinBuilder.java:306) at org.rodinp.internal.core.builder.RodinBuilder.build(RodinBuilder.java:216) at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:853) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:232) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:281) at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:334) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:337) at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:389) at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:410) at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:160) at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:251) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63) Greetings, Michael > On 26 Sep 2022, at 19:35, Michael Leuschel <Mic...@un...> wrote: > > > > Issue 1) > From time to time I get “error while running tool” messages. > Not really sure when; multiple restarts seem to solve the problems. The error log contained this: java.lang.NullPointerException: Cannot invoke "fr.systerel.editor.internal.editors.SelectionController.getSelectedElements()" because the return value of "fr.systerel.editor.internal.editors.RodinEditor.getSelectionController()" is null at fr.systerel.editor.internal.presentation.updaters.EditorSnapshot.record(EditorSnapshot.java:55) at fr.systerel.editor.internal.presentation.updaters.EditorResynchronizer.takeSnapshot(EditorResynchronizer.java:108) at fr.systerel.editor.internal.presentation.updaters.EditorResynchronizer$SynchronizationRunnable.run(EditorResynchronizer.java:91) … And many errors of this kind: Rodin Database Exception: java.lang.IllegalStateException: Error when deserialise proof-rule metadata: org.eventb.internal.core.basis.ProofStoreReader$Bridge@30bf926a at org.eventb.internal.core.Util.newRodinDBException(Util.java:149) at org.eventb.core.basis.PRProofRule.getInput(PRProofRule.java:179) at org.eventb.core.basis.PRProofRule.getProofSkeleton(PRProofRule.java:126) at org.eventb.core.basis.EventBProofElement.getSkeleton(EventBProofElement.java:365) at org.eventb.core.basis.PRProof.getSkeleton(PRProof.java:176) at org.eventb.internal.core.pom.PSUpdater.isBroken(PSUpdater.java:228) at org.eventb.internal.core.pom.PSUpdater.updateStatus(PSUpdater.java:180) at org.eventb.internal.core.pom.PSUpdater.updatePO(PSUpdater.java:115) at org.eventb.internal.core.pom.AutoPOM.run(AutoPOM.java:87) at org.rodinp.internal.core.builder.FileRunnable.run(FileRunnable.java:37) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2313) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2338) at org.rodinp.internal.core.BatchOperation.executeOperation(BatchOperation.java:44) at org.rodinp.internal.core.RodinDBOperation.run(RodinDBOperation.java:701) at org.rodinp.core.RodinCore.run(RodinCore.java:397) at org.rodinp.core.RodinCore.run(RodinCore.java:358) at org.rodinp.internal.core.builder.Graph.runTool(Graph.java:343) at org.rodinp.internal.core.builder.Graph.topSortStep(Graph.java:551) at org.rodinp.internal.core.builder.Graph.topSortNodes(Graph.java:530) at org.rodinp.internal.core.builder.Graph.builderBuildGraph(Graph.java:196) at org.rodinp.internal.core.builder.RodinBuilder.buildGraph(RodinBuilder.java:245) at org.rodinp.internal.core.builder.RodinBuilder.fullBuild(RodinBuilder.java:306) at org.rodinp.internal.core.builder.RodinBuilder.build(RodinBuilder.java:216) at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:853) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:232) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:281) at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:334) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:337) at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:389) at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:410) at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:160) at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:251) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63) Caused by: java.lang.IllegalStateException: Error when deserialise proof-rule metadata: org.eventb.internal.core.basis.ProofStoreReader$Bridge@30bf926a at org.eventb.theory.internal.rbp.reasoners.input.PRMetadataReasonerInput.<init>(PRMetadataReasonerInput.java:53) at org.eventb.theory.internal.rbp.reasoners.input.RewriteInput.<init>(RewriteInput.java:66) at org.eventb.theory.rbp.reasoners.ManualRewriteReasoner.deserializeInput(ManualRewriteReasoner.java:293) at org.eventb.theory.rbp.reasoners.ManualRewriteReasoner.deserializeInput(ManualRewriteReasoner.java:288) at org.eventb.core.basis.PRProofRule.getInput(PRProofRule.java:159) ... 33 more Caused by: java.lang.IllegalStateException: Error when deserialise proof-rule metadata: org.eventb.internal.core.basis.ProofStoreReader$Bridge@30bf926a at org.eventb.theory.internal.rbp.reasoners.input.PRMetadataReasonerInput.<init>(PRMetadataReasonerInput.java:53) at org.eventb.theory.internal.rbp.reasoners.input.RewriteInput.<init>(RewriteInput.java:66) at org.eventb.theory.rbp.reasoners.ManualRewriteReasoner.deserializeInput(ManualRewriteReasoner.java:293) at org.eventb.theory.rbp.reasoners.ManualRewriteReasoner.deserializeInput(ManualRewriteReasoner.java:288) at org.eventb.core.basis.PRProofRule.getInput(PRProofRule.java:159) at org.eventb.core.basis.PRProofRule.getProofSkeleton(PRProofRule.java:126) at org.eventb.core.basis.EventBProofElement.getSkeleton(EventBProofElement.java:365) at org.eventb.core.basis.PRProof.getSkeleton(PRProof.java:176) at org.eventb.internal.core.pom.PSUpdater.isBroken(PSUpdater.java:228) at org.eventb.internal.core.pom.PSUpdater.updateStatus(PSUpdater.java:180) at org.eventb.internal.core.pom.PSUpdater.updatePO(PSUpdater.java:115) at org.eventb.internal.core.pom.AutoPOM.run(AutoPOM.java:87) at org.rodinp.internal.core.builder.FileRunnable.run(FileRunnable.java:37) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2313) at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2338) at org.rodinp.internal.core.BatchOperation.executeOperation(BatchOperation.java:44) at org.rodinp.internal.core.RodinDBOperation.run(RodinDBOperation.java:701) at org.rodinp.core.RodinCore.run(RodinCore.java:397) at org.rodinp.core.RodinCore.run(RodinCore.java:358) at org.rodinp.internal.core.builder.Graph.runTool(Graph.java:343) at org.rodinp.internal.core.builder.Graph.topSortStep(Graph.java:551) at org.rodinp.internal.core.builder.Graph.topSortNodes(Graph.java:530) at org.rodinp.internal.core.builder.Graph.builderBuildGraph(Graph.java:196) at org.rodinp.internal.core.builder.RodinBuilder.buildGraph(RodinBuilder.java:245) at org.rodinp.internal.core.builder.RodinBuilder.fullBuild(RodinBuilder.java:306) at org.rodinp.internal.core.builder.RodinBuilder.build(RodinBuilder.java:216) at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:853) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:232) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:281) at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:334) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:337) at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:389) at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:410) at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:160) at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:251) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63) |