Dutch Model Checking Day 2022 – GEARS: An NWO TOP funded research project

About Dutch Model Checking Day 2022

Model checking is a tool-supported technique to analyse the correctness of ICT systems that enjoys increasing popularity in both scientific and industrial circles. In the past decades, research in this area has led to dramatic improvements in the performance of model checking tools. This has enabled its application to real-life problems and has induced various industries to invest in the development and application of model checkers.

The Dutch Model Checking Day (DMCD) is a forum for practitioners and researchers interested in model-checking based techniques for the validation and analysis of communication protocols and software systems. Topics covered in the DMCD include theoretical and algorithmic foundations and tools for distributed verification, large and infinite state spaces, coordination problems, timed systems and hybrid systems. The workshop aims to foster interactions and exchanges of ideas with all related areas in software engineering.

The Dutch Model Checking Day aims at providing a forum for discussions, to exchange ideas and inform each other on the state of the art in this research area.

Due to the tight Corona measures inflicted on the 2021 planned events, the DMCD 2022’s edition has been moved to the 10^th of March, 2022 as a hybrid event. The DMCD coincides with the PhD defense of Muhammad Osama at 16:00 (Atlas 0.710), entitled “GPU Enabled Automated Reasoning”.

Programme

10:00 – 10:25	Welcome (with Coffee or Tea)
10:25 – 12:00	Block 1 (Film room at De Zwarte Doos) – Session chair: Muhammad Osama
10:25 – 10:30	Opening by Anton Wijs
10:30 – 11:00	Joost-Pieter Katoen (RWTH Aachen University, DE) Title: Model Checking Recursive Probabilistic Programs. Abstract: Probabilistic push-down automata (pPDA) are a standard operational model for probabilistic programming languages involving recursive procedures. We show that the model checking problem of pPDA against omega-visibly push-down languages is decidable. This enables the automated verification of Alur et al.’s temporal logic CaRet, an extension of LTL that explicitly takes the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness of recursive probabilistic programs. This is joint work with Tobias Winkler and Christina Gehnen.
11:00 – 11:30	Armin Biere (University of Freiburg, DE) Title: Improving incremental SAT Solvers for Model Checking. Abstract: In SAT based model checking, SAT solvers need to work on many related queries over shared constraints. Incremental solving, i.e., using the SAT solver as a library and the same solver instance for multiple queries, can take advantage of information learned over the sequence of these queries. This can reduce accumulated solving time considerably and as a consequence overall model checking time too. After going over classical approaches to incremental solving, we discuss trade-offs between preprocessing and incremental solving for heavy solving tasks like bounded model checking with few but hard queries and then move to a lighter scenario with many but easy queries, as is common in IC3. The presented solutions range from extending the programmatic interface and algorithms of SAT solvers to a theoretical characterization of incremental SAT solving. This is joint work with Katalin Fazekas, Christoph Scholl and Nils Froleyks related to our SAT’19 and FMCAD’21 papers.
11:30 – 12:00	Tim Willemse (TU Eindhoven, NL) Title: Solving Symbolic Parity Games On-the-Fly. Abstract: Parity games can be used to encode a variety of decision problems. In practice, tools that use parity games often rely on a specification in a higher-order logic from which the actual game can be obtained by means of an exploration. For many of these decision problems we are only interested in the solution for a designated vertex in the game. We show how to use on-the-fly solving techniques during the exploration process, and illustrate that this can help to decide the winner of such a designated vertex in an incomplete game. Furthermore, we show how standard partial solving techniques can be made resilient to work directly on the incomplete game, rather than on a set of ‘safe’ vertices. Our implementation of our techniques for symbolic parity games shows that speed-ups of several orders of magnitude are feasible and overhead (if unavoidable) is typically low. This is joint work with Maurice Laveaux and Wieger Wesselink.
12:00 – 13:00	Lunch Break
13:00 – 14:00	Block 2 (Film room at De Zwarte Doos) – Session chair: Tim Willemse
13:00 – 13:30	Michel Reniers (TU Eindhoven, NL) Title: Translation of supervised controllers to mCRL2 models. Abstract: In this talk I will propose a method for transforming networks of extended finite automata, in the form of a CIF model, into an mCRL2 specification for the purpose of verfification of expected behavioural properties. The approach is illustrated using a case dealing the coordination of maintenance procedures for a high-end printer. It is also shown how the approach may be used to verify that a synthesized supervisor indeed has the properties safety (w.r.t. safety requirements used in the synthesis procedure), nonblockingness and controllability. The CIF 3 toolset is used to offer support for modelling, analysis and synthesis activities in a model-based systems engineering process. The main functionality ofthe CIF 3 toolset is the synthesis of supervisory controllers from discrete-event models of the uncontrolled system (plant) and the requirements. The supervisory controller that results from synthesis is correct (nonblocking, controllable, safe, and maximally permissive; insofar the models it is achieved from are a good representation of reality. read more To investigate this correctness of the plant, the requirements and the supervisory controller, the toolset allows simulation-based analysis. Simulation-based verification can only beused to demonstrate the presence of unexpected or wrong behaviour, but can never be used to conclude that the modelled system has certain properties (such as absence ofdeadlocks and livelocks). Model checking can be used for this purpose. It allows the specification of a (discrete-event) model and of a property (formulated as an expression in some modal logic) and rigorously checks that the property holds with respect to all behaviour of the modelled system. One example of such a model checker is mCRL2, where system sare described using a process algebraic formalism and properties are described in modal μ-calculus. In previous work, the problem of (efficient) verification of non-blockingness of extended finite automata has been considerusing a compositional approach. The main difference with the approach presented in this presentation is that our approach allows verification of an arbitrary behavioural property expressed by a modal μ-calculus formula. mCRL2 has already been used for verification of functional properties of supervisory controllers synthesized using Supremica. Both UPPAAL and mCRL2 have been applied to supervisory controllers synthesized on the basis of safety requirements in order to establish that the resulting controlled system has the intended behaviour (a.o. liveness properties). In both cases the transformation was implemented in a stand alone tool, whereas in this paper a transformation that is integrated in the CIF tool set has been used. This existing transformation basically translates each of the extended finite automata into an mCRL2 process definition. Combining these by means of the mCRL2 composition operators in order to mimic their synchronous composition has shown to result in an mCRL2 process that is hard to analyze. Especially, the linearization step that is required on an mCRL2 process before it can be further analysed in the mCRL2 toolset has shown to be computationally challenging. To avoid this problem, the present work proposes a more pragmatic approach that uses existing transformations and guarantees trivial linearization.
13:30 – 14:00	Hans Zantema (TU Eindhoven, NL) Title: The paint pot problem and finding models to prove unreachability. Abstract: On a finite sequence of paint pots the following steps are allowed: – Swap two consecutive non-empty pots. – If the two neighbors of a non-empty pot are empty, then divide the paint in the middle pot over the two neighbors, after which these neighbors will be non-empty and the middle one will be empty. Also the reverse allowed: if an empty pot has two neighbors of the same color, the paint of these neighbors may be put in the middle pot. Is it possible to start by a sequence in which the first four pots contain paint in four different colors, and get the first pot empty? This remarkably hard problem is an instance of model checking: it is a reachability problem in the above defined transition system. The negative answer will be given by a particular finite model, similar to the way MACE4 looks for such finite counter example models. In this case the model was found by SMT solving.
14:00 – 14:10	Coffee Break
14:10 – 15:10	Block 3 (Film room at De Zwarte Doos) – Session chair: Anton Wijs
14:10 – 14:40	Alfons Laarman (TU Leiden, NL) Title: Model Checking with Sentential Decision Diagrams. Abstract: Recently, Sentential Decision diagrams (SDDs) have been introduced for concisely representing Boolean functions. Like binary decision diagrams (BDDs), they are canonical and allow efficient manipulation operations on functions that have a small decision-diagram representation. This makes them ideally suited for model checking, an application that was not explored yet. In this talk, we discuss new heuristics for applying SDDs in model checking. With an implementation, we experimentally compare the performance with that of BDDs. We identify an expected trade-off between memory use and runtime, but also considerable room for further improvement based on the additional configuration parameters in SDDs.
14:40 – 15:10	Scott A. Smolka and Yifei Liu (Stony Brooke University, USA) Title: Model-Checking Support for File System Development. Abstract: Developing and maintaining a file system is time-consuming, typically requiring years of effort. Developers often test compliance with APIs such as POSIX with hand-written regression suites that, alas, examine only a fraction of a file system’s state space. Conversely, formal model checking can explore vast state spaces efficiently, increasing confidence in the file system’s implementation. Yet model checking is not currently part of file system development. Our position is that file systems should be designed a priori to facilitate their model checking. To this end, we introduce MCFS, an architecture for efficient and comprehensive file-system model checking. MCFS relies on two new APIs that save and restore a file system’s in-memory and on-disk state. We describe our earlier attempts at model-checking file systems, including unsuccessful or inefficient ones. Those attempts resulted in VeriFS, a FUSE-based file system we developed with MCFS’s help that implements the new APIs.
16:00 – 17:00	PhD Defense – GPU Enabled Automated Reasoning (Atlas 0.710)

Registration

Participation is free and includes lunch. You can register to the DMCD’22 via this form. Please submit your name, email, institution and indicate if you would like to join physically and have lunch (with any dietary requirements). The registration deadline is February 28^th, 2022. [closed]

Location

The Dutch Model Checking day 2022 will take place at Eindhoven University of Technology (TU/e). The hosting room is “Film Zaal” on the second floor of “De Zwarte Doos” restaurant.

Organising Committee

Muhammad Osama (TU/e)

Email: o.m.m.muhammad@tue.nl

Anton Wijs (TU/e)

Email: a.j.wijs@tue.nl

Sponsers