THE 22ND OVERTURE WORKSHOP

The 22nd Overture Workshop will be held on the 10th September 2024 co-located with FM 2024, hosted by Politecnico di Milano.

Location: Room 3.1.12, Edifico 3, Politechnico Milano, Milan Italy

Online: Webex*

* For online participation, please register here: https://www.fm24.polimi.it/?page_id=559. A discount code is available to reduce the price to ~€50. Please request from kenneth.pierce@ncl.ac.uk.

Programme

Note: Overture proper starts at 11:00 CEST

09:00-10:20 Session 7D: Plenary keynote, invited by LOPSTR/PPDP. Safe and Easy Compile-Time Generative Programming (Ningning Xie) ABSTRACT. Program generation is a powerful and expressive approach to eliminating abstraction overhead and improving program performance, which has been studied and implemented in a variety of languages with different forms. In this talk we overview MacoCaml, a new design and implementation of compile-time computation for OCaml. MacoCaml features a unifying and novel combination of phase separation and quotation-based staging. We review MacoCaml’s recent developments, including a comprehensive formalism of a feature- rich macro calculus with key meta-theoretic properties, and an extension to module functors that leads to explicit phase distinction. We describe how the meta-theoretical results offer practical benefits for programmers, and conclude the talk with a few directions for future exploration.

10:30-11:00 Coffee

11:00-11:10 Welcome to the Overture Workshop

11:10-11:40 vdmweb: a web-based VDM animation tool [paper; slides] (Harry Hughes and Leo Freitas)

11:40-12:10 QuickCheck for VDM [paper; slides] (Nick Battle and Markus Ellyton)

12:10-12:40 vdm2dafny: An Automated Translation Tool for VDMSL [paper; slides] (Adam Winstanley and Leo Freitas)

12:40-14:00 Lunch

14:00-14:30 Specification Slicing for VDM-SL [paper; slides] (Tomohiro Oda and Han-Myung Chang))

14:30-15:00 Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols [paper; slides] (Nisansala Yatapanage and Cliff Jones)

15:00-15:30 Cilium and VDM - Towards Formal Analysis of Cilium Policies [paper; slides] (Tomas Kulik and Jalil Boudjadar)

15:30-16:00 Coffee

16:00-17:00 Community Discussion

• Proposal for asynchronous collaboration for Core and Language Board
• AOB
• Closing

CALL FOR PAPERS

The 22nd Overture Workshop is the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the best established formal methods for systems development. A lively community of researchers and practitioners in academia and industry has grown around the modelling languages (VDM-SL, VDM++, VDM-RT) and tools (including VDMTools, Overture, INTO-CPS, ViennaTalk, VDMJ and VDM VSCode). Together, these provide a platform for work on modelling and analysis technology that includes IDEs, static and dynamic analysis, test generation, execution support, and model checking.

Previous workshops have been invaluable in encouraging both new and established members of the community in their work, and helping to determine priorities and future directions. Proceedings of former workshops are available at https://www.overturetool.org/.

Important Dates

15th July 2024 29th July 2024: Submission of papers

19th August 2024 26th August 2024: Notification to authors

2nd September 2024 9th September 2024: Final version of papers due

10th September 2024: Workshop

Call

Our workshop provides a forum for discussing and advancing the state of the art in formal modelling and analysis using VDM and its family of associated formalisms including extensions for distributed VDM and real-time systems. We strongly welcome contributions on the development of tools for, as well as developments in, foundations and reports of practical experience. Each paper will be peer-reviewed by at least three members of the PC, must use the Springer LNCS format, and should not exceed 15 pages in length.

The scope of the workshop includes, but is not restricted to:

• Reports of applications of VDM technology, especially reports of industrial use.
• Papers describing requirements, designs, implementations and case studies of support tools for VDM, whether or not implemented in the VDM-related tools.
• Papers on the foundations and methodology associated with VDM and its extensions, including the description of real-time, cyber-physical systems, digital twins and systems-of-systems.
• Papers combining VDM with other notations and tools.
• Position papers on VDM and its promotion in industry practice.
• Papers on extensions of VDM-related tools including Overture, INTO-CPS and ViennaTalk.

Submission

https://easychair.org/conferences/?conf=ovt22

Organising

• Ken Pierce, Newcastle University, United Kingdom (ken.pierce@newcastle.ac.uk)
• Hugo Daniel Macedo, Aarhus University, Denmark (hdm@ece.au.dk)
• Leo Freitas, Newcastle University, United Kingdom(leo.freitas@newcastle.ac.uk)

(Draft) Program Committee

TBA

Contact

All questions about submissions should be emailed to (kenneth.pierce@newcastle.ac.uk)

Sponsor

TBA