Published: 27th November 2018
DOI: 10.4204/EPTCS.284
ISSN: 2075-2180

EPTCS 284

Proceedings 4th Workshop on
Formal Integrated Development Environment
Oxford, England, 14 July 2018

Edited by: Paolo Masci, Rosemary Monahan and Virgile Prevosto

Preface
Paolo Masci, Rosemary Monahan and Virgile Prevosto
Keynote Speakers
Jean-Christophe Filliâtre and Leo Freitas
Lightweight Interactive Proving inside an Automatic Program Verifier
Sylvain Dailler, Claude Marché and Yannick Moy
1
User Support for the Combinator Logic Synthesizer Framework
Jan Bessai and Anna Vasileva
16
AsmetaF: A Flattener for the ASMETA Framework
Paolo Arcaini, Riccardo Melioli and Elvinia Riccobene
26
Improving the Visualization of Alloy Instances
Rui Couto, José C. Campos, Nuno Macedo and Alcino Cunha
37
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Alexander Knüppel, Thomas Thüm, Carsten Pardylla and Ina Schaefer
53
Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents
Makarius Wenzel
71
A Notebook Format for the Holistic Design of Embedded Systems (Tool Paper)
Spencer Park and Emil Sekerinski
85
Integrating User Design and Formal Models within PVSio-Web
Nathaniel Watson, Steve Reeves and Paolo Masci
95

Preface

F-IDE 2018 is the fourth Formal Integrated Development Environment workshop (F-IDE 2018) held in Oxford, England, on July 14, 2018 as a satellite workshop of FLoC 2018.

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 in order to ease the justification of design choices and the review of code and proofs. A 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 one 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 one is to offer automated management of application documentation. It may also be expected that developments done with such a F-IDE are reusable and modular. Moreover, tools for testing and static analysis may be embedded in this F-IDE, to help address most steps of the assessment process. The workshop is a forum of exchange on different features related to F-IDEs.

We solicited several kinds of contributions: research papers providing new concepts and results, position papers and research perspectives, experience reports, tool presentations. The workshop was open to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. The current edition is a one-day workshop with nine communications, offering a large variety of approaches, techniques and tools. Some of the presentations took the form of a tool demonstration. Each submission was reviewed by three reviewers.

We had the honor of welcoming two keynote speakers: Jean-Christophe Filliâtre from CNRS who gave a keynote entitled Auto-active verification using Why3's IDE, and Leo Freitas from Newcastle University who gave a keynote entitled VDM at large: Analysing the EMV Next Generation Kernel.

The committees of F-IDE 2018 were composed of:

Steering Committee: PC Co-chairs: Program Committee:

We would like to thank the PC members for doing such a great job in writing high-quality reviews and participating in the electronic PC discussion. We would like to thank all authors who submitted their work to F-IDE 2018. We are grateful to the FLoC Organisation Committee, who hosted our workshop. The logistics of our job as Program Chairs were facilitated by the EasyChair system and we thank the editors of Electronic Proceedings in Theoretical Computer Science who accepted the papers for publication.


Keynote Speakers

Speaker: Jean-Christophe Filliâtre, CNRS, France

Title: 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 illustrate the typical workflow of program verification using Why3's IDE, focusing on the key features of WhyML, auto-active verification, and proof maintenance.

Speaker: Leo Freitas, Newcastle University, UK

Title: 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 talk, 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 presentation, we emphasise the part VDM played.