This volume contains the papers presented at F-IDE-18: Formal Integrated Development Environment held on July 14, 2018 in Oxford, as a satellite workshop of the FLoC/FM2018 conference.
The workshop aims to promote the design and evaluation of formal methods development environments (F-IDEs) for assessing safety, security and privacy aspects of high-confidence software systems. 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 F-IDEs are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process.
We solicited several kinds of contributions: research papers providing new concepts and results, position papers and research perspectives, experience reports, tool presentations. This year's edition is a one-day event with 11 communications (9 peer-reviewed papers, and 2 keynote talks), offering a large variety of approaches, techniques and tools. Each submission was evaluated by at least three reviewers.
This year's program is enriched by joint sessions with the Overture workshop, and includes two brilliant keynote speakers:
- Jean-Christophe Filliâtre, senior researcher at CNRS, France, lead developer of the program verification tool Why3. His keynote speech is entitled ``Auto-active verification using Why3's IDE''
- Leo Freitas, lecturer a Newcastle University, UK. His keynote speech is entitled ``VDM at large: Modelling the EMVCo 2nd Generation Kernel'
We would like to thank the Steering Committee members, Catherine Dubois (Samovar / ENSIIE) and Dominique Méry (LORIA / Universite de Lorraine), which facilitated the realization of another successful edition of the F-IDE workshop.
Special thanks go to our PC members for doing an excellent job in writing high-quality reviews in a timely manner, all authors who submitted their work to F-IDE-18, and the FLoC event organizers, who have accepted to host our workshop. The logistics of our job as Program Chairs were facilitated by the EasyChair system. We thank the editors of Electronic Proceedings in Theoretical Computer Science who accepted to publish post-proceedings of the F-IDE-18 papers.
Rosemary Monahan
Virgile Prevosto