F-IDE 2015

2nd Workshop on Formal-IDE

A satellite workshop of FM2015

General theme: "Formal Integrated Development Environment (F-IDE) for joint construction of an application and its correctness proof upon its formalized specification".

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 in order 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 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 an 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 first F-IDE workshop has been organized by Catherine Dubois, Dimitra Giannakopoulou and Dominique Mery as a satellite event of ETAPS 2014 in April 2014 in Grenoble, France. The workshop featured 8 presentations and an invited talk given by Carlo Furia and Julian Tschannen from ETH Zurich. Post-proceedings have been edited as EPTCS proceedings, as EPTCS 149. The workshop was attended by ~20 participants.
Topics

The workshop is opened to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It should allow 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, compilation
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 of developing F-IDE
Experience reports of using F-IDE
Experience reports of formal methods-based assessments of industrial applications