Dutch Model Checking Day 2016

About the Dutch Model Checking Day 2016

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.

This year's Dutch Model Checking Day has a focus on symbolic approaches to model checking, as well as parallel computation of model checking algorithms. The DMCD coincides with the PhD defense of Tom van Dijk. At 16:45, Tom van Dijk defends his thesis titled "Sylvan: Multi-core Decision Diagrams".

Programme

10:30 - 11:15

Gianfranco Ciardo: Decision diagrams: definitions, applications, and open problems

Binary decision diagrams (BDDs) have had enormous success since Bryant showed how to use them for the efficient verification of boolean hardware designs and Clarke and McMillan employed for symbolic model checking.
In this talk, we take BDDs as a starting point and explore various extension of decision diagrams, we apply them to problems beyond temporal logic verification, and we discuss several challenging research problems related to decision diagrams.

11:15 - 12:00

Yann Thierry-Mieg: Using the Guarded Action Language to express concurrent semantics

Much progress has been made for verification by model-checking of concurrent systems, despite the state space explosion problem. However building a tool that leverages this progress but remains versatile enough to tackle a wide variety of specification formalisms is a challenge.
The problem is to isolate the entities that model-checking reasons on, i.e. Kripke structures (KS) representing the state graph, from the actual system specification expressed in e.g. Petri nets, Promela, Divine, ... Too much opacity in the way the states are represented or the way the transition relation operates can severely limit the set of techniques a model-checker can deploy.
The PINS interface of LTSmin is a good compromise, as it exposes more information than a KS, but actions remain opaque (only their support is known). We propose instead a pivot language GAL to express concurrent semantics, designed to be as simple as possible while still preserving high expressivity.
Model translation approaches are popular industrially and well supported by tools, and the current trend is to develop ad hoc Domain Specific Languages. The GAL language currently features a user friendly front-end, EMF support, various structural reductions, powerful decision diagram based model-checking engine, and (bounded) SMT based verification for a subset of the language.
http://ddd.lip6.fr

13:00 - 13:30

Joost-Pieter Katoen: Scalable Parameter Synthesis in Markov Models

In this talk, I'll discuss parameter synthesis: Given a Markov model whose transition probabilities are unknown, what are the parameter values for which a "bad" state is reached with a given low threshold? The parameter synthesis problem is intrinsically harder than the model checking problem. I'll present two techniques to tackle parameter synthesis. They outperform the existing approaches by several orders of magnitude regarding both run-time and scalability. The beauty of the second technique is its applicability to various probabilistic models. It in particular provides the first sound and feasible method for doing parameter synthesis of Markov decision processes.

13:30 - 14:00

Jan Friso Groote: Modal logics for extra-functional behavioural requirements

14:00 - 14:20

Boudewijn Haverkort: Using stochastic model checking to assess the cost of energy independence

In this presentation we address the cost of energy independence in smart homes with local energy generation and local storage, under stochastic grid outages and seasonal demand and production profiles. We provide a seasonal dependent battery management strategy, that reduces the costs of surviving grid outages. We use a survivability evaluation method based on model checking a stochastic hybrid model, represented as hybrid Petri net.

14:40 - 15:10

Alfons Laarman: Scalable Multi-Core Model Checking

Scalable parallel model checking on modern multi-core machines was a long thought to be impossible due to the memory-intensive nature of the procedure. We show how to scale multi-core model checking using an array of carefully designed algorithms and data structures.

15:10 - 15:30

Thomas Neele: Partial-order reduction for GPU model checking

Model checking using GPUs has seen increased popularity over the last years. Because GPUs have only a limited amount of memory, only small to medium-sized systems can be verified. We improve memory efficiency for explicit-state GPU model checking by applying on-the-fly partial-order reduction. The correctness of the proposed algorithms is proved using a new version of the cycle proviso. Benchmarks show that our implementation achieves a reduction similar to or better than the state-of-the-art techniques for CPUs, while the runtime overhead is acceptable.

15:30 - 15:50

Wytse Oortwijn: Distributed Binary Decision Diagrams for Symbolic Reachability

Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial verification algorithm is symbolic reachability, which systematically explores all reachable system states. We propose heterogeneous algorithms for BDD-based symbolic reachability, targetting compute clusters: high-performance networks of multi-core machines. In this presentation, we discuss the underlying components: the distributed BDD table, the operations for cluster-based work stealing, the distributed memoization table, and several other caching structures. All these components are designed to utilise the newest networking technology. We show good parallel and distributed scalability and improve on existing work by demonstrating speedups up to 45.9 with 64 machines. Therefore, our reachability method not only benefits from the large amounts of available memory on compute clusters, but can also effectively use all the computational power available from their CPUs.

Registration

Registration is free, including lunch. You can now register for the Dutch Model Checking Day 2016 by sending an email to dmcd2016@utwente.nl. Please include your name, email, institution and whether you want to have lunch with us (and if you have dietary requirements), as well as any questions or comments that you may have. The registration deadline is July 6th, 2016.

Venue

The Dutch Model Checking Day 2016 takes place at the University of Twente.

The location for the DMCD is the Ravelijn building, room 1501. The PhD Defense will be in the Waaier building, room 4 (the Prof.dr. G. Berkhoff room). These locations are very close to each other.

See also this route description how to reach the University of Twente. If you arrive by train, it is sometimes more convenient to take a bus (line 9) from Hengelo. Applications like 9292.nl should give you the best option using the destination address: Drienerlolaan 5, Enschede.

Organisation

Formal Methods and Tools
Faculty of EEMCS
University of Twente

Organising Committee

Tom van Dijk (UT)
Jaco van de Pol (UT)
Ida den Hamer (UT)

Contact Address

Dutch Model Checking Day
Formal Methods and Tools
Faculty of EEMCS
University of Twente
P.O. Box 217, 7500 AE Enschede

Phone: +31 53 489 3767
Email: dmcd2016@utwente.nl
URL: http://fmt.cs.utwente.nl/workshops/dmcd2016/