Conferences and Symposia

Festschrifts

Doctoral Symposium &  Industry Day

Workshops

➡️ FM 2019 International Workshops (Volume I + Volume II) ⬅️

Tutorials

  • ALLOY – Formal software design with Alloy and Electrum
    1. Duration: 1 day
    2. Abstract: This full day tutorial will introduce participants to the Alloy and Electrum formal specification languages and the respective analysis tools. Alloy is a language that relies on relational logic to describe both the structures in a software design and its desired properties. Following the small scope hypothesis, which states that most bugs can be found with small counter-examples, the Alloy Analyzer verifies properties by automatically checking all scenarios up to a given user-specified scope. This verification is complemented with techniques to simplify design exploration, namely a customizable visualizer and a symmetry breaking mechanism that eliminates isomorphic scenarios. Electrum is an extension of Alloy tailored for reasoning about behavior. In Electrum both a system dynamics and its desired properties are specified declaratively using temporal relational logic, a language that adds linear temporal logic operators, including past ones, to relational logic. The Electrum Analyzer shares most of the features of its Alloy counterpart, adding bounded and complete model checking engines to support the verification of temporal properties. The tutorial will cover a range of topics, from the fundamentals of the logics to more advanced techniques useful in larger case studies, for example, techniques to debug specifications or to improve the visualization to ease the exploration of a design. After the tutorial, participants will be able to develop and analyze simple Alloy and Electrum specifications, and to determine whether these formal methods are well suited to apply in a concrete problem domain (either in a research or an industrial context). Educators will also gain access to a sample of materials and examples that could ease the introduction of these formal methods in their courses.
    3. Presenters: Alcino Cunha (HASLab/INESC TEC & U.Minho, Portugal), Eunsuk Kang (School of Computer Science, Carnegie Mellon University, USA), David Chemouil (ONERA, France), Julien Brunel (ONERA, France) and Nuno Macedo (HASLab/INESC TEC & U.Minho, Portugal).
  • CbC – The Correctness by Construction Approach to Programming
    1. Duration: 1/2 day
    2. Abstract: Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. The CbC approach to program development begins with a Hoare triple comprising a precondition, an abstract statement, and a postcondition. Such a triple should be read as a total correctness assertion, if the precondition holds and its abstract statement “executes” then the execution will terminate and its postcondition will hold. This triple can be refined by using a set of refinement rules, i.e., the statement is replaced by more concrete statements. For example, a loop is introduced, or an abstract statement is replaced by an assignment. If no abstract statement remains, the code is fully specialized. In the tutorial, we want to introduce participants to the CbC approach to programming. First, we provide the theoretical background of refinement rules. Afterwards, we apply the CbC approach to a series of examples. By using an open source tool, the participants can try the CbC approach on their own. In the end, we present how CbC supports the construction of large-scale algorithmic families, and compare CbC against post-hoc verification. The purpose of the tutorial is to influence the way the participants approach the task of developing algorithms. Instead of specifying a problem and solving the problem by coding with gut feelings and intuitions, we want to focus on the more formal CbC approach to construct programs. The participants should reflect on their coding style and find their best practice to construct formally correct programs. The tutorial relies on the following easily accessible text book: Derrick G. Kourie, Bruce W. Watson: The Correctness-by-Construction Approach to Programming. Springer 2012, ISBN 978-3-642-27918-8.
    3. Presenters: Ina Schaefer (Universität Braunschweig, Germany), Tobias Runge (Universität Braunschweig, Germany), Loek Cleophas (TU Eindhoven, The Netherlands) and Bruce Watson (Universiteit Stellenbosch, Germany).
  • (Cancelled) FM4BioMed – Formal Methods for BioMedicine
    1. Duration: 1 day
    2. Abstract: Biomedicine is undergoing a transformation towards a data-driven, quantitative science, while mathematical modeling techniques and computational approaches are increasingly becoming a part of systems biomedicine. A major effort in systems biomedicine goes into understanding the biological behavior of the whole based on the function of its parts, studying regulatory patterns, aberrations responsible for disease states, and compensatory pathways. On the other hand, the importance of biology as a new application area for applied mathematics and computer science is becoming increasingly apparent.
      Computer scientists entering this field often lack a background in biological sciences and may even lack training in the mathematical and computational techniques most often used in this field. Through this one-day tutorial, we aim to give an introduction to computational systems biomedicine, starting with a crash course on molecular biology for computer scientists, and continuing with an introduction to continuous and discrete modeling techniques, including formal methods-based modeling approaches. We also plan to overview several systems biology/biomedicine projects (including applications to oncology and a formal methods-based modeling of the heat-shock protein biological pathway) that we have been working on recently. We believe that this combination of concepts and techniques would give our audience a valuable insight into the beauty and the challenges of systems biomedicine. We also hope to show how computer science tools and techniques they are already familiar with can be applied to the biological setting.
    3. Presenters: Ion Petre (University of Turku, Finland), Orieta Celiku (National Cancer Institute, USA) and Luigia Petre (Åbo Akademi, Finland).
  • FRAMA-C-IoT – Formal Verification of IoT Software with Frama-C
    1. Duration: 1/2 day
    2. Abstract: Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), have proliferated very quickly in the past years. There are now billions of interconnected devices, and this number is growing. It is anticipated that by 2021, about 46 billions of devices will be in use. Some of these devices are in service in safety and security critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. Formal methods have been used successfully for years in highly critical domains, now they can help to bring security into the IoT field. In practice it is common to rely on a combination of formal methods to achieve an appropriate degree of guarantee: static analysis to guarantee the absence of runtime errors, deductive verification of functional correctness, dynamic verification for parts that cannot be proved using deductive verification. This tutorial gives a practical hands-on presentation of these verification techniques and is based on Frama-C, a source code analysis platform that aims at conducting verification of industrial-size programs written in ISO C99 source code. Frama-C fully supports the combination of formal methods approach, by providing to its users with a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. Moreover collaborative verification across cooperating plugins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language ACSL. Recently Frama-C has been applied to the verification of software in the context of the Internet of Things.This tutorial will be of interest for both researchers and practitioners interested in software verification in general, and in particular in IoT software, as well as for students in Software Engineering. Participants will learn how to use the different formal analysis techniques and how to combine them. The tutorial only assumes knowledge of the C programming language. Several examples and use cases presented during the tutorial will give them a clear practical vision of possible usages of the underlying static and dynamic analyses in their everyday work. To work on the exercises, the attendees will be provided a virtual machine image containing all the tools ready to use.
    3. Presenters: Allan Blanchard (Inria Lille – Nord Europe, France), Nikolai Kosmatov (CEA, List, Software Reliability and Security Lab, France) and Frédéric Loulergue (School of Informatics Computing and Cyber Systems, Northern Arizona University, USA).
  • KEYMAERA X – Modular Formal Verification of Cyber-Physical Systems with KeYmaera X
    1. Duration: 1 day
    2. Abstract: This tutorial studies modularity principles for the design and formal verification of cyber-physical systems (CPS), which are those that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPSs have many important applications, e.g., in robotics, aerospace, and automotive domains, but require careful designs to meet stringent safety demands. Formal verification techniques justify such safety properties but need to handle mathematical models of CPSs called hybrid systems, i.e., those that combine the discrete dynamics of stepwise controller computations with the continuous dynamics of their differential equations. This tutorial explains how differential dynamic logic (dL) for hybrid systems can be used to model and verify CPS in a modular fashion. Its theorem prover KeYmaera X provides compositional verification techniques for hybrid systems, which not only handle nonlinear systems but also use invariants to reduce the verification of larger systems to subsystems. For very large models, component-based modeling can be used to split large models into multiple component models with local responsibilities to further reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. We show how decomposition into sub-components works by disentangling the physical interaction into measurements and actuation guarantees that are represented in local contracts. More detail about the presented approach can also be found in the recent textbook on Logical Foundations of Cyber-Physical Systems.
    3. Presenters: Stefan Mitsch (Computer Science Department, Carnegie Mellon University, Pittsburgh, USA) and André Platzer (Computer Science Department, Carnegie Mellon University, Pittsburgh, USA).
  • (Cancelled) MLFV – ML + FV = ♥? A Gentle Introduction to the use of Machine Learning within Formal Verification Tools
    1. Duration: 1/2 day
    2. Abstract: Formal Verification (FV) and Machine Learning (ML) can seem incompatible due to their opposite mathematical foundations and their use in real-life problems: FV mostly relies on discrete mathematics and aims at ensuring correctness; ML often relies on probabilistic models and consists of learning patterns from training data.
      In this tutorial, we will explore how ML helps FV in some classical approaches: static analysis, theorem-proving, and SAT solving (and Model-Checking, if time permits). We draw a landscape of the current practice and demonstrate with practical examples from state-of-the-art tools some of the most prominent uses of ML in FV, thus offering a new perspective on FV techniques that can help researchers and practitioners to better locate potential synergies. We will discuss lessons learned from a survey we have done during the past year, point to possible improvements and offer visions for the future of the domain in the light of the science of software and systems modelling.
      The tutorial will be interactive in the sense that we will hold discussions with the audience in order to both challenge the views we present throughout the tutorial and gather directions for future research on this topic.
    3. Presenters: Moussa Amrani (University of Namur, Belgium), Levi Lucio (fortiss GmbH, Germany) and Adrien Bibal (University of Namur, Belgium).
  • SRV – Stream-based Runtime Verification
    1. Duration: 1 day
    2. Abstract: Runtime verification (RV) is a light-weight verification technique for online monitoring a particular execution of the system under test. While traditional RV approaches use temporal logics, Stream-based Runtime Verification (SRV) extends RV with the concept of complex event processing. SRV is not limited to verification of correct executions, but also allows to specify quantitative and statistical analyses of program traces. We present synchronous and asynchronous SRV languages, i.e. LOLA and the temporal stream-based specification language TeSSLa. After establishing the theoretical foundations we present software- and hardware-based implementations of SRV and compare them to other hardware-based RV~approaches. In this tutorial we consider cyber-physical systems (CPS) as an example application. We demonstrate how to use SRV to integrate continuous and discrete signals from different trace source of a CPS. We present a comprehensive approach to non-intrusive monitoring of multi-core processors using SRV. We demonstrate how embedded trace-ports of multi-core processors can be used to access the actual control flow trace executed by the program running on the processor. We carry out analyses on the control flow trace of typical cyber-physical systems in real time using FPGAs. We describe how light-weight, hardware-supported instrumentation can be used to enrich the control-flow trace with data values from the application. Finally, we demonstrate how these technologies can be used to detect data races in cyber-physical systems.
    3. Presenters: Martin Leucker (University of Lübeck, Germany), Torben Scheffel (University of Lübeck, Germany), Malte Schmitz (University of Lübeck, Germany), Daniel Thoma (University of Lübeck, Germany), César Sánchez (IMDEA Software Institute, Spain), Volker Stolz (Høgskulen på Vestlandet, Norway) and Alexander Weiss (Accemic GmbH, Germany).