Published: 27th November 2018|
|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|
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:
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.
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.