Model checking is a tool-supported technique to analyze the correctness of ICT systems that enjoys increasing popularity in both scientific and industrial circles. In the past twenty-five years, 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 major corporations such as Microsoft and Intel to invest in the development and application of model checking technology.
The Dutch Model Checking Day (DMCD) is a forum for practitioners and researchers interested in model-based techniques for the validation and analysis of software and hardware. DMCD covers a broad spectrum of topics, ranging from fundamental algorithms to industrial applications and tools. The workshop aims to foster interactions and exchanges of ideas with all related areas in software engineering.
DMCD 2012 will take place at VU University Amsterdam.
Note that the event does not take the whole day, but half a day (afternoon), as it is scheduled after the PhD defense of Ela Krepska. Note also, there will be a (late) lunch served to the participants.
We hope to see you there! Organizers
| Invited speakers | Program | Registration | Venue |
| Previous events | Program committee | Contact | Call for participation |
Invited speakers (alphabetically)Back to top
Jiri Barnat, Masaryk University, Brno, Czech Republic
Speaker's short bio:
Jiri Barnat is an Associate Professor in the Faculty of Informatics
at Masaryk University, Brno, Czech Republic.
He has previously been affiliated with CWI, Amsterdam,
as well as at the University of Aalborg
and INRIA Rhone-Alps.
His research
interests include parallel algorithms
for inherently sequential problems,
formal verification (LTL Model-Checking,
Probabilistic LTL), and algorithm
engineering (multi-core performance
tweaking, I/O efficient algorithms).
Jiri completed his PhD studies at Masaryk University in
2005, with a thesis on Distributed-Memory LTL Model Checking.
See www.fi.muni.cz/~xbarnat/
for more details.
Talk title (updated):
GPU Accelerated Explicit-State Model Checking
Abstract (updated):
Within the talk we will explore the possibility of employing CUDA technology for acceleration of the explicit state LTL model checking process. In particular, we will show how to reformulate exisiting parallel model checking algorithms for efficient CUDA utilization as well as explore the possibility of employing multiple CUDA devices for acceleration of a single verification task.
Dragan Bosnacki, Eindhoven University of Technology, Netherlands
Speaker's short bio:
Dr. Dragan Bosnacki obtained his BSc and MSc degrees
from Sts. Cyril and Methodius University in Skopje
and his PhD degree from Eindhoven University of
Technology, where he is currently an assistant
professor. His main research interests are in
model checking and applications of computer
science in biology and medicine. In the model
checking community he is best known by his work
on methods for coping with the state space
explosion problem, e.g., partial-order reduction
and symmetry reduction. Several of his
contributions are implemented in Spin, which is
probably the best known model checking tool. In
the recent years he coauthored the pioneering
papers on parallel model checking algorithms for
multi-core systems and GPUs.
See www.win.tue.nl/~dragan/
for more information.
Talk title:
Modeling and analysis of protein biosynthesis using probabilistic model checking
Abstract:
Probabilistic model checking can be used very
effectively to model biological systems. In many
such cases model checking can replace successfully
stochastic simulations. We present a stochastic
model of the translation of mRNA into proteins,
which is one of the basic processes in the cell.
With this model one can analyze the errors that
occur in the synthesized proteins as well as the
translation times that are needed to translate
specific mRNAs. Besides their fundamental
importance, this kind of models have potential
applications in the development of antibiotics and
for an industrial scale biosynthesis of proteins.
We argue that the presented model is a
representative of an interesting class of
biological problems that can be tackled by
probabilistic model checking.
Byron Cook, Microsoft Research, Cambridge, UK
Speaker's short bio:
Dr. Byron Cook is a Principal Researcher at Microsoft Research Cambridge, as well
as Professor of Computer Science at University College London. His research interests
focus on formal verification, theorem proving, operating systems and biology.
Byron is particularly well known for his work on the Terminator program termination prover
as well as the SLAM software model checker.
See research.microsoft.com/~bycook
for more information.
Talk title:
A new approach to temporal property verification
Abstract:
I will describe a new approach to the old problem of automatic temporal property verification.
As well as leading to dramatic performance improvements over existing techniques,
this approach also brings some light on old questions.
Ana Varbanescu, Delft University of Technology, Netherlands
Speaker's short bio:
Dr. Ana Varbanescu is PostDoctoral Researcher within the Parallel and Distributed
Group of the TU Delft, Faculty of Engineering, Mathematics and Computer Science (EWI),
where she received her PhD in 2010.
She received her Engineer diploma (2001), and her MSc degree (2002) from
the Politehnica University of Bucharest, Romania, in the field of Computer Science and Engineering.
Her research interests are in the areas of embedded multi-processor architectures (MPSoCs),
focusing on parallel programming models and analytical performance prediction.
See www.st.ewi.tudelft.nl/~varbanescu/
for more information.
Talk title:
Large-scale graph processing in the many-core era
Abstract:
Many-core systems have already become
state-of-the-art in all computing devices, from
mobile phones to supercomputers, clusters and
clouds. Because of their fine-grain massive
parallelism, these platforms are hardly seen as a
good match for the inherently irregular nature of
graph processing. In this talk, I will discuss the
real limitations of these platforms, from the
perspective of graph processing, and discuss
several ways in which many-cores can be used to
improve the performance of graph processing
algorithms.
ProgramBack to top
| 14:30-15:00 | Food and drinks and registration |
| 15:00-15:40 | GPU Accelerated Explicit-State Model Checking (title updated) |
| 15:40-16:20 | Modeling and analysis of protein biosynthesis using probabilistic model checking |
| 16:20-16.40 | Short break |
| 16:40-17.20 | A new approach to temporal property verification |
| 17:20-18.00 | Large-scale graph processing in the many-core era |
| 18:00-18.15 | Farewell drinks |
Registration Back to top
Registration is free of charge. Please register by sending an e-mail to .VenueBack to top
The DMCD'12 takes place at VU University Amsterdam, in the main building (`hoofdgebouw'), room 4A04.- Address:
De Boelelaan 1105
1081 HV Amsterdam
T (centraal): 020 59 89898
F (centraal): 020 59 89899
- By train: exit at Amsterdam Zuid/WTC.
By tram 5/16/24 or subway 51: exit at De Boelelaan/VU.
Route description
To plan your journey: 9292.nl.
Maps of public transport - By car
- By taxi, for example TCA (+31 20 7777777 (7x7)) offers a good service.
- Getting to room A404: enter through the main entrance (from Boelelaan, near the bookstore), turn left to find the yellow elevators, go to floor 4, find room 4.
Previous events Back to top
Most recent previous events:Organizing committeeBack to top
- Henri Bal
- Wan Fokkink
- Thilo Kielmann
- Ela Krepska
Contact Back to top
DMCD'12 is organized by the VU University Amsterdam. Please direct questions to: Ela Krepska at e.krepska@vu.nl (preferred) or to:
Elzbieta Krepska
Dept. of Computer Science
De Boelelaan 1081
1081 HV Amsterdam, Netherlands
Dept. of Computer Science
De Boelelaan 1081
1081 HV Amsterdam, Netherlands