ABSTRACT. KeY is a deductive software verification approach and system, whose most elaborate version targets Java programs. In a recent KeY case study, which attracted attention also outside formal method circles, verification with KeY could reveal a bug in the main sorting routine of OpenJDK. While this talk will also cover the user interface of KeY, the focus of the discussion is more fundamental. KeY follows to a significant extent principles which are different from other deductive verification systems, on the level of the program logic, the proof calculus, the interaction with the prover, the transparency of proofs, and the usage of back-end solvers. In this talk, I will discuss the impact of these aspects, with a special focus on usability. In addition, we will look at how the design of the logic and calculus influenced the integration with other validation techniques, like test generation and runtime verification.

ABSTRACT. One of the ultimate goals of software engineering is to leave virtual spaces and move real things. We take one step toward supporting users with this goal by connecting a type-based synthesis algorithm, Combinatory Logic Synthesizer ((CL)S), and its IDE to a logistics lab environment. The environment is built and used by domain experts, who have little or no training in formal methods, and need to cope with large spaces of software, hardware and problem specific solution variability. It consists of a number of Cyber-Physical Systems (CPS), including wheel-driven robots as well as flying drones, and it has laser-based support to visualize their possible movements. Our work describes results on an experiment integrating the latter with (CL)S. Possibilities and challenges of working in the domain of logistics and in cooperation with its experts are outlined. Future research plans are presented and an invitation is made to join the effort of building better, formally understood, development tools for CPS-enabled industrial environments.

ABSTRACT. Ladder Logic is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of inputs (whose values are given at runtime by factory sensors), outputs (whose values are given at runtime to factory actuators), and the logical expressions computing output values from input values. Due to the graphical form of Ladder programs, and the amount of inputs and outputs in typical industrial programs, debugging such programs is time-consuming and error-prone. We present, in this paper, a Why3-based tool research prototype we have implemented for automating the use of deductive verification in order to provide an easy-to-use and robust debugging tool for Ladder programmers.

ABSTRACT. We present a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or white-box testing can be applied to the same source, which is part of an integrated PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for framing conditions.

Our framework supports semantic annotations of C sources in the form of comments. Annotations serve to locally control back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables.

Our approach demonstrates the degree of maturity and expressive power the Isabelle/PIDE subsystem has achieved in recent years. Our integration technique employs Lex and Yacc style grammars to ensure efficient deterministic parsing. We present two case studies for the integration of (known) semantic back-ends in order to validate the design decisions for our back-end interface.

ABSTRACT. The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications.

After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches.

ABSTRACT. The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools, but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming. The main features and architecture of the environment are presented, along with a comparison with other similar tools.

ABSTRACT. TLA+ is a high-level, math-based, formal specification language used at companies such as Amazon and Microsoft to verify designs of distributed and concurrent systems. TLA+ specifications are written with the publicly available TLA+ Toolbox and verified by tools run from it. Those tools include a model checker and a proof system that can be used together on the same spec.

The paper discusses the rationale and drawbacks of the Toolbox's main features. Specifically, it reports on two Toolbox features which — to the best of our knowledge — are novel in the scope of formal IDEs: CloudTLC connects the Toolbox with cloud computing to scale up model checking. Moreover, CloudTLC allows to verify large numbers of models concurrently which enables users to explore a specification's design space faster. The expressiveness of TLA+ results in stated expressions that present a challenge for the model checker to evaluate efficiently. To address this challenge, the Toolbox provides a Profiler to analyze the evaluation to override inefficient expressions with efficient ones. We provide a summary about the Toolbox's architecture and its test infrastructure to show how others can add new features. The paper concludes with outlining future research and engineering-related work.

ABSTRACT. Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode can not take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework.

ABSTRACT. Development processes in various engineering disciplines are incorporating formal models to ensure safety properties of critical systems. The use of these formal models requires to reason about their adequacy, i.e., to validate that a model mirrors the structure of the system sufficiently that properties established for the model indeed carry over to the real system. Model validation itself is non-formal, as adequacy is not a formal (i.e., mathematical) property. Instead it must be carried out by the modeler to justify the modeling to the certification agency or other stakeholders. In this paper we argue that model validation can be seen as a special form of requirements engineering, and that interactive visualization and concepts from requirements traceability can help to advance tool support for formal modeling by lowering the cognitive burden needed for validation. We present the VisualisierbaR tool, which supports the formal modeling of railway operations and describe how it uses interactive visualization and requirements traceability concepts to validate a formal model.