|
|
| Line 12: |
Line 12: |
| | * Evaluations, benchmarkings, case studies, etc. | | * Evaluations, benchmarkings, case studies, etc. |
| | | | |
| − | The IVOIRE workshop was co-located with [https://ifm22.si.usi.ch/ iFM 2022] in Lugano, Switzerland, | + | The IVOIRE workshop will be co-located with [https://abz2023.loria.fr/] in Nancy, France,and will take place on 30th of May 2023. |
| − | took place on 7 June 2022 (the day before the main conference).
| |
| − | The workshop has taken place physically, like the conference itself.
| |
| | | | |
| | | | |
| Line 22: |
Line 20: |
| | | | |
| | | | |
| − | | + | To be announced. |
| − | * '''09:00–09:10''' Welcome note
| |
| − | * '''09:10–10:30''' The IVOIRE project (Session Chair: Michael Leuschel)
| |
| − | ** '''09:10–09:30''' [[Media:Atif Mashkoor - Validation obligations.pptx|Validation obligations]] (Atif Mashkoor, JKU Linz, Austria)
| |
| − | ** '''09:30–09:50''' [[Media:Fabian Vu - Formalization of VOs.pdf|Formalization of VOs]] (Fabian Vu, HHU, Düsseldorf, Germany)
| |
| − | ** '''09:50–10:10''' [[Media:Advanced_semantics_for_VOs.pdf | Abstraction and Refinement of VOs]] (Sebastian Stock, JKU Linz, Austria)
| |
| − | ** '''10:10–10:30''' IVOIRE Demo: VO Manager in ProB2-UI (David Geleßus, HHU Düsseldorf, Germany)
| |
| − | * '''10:30–11:00''' ''Coffee break''
| |
| − | * '''11:00–13:00''' B/Event-B's perspective on validation (Session Chair: Atif Mashkoor)
| |
| − | ** '''11:00–11:30''' [[Media:Jean-Pierre Jacquot - Validation An Event-B perspective with JeB.pdf|Validation: An Event-B perspective with JeB]] (Jean-Pierre Jacquot, University of Lorraine, France)
| |
| − | ** '''11:30–12:00''' [[Media:Richard Banach - Graded Refinement, Retrenchment and Simulation, for Challenging Requirements.pdf|Graded Refinement, Retrenchment and Simulation, for Challenging Requirements]] (Richard Banach, University of Manchester, UK)
| |
| − | ** '''12:00–12:30''' [[Media:Colin Snook - Behavior Driven Formal Modelling.pdf|Behavior Driven Formal Modelling]] (Colin Snook, University of Southampton, UK)
| |
| − | ** '''12:30–13:00''' [[Media:Dominique Méry - Refinement-based Construction of Correct IoT Protocols.pdf|Refinement-based Construction of Correct IoT Protocols]] (Dominique Méry, University of Lorraine, France)
| |
| − | * '''13:00–14:30''' ''Lunch break''
| |
| − | * '''14:30–16:00''' ASM's perspective on validation (Session Chair: Alexander Egyed)
| |
| − | ** '''14:30–15:00''' [[Media:Egon Börger - The ASM Method Integrates Validation and Verification at Different Abstraction Levels.pdf|The ASM Method Integrates Validation and Verification at Different Abstraction Levels]] (Egon Börger, University of Pisa, Italy)
| |
| − | ** '''15:00–15:30''' [[Media:Angelo Gargantini - On the importance of scenario-based validation.pptx|On the importance of scenario-based validation]] (Angelo Gargantini, University of Bergamo, Italy)
| |
| − | ** '''15:30–16:00''' [[Media:Elvinia Riccobene - Exploiting the advantage of formal executable models@RUNTIME.pdf|Exploiting the advantage of formal executable models@RUNTIME]] (Elvinia Riccobene, University of Milan, Italy)
| |
| − | * '''16:00–16:30''' ''Coffee break''
| |
| − | * '''16:30–17:00''' Industrial perspective on validation (Session Chair: Michael Leuschel)
| |
| − | ** '''16:30–17:00''' [[Media:Alexander Egyed - DesignSpace for collaborative engineering.pdf|DesignSpace for collaborative engineering]] (Alexander Egyed, JKU Linz, Austria)
| |
| − | ** [[Media:Thierry Lecomte - Methodology for formal proof of spec.pdf|Methodology for formal proof of specification]] (Thierry Lecomte, CLEARSY, France)
| |
| − | * '''17:00–17:30''' Discussion and concluding remarks
| |
| − | * '''19:30''' ''Workshop dinner''
| |
| | | | |
| | == Registration == | | == Registration == |
| | | | |
| − | Registration for the workshop will be handled by iFM.
| + | to be announced. |
| − | See [https://ifm22.si.usi.ch/pages/registration/#other-events-7-june-2022 their registration page] for details.
| |
| | | | |
| | == Organizers == | | == Organizers == |
Historically, formal methods and supported environments have focused more on only one-half of the quality-assurance process: verification (are we building the software right?).
The other half, validation (are we building the right software?) has been given much less attention,
i.e., we have fewer automated/push-button tools available for validation, unlike verification.
The IVOIRE project focuses on developing an enhanced formal paradigm based on an extension of the refinement framework that includes a comprehensive validation process and toolchain to perform validation obligations.
The main goal of this workshop was to provide a platform for formal methods practitioners, researchers, and academics to discuss various issues associated with validation for formal methods,
including but not limited to:
- Validation obligations or other systematic approaches to validation
- Relation between refinement and validation, and the interplay between verification and validation
- Environments and tools to manage the validation process
- Evaluations, benchmarkings, case studies, etc.
The IVOIRE workshop will be co-located with [1] in Nancy, France,and will take place on 30th of May 2023.
Schedule
To be announced.
Registration
to be announced.
Organizers
Workshop chairs:
- Atif Mashkoor (JKU Linz, Austria)
- Michael Leuschel (HHU Düsseldorf, Germany)
Workshop organizing committee:
- Sebastian Stock (JKU Linz, Austria)
- Fabian Vu (HHU Düsseldorf, Germany)
- David Geleßus (HHU Düsseldorf, Germany)
