|
Published: 26th April 2014 DOI: 10.4204/EPTCS.149 ISSN: 2075-2180 |
| Preface | |
| The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel Carlo A. Furia, Julian Tschannen and Bertrand Meyer | 1 |
| The Dafny Integrated Development Environment K. Rustan M. Leino and Valentin Wüstholz | 3 |
| Who watches the watchers: Validating the ProB Validation Tool Jens Bendisposto, Sebastian Krings and Michael Leuschel | 16 |
| Teaching Formal Methods and Discrete Mathematics Mathieu Jaume and Théo Laurent | 30 |
| SPEEDY: An Eclipse-based IDE for invariant inference David R. Cok and Scott C. Johnson | 44 |
| Experience in using a typed functional language for the development of a security application Damien Doligez, Christèle Faure, Thérèse Hardin and Manuel Maarek | 58 |
| FoCaLiZe: Inside an F-IDE François Pessaux | 64 |
| OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse David R. Cok | 79 |
| Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB John Witulski and Michael Leuschel | 93 |
The workshop F-IDE is the first one on those topics and welcomed submissions in the following areas, among others:
In this volume, a communication is presenting OpenJML; it is a tool for software verification of Java programs in the contract-based approach and demonstrates the value of integrating specification and verification tools directly in the software development IDE and in automating as many tasks as possible. Two other communications describe Integrated Development Environments like for Dafny or as SPEEDY and show how these tools are useful in practical cases. Several communications concern FoCaliZe and illustrate the reply of this environment for meaning what is a formal IDE. Another communication reports on the use of a typed functional language for developing a secure application. Finally, two communications focus on the validations efforts for the validation tool ProB, in a quest of certification, e.g. in the context of the EN50128 norm and safety critical applications in the railway domain.
The program committee of F-IDE 2014 was composed of:
Bernhard Beckert, Karlsruhe Institute of Technology, Germany
Loïc Correnson, CEA, France
Catherine Dubois, ENSIIE, France
Dimitra Giannakopoulou, NASA, USA
Thérèse Hardin, University Pierre and Marie Curie, France
Peter Lammich, Technische Universität München, Germany
Rustan Leino, Microsoft Research, USA
Michael Leuschel, University of Düsseldorf, Germany
Claude Marché, INRIA, France
Dominique Méry, University of Nancy, France
Suzette Person, NASA, USA
François Pessaux, ENSTA ParisTech, France
Marie-Laure Potet, ENSIMAG, France
Mike Whalem, University of Minnesota Software Engineering Center, USA
We thank the program committee members who studied very carefully the submitted papers and helped with their valuable comments to prepare this workshop. We thank Thérèse Hardin who contributed to the initiation of the event and François Pessaux who designed and maintained the F-IDE website. We are very grateful to the ETAPS organizers for taking care of all the local organization.
We use the construction of the Gotthard tunnel – connecting the German- and Italian-speaking parts of Switzerland through the Gotthard massif – as a metaphor for the two-pronged design of the Eiffel Verification Environment (EVE). No prior knowledge of Swiss geography is required to enjoy the presentation.
Like a tunnel that connects people speaking two different languages, EVE tries to cater to two different kinds of users. At one end are the Joes Six-Pack of verification: run-of-the-mill programmers with little or no background in formal methods, who are used to standard integrated development environments but cannot be expected to write or understand complex formal specifications. At the other end are highly-trained experts, fluent in formal techniques, to whom writing and reasoning about rigorous specifications is second nature. The design of EVE accommodates features useful at both ends.
For programmers unacquainted with verification, EVE supports lightweight techniques which work with the simple contracts that most Eiffel programmers can write [2]:
For full-fledged verification experts, EVE integrates AutoProof [10], an auto-active [3] advanced program verifier which supports a large part of the Eiffel language. AutoProof's input language also features support for annotations availing of mathematical models and other specification idioms such as quantifiers and ghost code. AutoProof's logic is based on a flexible “semantic” methodology [8] to specify and reason about invariants of both hierarchical and collaborative object structures; this enables the full verification of complex design patterns, such as Observers and Composites [9], with reasonable annotation burden. The AutoInfer framework [12] is another component of EVE geared to strong specifications: it automatically infers postconditions of routines, often achieving high percentages of correctness and completeness.
The introduction of new features and the improvement of existing ones continues at both ends of the formality spectrum. Integration also progresses through EVE's architecture, which allows the various tools to run in parallel, collects their results, and displays them within a simple uniform interface that indicates, for each element such as routine or class, how much its verification has progressed, and what actions could be undertaken to improve the quality of the program under development.
The ultimate goal of EVE's ongoing double-ended development is meeting in the middle: once the tunnel is completed, it will provide a way to smoothly transition into formal techniques from everyday's programming practices.