F-IDE 2018

4th Workshop on Formal Integrated Development Environment

A satellite workshop of FLoC/FM2018

July 14, 2018 - Oxford, UK

Venue

Registration: Mathematical Institute (also called the “Andrew Wiles Building”), Woodstock Road, OX2 6GG
Workshop venue: Seminar Room 1, Blavatnik School of Government, Radcliffe Observatory Quarter, Woodstock Road, Oxford, OX2 6GG

News

Post proceedings are now available at https://arxiv.org/html/1811.09014

Aims

High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process.

Topics

The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It welcomes the presentation of tools, methods, techniques and experiments. Topics of interest include, but are not limited to, the following:

F-IDE building: design and integration of languages, development of user-friendly front-ends
How to make high-level logical and programming concepts palatable to industrial developers
Integration of Object-Oriented and modularity features
Integration of static analyzers
Integration of automatic proof tools, theorem provers and testing tools
Documentation tools
Impact of tools on certification
Experience reports on developing F-IDEs
Experience reports on using F-IDEs
Experience reports on formal methods-based assessments in industrial applications

Invited speakers

Jean-Christophe Filliâtre: Auto-active verification using Why3's IDE. Why3 is a platform for deductive program verification. It features a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a dedicated IDE where users edit source files and build proofs interactively using a blend of logical transformations and calls to external theorem provers. In this talk, I will illustrate the typical workflow of program verification using Why3's IDE, focusing on the key features of WhyML, auto-active verification, and proof maintenance.
Leo Freitas: VDM at large: Analysing the EMV Next Generation Kernel. The EMV consortium protocols facilitate worldwide interoperability of secure electronic payments. Relevant attacks still plague the industry, with financial fraud on payment systems rising. Despite recent advances, it has proved difficult for academia to provide a suitable solution within industry’s constraints. In this paper, we describe a methodology being adopted by EMVCo for its EMV2 to be released in 2019. It stems from our earlier work on EMV1. It involves domain specific languages and verification tools targeting different analysis of interest; in this paper, we emphasise the part VDM played.

Program

Session 1: Program Verification (9:00-10:30)

09:00-10:00 (*) Keynote 1: Auto-active verification using Why3's IDE (Jean-Christophe Filliâtre)
10:00-10:30 Lightweight Interactive Proving inside an Automatic Program Verifier (Sylvain Dailler, Claude Marché and Yannick Moy)

(Coffee Break)

Session 2: User interfaces for formal tools (11:00-12:30)

11:00-11:30 User Support for the Combinator Logic Synthesizer Framework (Jan Bessai and Anna Vasileva)
11:30-12:00 AsmetaF: a flattener for the ASMETA framework (Paolo Arcaini, Riccardo Melioli and Elvinia Riccobene)
12:00-12:30 Improving the Visualization of Alloy Instances (Rui Couto, José Creissac Campos, Nuno Macedo and Alcino Cunha)

(Lunch)

Session 3: Experience in analyzing large programs (14:00-15:30)

14:00-15:00 (*) Keynote 2: VDM at large: analysing the EMV Next Generation Kernel (Leo Freitas)
15:00-15:30 Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (Alexander Knüppel, Thomas Thüm, Carsten Pardylla and Ina Schaefer)

(Coffee Break)

Session 4: Integrating formal verification results (16:00-18:00)

16:00-16:30 Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents (Makarius Wenzel)
16:30-17:00 A Notebook Format for the Holistic Design of Embedded Systems (Spencer Park and Emil Sekerinski)
17:00-17:30 The CLEAR Way To Transparent Formal Methods (Devesh Bhatt, Anitha Murugesan, Brendan Hall, Hao Ren and Yogananda Jeppu)
17:30-18:00 Integrating user design and formal models within PVSio-Web (Nathaniel Watson, Steve Reeves and Paolo Masci)

-------------------

Note: Sessions marked with (*) are shared with the Overture workshop.

Instructions for Pre- and Post-Proceedings

The camera ready version of accepted papers can be submitted through Easychair: https://easychair.org/conferences/?conf=fide18

Authors should use the EPTCS format:

Papers accepted as Full papers: up-to 20 pages (EPTCS format), including references and appendices
Papers accepted as Short papers: up-to 10 pages (EPTCS format), including references and appendices

Deadline for submitting the camera ready version: May 25th

Preliminary proceedings, including all papers selected for the workshop, will be available electronically at the workshop. Post-proceedings will be published with Electronic Proceedings in Theoretical Computer Science (EPTCS)

Important dates

~~Abstract submission: April 23, 2018~~
~~Paper submission: April 30, 2018~~
~~Notification: May 15, 2018~~
~~Camera-ready version: May 25, 2018~~
Workshop date: July 14, 2018

PC Co-Chairs

Paolo Masci, HASLab/INESC-TEC and Universidade do Minho, paolo (dot) masci (at) inesctec (dot) pt
Rosemary Monahan, Maynooth University, rosemary (dot) monahan (at) nuim (dot) ie
Virgile Prevosto, Institut List, CEA, Université Paris-Saclay, virgile (dot) prevosto (at) cea (dot) fr

Steering Committee

Catherine Dubois, Samovar / ENSIIE, catherine (dot) dubois (at) ensiie (dot) fr
Dominique Méry, LORIA / Université de Lorraine, dominique (dot) mery (at) loria (dot) fr

Program Committee

Bernhard Beckert (Karlsruhe Institute of Technology)
Cinzia Bernardeschi (University of Pisa)
José Creissac Campos (University of Minho)
Claudio Sacerdoti Coen (University of Bologna)
Paul Curzon (Queen Mary University of London)
Damien Doligez (INRIA)
Andrea Domenici (University of Pisa)
Michalis Famelis (University of Montreal)
Carlo A. Furia (Chalmers University of Technology)
Andrew Gacek (Rockwell Collins, Inc.)
Kenneth Lausdahl (Aarhus University)
Stephan Merz (Inria Nancy)
Stefan Mitsch (Carnegie Mellon University)
César Muñoz (NASA Langley)
Andrei Paskevich (Université Paris-Sud, LRI)
François Pessaux (ENSTA ParisTech)
Marie-Laure Potet (Laboratoire Vérimag)
James Power (Maynooth University)
Steve Reeves (University of Waikato)
Bernhard Rumpe (RWTH Aachen University)
Enrico Tassi (INRIA)
Laurent Voisin (Systerel)
Makarius Wenzel (sketis.net)
Yi Zhang (U.S. Food and Drug Administration)

Previous Editions

F-IDE 2016 (co-located with FM2016 Limassol, Cyprus)
F-IDE 2015 (co-located with FM2015, Oslo, Norway)
F-IDE 2014 (co-located with ETAPS 2014, Grenoble, France)

Google Sites

Report abuse