ABSTRACT. TBA

ABSTRACT. 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 will illustrate the typical workflow of program verification using Why3's IDE, focusing on the key features of WhyML, auto-active verification, and proof maintenance.

ABSTRACT. Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK 2014 environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts.

In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the art automatic provers. Adding interactive proof features in SPARK2014 appears to be complicated by the fact that the proof tool chain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client/server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK2014.

ABSTRACT. Usability is crucial for the adoption of software development technologies. This is especially true in development stages, where build processes fail, because software is not yet complete or was incompletely modified. We present early work that aims to improve usability of the Combinatory Logic Synthesizer (CL)S framework, especially in these stages. (CL)S is a publicly available type-based development tool for the automatic composition of software components from a user-specified repository. It provides an implementation of a type inhabitation algorithm for Combinatory Logic with intersection types, which is fully integrated into the Scala programming language. Here, we specifically focus on building a web-based IDE to make potentially incomplete or erroneous input specifications for and decisions of the algorithm understandable for non-experts. A main aspect of this is providing graphical representations illustrating the step-wise search process of the algorithm. We also provide a detailed discussion of possible future work to further improve the understandability of these representations.

ABSTRACT. Abstract State Machines (ASMs) have shown to be a suitable high-level specification method for complex, even industrial, systems; the ASMETA framework, supporting several validation and verification activities on ASM models, is an example of a formal integrated development environment. Although ASMs allow modeling complex systems in a rather concise way -and this is advantageous for specification purposes-, such concise notation is in general a problem for verification activities as model checking and theorem proving that rely on tools accepting simpler notations. In this paper, we propose a flattener tool integrated in the ASMETA framework that transforms a general ASM model in a flattened model constituted only of update, parallel, and conditional rules; such model is easier to map to notations of verification tools. Experiments show the effect of applying the tool to some representative case studies of the ASMETA repository.

ABSTRACT. Alloy is a lightweight formal specification language, supported by an IDE, which has proven well-suited for reasoning about software design in early development stages. The IDE provides a Visualizer that produces graphical representations of analysis results, which is essential for the proper validation of the model. Alloy is a rich language but inherently static, so behavior needs to be explicitly encoded and reasoned about. Even though this is a common scenario, the Visualizer presents limitations when dealing with such models. The main contribution of this paper is a principled approach to generate instance visualizations, which improves the current Alloy Visualizer, focusing on the representation of behavior.

ABSTRACT. In this short talk we present our experience in using VDMSL as tool for understanding a complex requirements specification of our model of the upcoming EMVCo Next Generation Kernel specifications. EMVCo is the consortium including MasterCard, Visa, Amex, etc for worldwide payment systems. It includes the familiar Chip&Pin and contactless protocols, as well as a number of new operational modes, security verification types (including biometric). EMVCo's objective is to ensure the requirements are are safe/correct as possible.

In order to engage them with any findings, a conversation between ourselves and stakeholders within EMVCo sub-groups has been established through formal simulation of specific protocol runs using VDMSL. The results have been productive and substantial: a number of corrections were suggested, and most importantly a large number of hidden assumptions about types, APIs, and other system parts have been carefully documented.

An issue of attempting to apply formal methods to industrial problems is that elegance often needs to be compromised in order to ensure stakeholders notice/accept the formal results: they ought to see what was built as their artefact, rather than a nicer abstraction.

Our aim, which we have achieved, is to influence the specification process prior to public release later in 2018. To date, we have modelled about 75% of the whole EMV kernel, and hope to complete it by the middle of 2018. It comprises 135 modules and 40KLOC in VDMSL, some of which is automatically generated from an XSD/XML data dictionary.

The work unravelled many technical issues in terms of design decisions, identified tool bugs, as well as the limits of Overture as a tool for industrial use at this scale. We hope to discuss these issues and make some useful suggestions.

ABSTRACT. Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, however, to develop verification tools aiding industrial software developers to find bugs or bottlenecks in software systems faster and more easily. The KeY project constitutes a framework for specifying and verifying software systems, aiming at making formal verification tools applicable for mainstream software development. To help the developers of KeY, its users, and the deductive verification community, we summarize our experiences with KeY 2.6.1 in specifying and verifying real-world Java code from a users perspective. To this end, we concentrate on parts of the Collections-API of OpenJDK 6, where an informal specification exists. While we describe how we bridged informal and formal specification, we also exhibit accompanied challenges that we encountered. Our experiences are that (a) in principle, deductive verification for API-like code bases is feasible, but requires high expertise, (b) developing formal specifications for existing code bases is still notoriously hard, and (c) the under-specification of certain language constructs in Java is challenging for tool builders. Our initial effort in specifying parts of OpenJDK 6 constitutes a stepping stone towards a case study for future research.

ABSTRACT. Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?

ABSTRACT. This paper proposes the use of notebooks for the design documentation and tool interaction in the rigorous design of embedded systems. Conventionally, a notebook is a sequence of cells alternating between (textual) code and prose to form a document that is meant to be read from top to bottom, in the spirit of literate programming. We extend the use of notebooks to embedded systems specified by pCharts. The charts are visually edited in cells inline. Other cells contain can statements that generate code and analyze the charts qualitatively and quantitatively; in addition, notebook cells can contain other instructions to build the product from the generated code. This allows a notebook to be replayed to re-analyze the design and re-build the product, like a script, but also allows the notebook to be used for presentations, as for this paper, and for the inspection of the design. The interaction with the notebook is done through a web browser that connects to a local or remote server, thus allowing a computationally intensive analysis to run remotely if needed. The pState notebooks are implemented as an extension to Jupyter. The underlying software architecture is described and the issue of proper placement of transition labels in charts embedded in notebooks is discussed.

ABSTRACT. Although Formal Method (FM) based techniques and tools have impressively improved in recent years, the need to train engineers to be accomplished users of formal notation and tailor the tools/workflow to meet objectives of the specific application domain, involves a high initial investment and difficulty to actualize in large, legacy organizations. In this paper, we present our approach to address these challenges in Honeywell Aerospace and share our experiences en-route. Starting with a constrained, structured natural language notation to author requirements and orchestrated with a set of novel in-house tool suite our approach allows automatically transforms those requirements into a consolidated formal representation to perform rigorous analyses and test generation. While the notation's natural-language flavor provides a `softer' front end, the tools-suite allows 'transparent' use of formal tools at the back-end without engineers having to know the underlying mathematics and theories. The initial application of our approach across various avionic software systems in Honeywell is well-accepted due to it minimal impact on the existing workflow while leveraging the benefits of formal methods.

ABSTRACT. Creating formal models of interactive systems has wide reaching benefits, not only for verifying low-level correctness, but also as a tool for ensuring user interfaces behave logically and consistently. Despite this, tools for designing user experiences and tools for creating and working with formal models are typically distinctly separate systems. This work aims to bridge this divide by allowing the generation of state machine diagrams and formal models via a simple, interactive prototyping tool that mirrors the basic functionality of many modern digital prototyping applications.