Preface

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. 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 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 current edition is a one-day workshop with eight 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 to welcome Professor Kim G. Larsen from Aalborg University. He gave a keynote entitled Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems.

The program committee of F-IDE 2015 was composed of:
Bernhard Becket, Karlsruhe Institute of Technology
Jens Bendisposto, University of Düsseldorf
José C. Campos, HASLab/INESC-TEC and Universidade do Minho
Paul Curzon, Queen Mary University of London
Michalis Famelis, University of British Columbia
Camille Fayollas, IRIT/LAAS
Carlo A. Furia, Chalmers University of Technology
Andrew Gacek, Rockwell Collins, Inc.
Temesghen Kashai, NASA Ames/CMU
Kenneth Lausdahl, Aarhus University
Rustan Leino, Microsoft Research
Stefan Mitsch, Carnegie Mellon University
Patrick Oladimeji, Swansea University
Andrei Paskevich, Université Paris-Sud/LRI
François Pessaux, ENSTA ParisTech
Marie-Laure Potet, Laboratoire Verimag
Virgile Prevosto, CEA Tech List
Steve Reeves, Waikato University
Bernhard Rumpe, RWTH Aachen University
Carlo Sacerdoti Coen, University of Bologna
Enrico Tassi, INRIA
Laurent Voisin, Systerel
Makarius Wenzel, sketis.net
Yi Zhang, CDRH/FDA
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 2016. We are grateful to the FM Organisation Committee, which has accepted to host 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 to publish the papers.

Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems

Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. In this talk we will survey how the various components of the UPPAAL tool-suite over a 20 year period have been developed to support various analysis of these formalisms.
This includes the classical usage of UPPAAL as an efficient model checker of hard real time constraints of timed automata models, but also the branch UPPAAL CORA which has been extensively used to find optimal solutions to time-constrained scheduling problems. More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies - and subsequent executable control programs - for safety and reachability objectives. More recently the branch UPPAAL SMC offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata, and the branch UPPAAL STRATEGO supports synthesis (using machine learning) of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and highlight their concerted applications to a selection of real-time and cyber-physical examples.

The Tinker GUI for Graphical Proof Strategies (tool demo)

1 Background

Composition in most tacticals either relies on the number and the order of sub-goals, or tries all tactics on all sub-goals. The former is brittle as the number and the order could be changed if any of the sub-tactics changes; and the latter is hard to debug and maintain, as if a proof fails the actual position is hard to find. It is also difficult for others to see the intuition behind tactic design.

2 PSGraph

A PSGraph can have the following types of nodes:

• Atomic tactics. An atomic tactic wraps a tactic of the underlying theorem prover. The default behaviour is to threat the label of the node as a tactic name and apply it as a function (tactic). For example, if a node is labelled by strip_∧ then this name will be parsed and executed as a tactic in the underlying theorem prover, and fail if no such tactic exists.
• Hierarchical nodes. Modularity is achieved by hierarchies. This can also help to reduce the complexity and size of a PSGraph by hiding parts of it. We will illustrate the new hierarchy features below.
• Identity nodes. Identity nodes are used to fanout and join wires. As the name suggests, they do not change the sub-goals.
• Breakpoints. A novel feature of Tinker is the introduction of breakpoint nodes, which can be added/removed from wires by a simple mouse click.
• Goal nodes. A goal node wraps a sub-goal of a proof, and this can not be modified by the user, i.e. these nodes can only be changed through tactic applications, and introduced by the CORE when a new proof is started.

To illustrate, consider the PSGraph in Figure 1. This example is taken from [7]. It is an encoding of a simple tactic from ProofPower to eliminate quantifiers. The overall strategy (i.e. the top-level graph on the right) contains an atomic tactic that repeatedly strips conjunctions (strip_∧), and two hierarchical nodes: one deals with existentially quantifier variables (simp_ex); the other deals with universal quantifiers (simp_forall). The goal types are used to send the goals to the correct node, and to decide when to terminate the loop.

3 The Tinker Tool

A PSGraph in Tinker can be applied as a normal tactic/method within the (Isabelle, ProofPower or Rodin) proof IDE. This is the normal execution. However, if it fails, it can instead be run in an `interactive mode' where the Tinker GUI is used to visualise and guide how the proof proceeds and identify where it failed. Figure 2 shows this GUI.

A user can draw a PSGraph from the Graph panel by selecting the type of node from the Drawing and evaluation controls panel. Nodes are connected by dragging a line between them. When selecting an entity, the details are displayed in the Information panel, and they can be edited by double clicking. The Drawing and evaluations controls panel gives users a lot of flexibility when developing and applying proof strategies, including:

1. select which goal to apply;
2. choose between stepping into and stepping over the evaluation of hierarchical nodes;
3. apply and complete the current hierarchical tactic;
4. apply and finish the whole proof strategy;
5. insert a breakpoint and evaluate a graph automatically until the break point is reached by a goal.

4 Summary

In the future, we would like to improve static checking of PSGraph; for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi-)automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.

References

1. D. Delahaye (2002): A Proof Dedicated Meta-Language. Electronic Notes in Theoretical Computer Science 70(2), pp. 96-109. doi:10.1016/S1571-0661(04)80508-5.
2. G. Grov, A. Kissinger & Y. Lin (2013): A Graphical Language for Proof Strategies. In: LPAR 2013, Springer, pp. 324-339. doi:10.1007/978-3-642-45221-5_23
3. G. Grov, A. Kissinger & Y. Lin (2014): Tinker, tailor, solver, proof. In: UITP 2014, ENTCS 167, Open Publishing Association, pp. 23-34. doi:10.4204/EPTCS.167.5.
4. Y. Liang, Y. Lin & G. Grov (2016): 'The Tinker' for Rodin. In: ABZ 2016, Springer, pp. 262-268, doi: 978-3-319-33600-8_19
5. T Libal, M. Riener & M Rukhaia (2014): Advanced Proof Viewing in ProofTool. In: UITP 2014, EPTCS 167, Open Publishing Association, pp. 35-47. doi: 10.4204/EPTCS.167.6.
6. Y. Lin, G. Grove, C. O'Halloran & P. G. (2016): A Super Industrial Application of PSGraph. In: ABZ 2016, Volume 9675 of LNCS, pp. 319-325, Springer. doi: 10.1007/978-3-319-33600-8_28.
7. Y. Lin, P. Le Bras & G. Grov (2016): Developing and Debugging Proof Strategies by Tinkering. In M. Chechik & J.-F. Raskin, editors: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, Berlin, Heidelberg, pp. 573-579, doi: 10.1007/978-3-319-33600-8_28.
8. D. Matichuk, M. Wenzel & T. Murray (2014): An Isabelle Proof Method Language, In: ITP 2014, Volume 8558 of LNCS, pp. 390-405. Springer International Publishing, Vienna, Austria, doi: 10.1007/978-3-319-08970-6_25.

Extending the Dafny IDE with Tactics and Dead Annotation Analysis (tool demo)

1  Introduction

Dafny [4] is a verification-aware programming language where the specification of desired properties is intertwined with their implementation in the program text. It uses an automated theorem prover to prove that the specification is satisfied by the program. A specification serves two purposes: (1) it specifies the properties to be proven and acts as a documentation of the program, which is desirable to include in the program text; (2) it is used to guide the prover if a property cannot be verified without help. This is a necessary evil, which is not desirable and may obfuscate the readability of the program text. We will call these specification elements that are only there to guide the prover for proofs.

Dafny has a Visual Studio IDE plug-in [6], which seamlessly applies the verification in the background. In this demonstration we will show two extensions to this IDE:

• In [3] we developed an extension to Dafny that enables users to encode verification patterns of proofs as tactics, while [2] extends the language and illustrates several patterns as tactics. We will illustrate ongoing work on integrating tactics into the IDE – this is described further in Section 2.
• We are working on developing a feature to automatically remove unnecessary proof elements and integrating this into the IDE – this is described in Section 3.

2  Working with Dafny tactics in the IDE

Tacny is a conservative extension of Dafny with features to implement verification patterns as tactics [1, 2]. This tactic language is a meta-language for Dafny, where evaluation of a tactic works at the Dafny level: it takes a Dafny program with tactics and tactic applications, evaluates the applications and produces a new valid Dafny program, where tactic calls are replaced by Dafny constructs that tactics have generated.

A tactic is a special Dafny ghost method, recognisable by the tactic keyword. It contains many features to talk about a program, and features to generate proofs in terms of Dafny by transforming the program. A crucial property is that neither the program, nor the actual (non-proof) specification, can be changed – which we call contract-preserving transformations [>1]. To illustrate, consider the following tactic:

tactic myTac(v:Element,t:Tactic)
{
tactic match v { t(); }
}

If the user selects ‘Read-only peek this tactic (F9)’ then a read-only window will appear in the editor, where the code is shown. This will not make any changes to source code:

A second alternative is to ‘Expand this tactic (F10)’. Here, the code that the tactic application generated will replace the tactic call. This is illustrated by the following screenshot:

Finally, in the top-level menu, a user can either disable tactics, meaning all tactic applications will be ignored, or expanding all tactic applications in the program:

The last option is to remove all “dead annotations”, which we discuss next.

3  Dead annotation removal

1])

A fully verified Dafny program may contain unnecessary proof annotations, which may obfuscate the program text. There are at least two reasons for why such “dead annotations” may be present:

1. Proof constructs are normally added incrementally to the program text until a proof is found. Previous increments may not have helped to progress the proof, but are left by the user.
2. The underlying verifier is improved such that guidance that used to be required is no longer needed.

Inspired by the dead code optimisation< found in most compilers, we have developed a tool called DARe (Dead Annotation Removal) that works by traversing the Dafny abstract syntax tree and remove as many annotations as possible. Each time an annotation is removed, Dafny is applied to check if the program still verifies, and the constructs will only be removed if Dafny does not complain. Here an annotation can be:

• an assertion,
• a call to lemma,
• a loop invariant,
• a loop variant (decreases clause),
• a step in a calculation (Dafny supports Dijkstra style calculational proofs [5]).

We are integrating the DARe tool into the Dafny Visual Studio IDE. It will initially apply DARe to all methods (that does not have any verification errors) after the IDE has remained idle (i.e. no user-interaction) for at least 10 seconds. As DARe will be relatively slow to run, it will terminate (with failure) once a user starts interacting with the system. When it successfully terminates, all unnecessary (or dead) annotations will be highlighted (underlined and greyed out). This is illustrated on line 31 of the following screen-shot:

The user can then press the light-bulb to get the options of removing the given dead annotation or all dead annotations of the method or file, as illustrated below:

The different options will behave as follows:

• The first option will only remove the selected dead annoation.
• The second option will remove all dead annotations in the current block (e.g. the method).
• The final option will remove all dead annotations in the entire file.

The tool will keep track of any methods that are changed since last time DARe was applied and will reapply DARe when a method have changed. Again, this will only happen if the method does not have any verification errors and the system remains idle for 10 seconds.

4  Summary

This tool demonstration shows two extensions to the Dafny Visual Studio IDE. Both of the extensions have the ability to improve the program text and to support users when developing Dafny programs: re-usable tactics can replace proofs by high-level proof patterns, while proof elements that are not required can be removed in a semi-automatic manner.

References

1. Duncan Cameron, Gudmund Grov, and Léon McGregor (2016): What is your actual annotation overhead? In informal proceedings of the 28th Nordic Workshop on Programming Theory (NWPT 2016). Kim G. Larsen and Jiri Srba (editors), pp. 15-17. Available from http://nwpt2016.cs.aau.dk/nwpt2016-proceedings.pdf.
2. Gudmund Grov, Yuhui Lin, and Vytautas Tumas (2016): Mechanised Verification Patterns for Dafny. In 21st International Conference on Formal Methods (FM 2016), pages 326-343, volume 9995 of LNCS, Springer, doi:10.1007/978-3-319-48989-6_20.
3. Gudmund Grov and Vytautas Tumas (2016): Tactics for the Dafny Program Verifier. In Marsha Chechik and Jean-François Raskin, editors, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 36-53. Springer, 2016. doi:10.1007/978-3-662-49674-9_3
4. K. Rustan M. Leino (2010): Dafny: An automatic program verifier for functional correctness. In LPAR 2010, volume 6355 of LNCS, pages 348–370. Springer-Verlag, doi:10.1007/978-3-642-17511-4_20
5. K. Rustan M. Leino and Nadia Polikarpova (2013): Verified Calculations. In VSTTE, 2013. Volume 8164 of LNCS, pages 170-190. doi:10.1007/978-3-642-54108-7_9
6. K. Rustan M. Leino and Valentin Wüstholz (2014): The Dafny integrated development environment. In Proceedings F-IDE 2014, EPTCS 149, 2014, pp. 3-15. doi:10.4204/EPTCS.149.2

---

This work has been supported by EPSRC grants EP/M018407/1 and EP/N014758/1. Special thanks to Rustan Leino and his colleagues at MSR. The work is an adaptation of features presented in [2, 3, 1].

---