- FM 2019 – 23rd International Symposium on Formal Methods
- MPC 2019 – 13th International Conference on Mathematics of Program Construction
- PPDP 2019 – 21st International Symposium on Principles and Practice of Declarative Programming
- RV 2019 – 19th International Conference on Runtime Verification
- SAS 2019 – 26th International Static Analysis Symposium
- TAP 2019 – 13th International Conference on Tests and Proofs
- UTP 2019 – 7th International Symposium on Unifying Theories of Programming
- VECoS 2019 – 13th International Conference on Verification and Evaluation of Computer and Communication Systems
Information about other co-located events will be provided as soon as their websites are available.
- AFFORD 2019 – Practical Formal Verification for Software Dependability
- DALI 2019 – Dynamic Logic: New Trends and Applications
- EFM 2019 – 1st International Workshop on Empirical Formal Methods
- FMBC 2019 – Workshop on Formal Methods for Blockchains
- FMIS 2019 – 8th Formal Methods for Interactive Systems Workshop
- F-IDE 2019 – 5th Workshop on Formal Integrated Development Environment
- HFM 2019 – History of Formal Methods
- OVT 2019 – 17th Overture Workshop
- RPLA 2019 – Reversibility in Programming, Languages, and Automata
Information about all other workshops will be provided as soon as their website are available.
Doctoral Symposium & Industry Day
- ALLOY – Formal software design with Alloy and Electrum
- Duration: 1 day
- 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.
- 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
- Duration: 1/2 day
- 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.
- 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).
- FM4BioMed – Formal Methods for BioMedicine
- FRAMA-C-IoT – Formal Verification of IoT Software with Frama-C
- Duration: 1/2 day
- 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.
- 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
- Duration: 1 day
- 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 com- positional 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 subcomponents 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.
- Presenters: Stefan Nitsch (Computer Science Department, Carnegie Mellon University, Pittsburgh, USA) and André Platzer (Computer Science Department, Carnegie Mellon University, Pittsburgh, USA).
- MLFV – ML + FV = ♥? A Gentle Introduction to the use of Machine Learning within Formal Verification Tools
- Duration: 1/2 day
- 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.
- Presenters: Moussa Amrani(University of Namur, Belgium), Levi Lucio (fortiss GmbH, Germany) and Adrien Bibal (University of Namur, Belgium).
- SRV – Stream-based Runtime Verification
- Duration: 1 day
- 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.
- 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).