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 2016) 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".
10:30 - 11:15
Gianfranco Ciardo: Iowa State University, USA
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: LIP6 - University Paris Marie Curie
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.
13:00 - 13:30
Joost-Pieter Katoen: RWTH Aachen, University of Twente
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: Eindhoven University of Technology
Modal logics for extra-functional behavioural requirements
Using the modal mu-calculus with data and time as used
in the mCRL2 toolset very complex functional requirements about
behavioural models (= software) can be phrased.
A natural question is whether non functional or extra functional properties
can also be formulated. Typically non functional requirements are whether
the expected response time is within bounds, whether buffers will on average
not overflow, or whether computational resources are sufficient to handle
We show that the modal mu-calculus is sufficiently expressive to express
the typical notions, such as limits and expected values, that are needed
to express such non functional requirements.
14:00 - 14:20
Boudewijn Haverkort: University of Twente
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: Technical University of Vienna
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: University of Twente, Eindhoven University of Technology
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: University of Twente
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 is free, including lunch.
You can now register for the Dutch Model Checking Day 2016
by sending an email to email@example.com.
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.
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.