First Workshop on
Statistical Model Checking
INRIA Rennes, France
23 September 2013

The SMC 2013 Workshop, associated with Runtime Verification 2013 (RV'13) provides an opportunity for participants to discuss about Statistical Model Checking. The workshop will be held before the main conference on 23 September at INRIA Rennes.


Statistical Model Checking has recently been proposed as an alternative to avoid an exhaustive exploration of the state space of a system under verification. The core idea of the approach is to conduct some simulations of the system and then use results from the statistics area in order to decide whether the system satisfies the property with respect to a given probability. The answer is correct up to some confidence. SMC is generally much faster (but less precise) than formal verification techniques. Moreover, the approach can be used to verify properties that cannot be expressed by the classical temporal logics used in formal verification. The objective of SMC 2013 is to discuss recent advances in Statistical Model Checking.


Anything that is related to Statistical Model Checking, from theory to applications and tools.

Call for Papers

Submissions to SMC 2013 can be of two kinds:

Both types of submissions will be carefully evaluated by the Program Committee. The page limit for both types of submissions is 15 pages; additional material may be submitted in a clearly marked appendix which may or may not be evaluated by the program committee.

Submissions must be formatted using the EPTCS LaTeX document class and uploaded at

Invited Speakers


Monday 23 September
8:00 Registration opens
8:30 Alexandre David Invited talk: Statistical model checking in UPPAAL, let's practice
9:30 Session 1: Applications I Chair: Pieter-Tjerk de Boer
Chakraborty, Katoen, Sher, Strelec Modelling and Statistical Model Checking of a Microgrid
10:00 Coffee
10:30 Session 2: Tools Chair: Alexandre David
Boyer, Corre, Legay, Sedwards PLASMA-lab: a flexible, distributable statistical model checking library
Nouri, Legay, Bensalem, Bozga SBIP: A Statistical Model Checking Extension for the BIP Framework
Barbot Comparison of Statistical Model Checkers
11:15 Session 3: Rare events Chair: Radu Grosu
Jegourel, Legay, Sedwards Importance Splitting for Statistical Model Checking of Rare Properties
Reijsbergen, de Boer, Haverkort, Scheinhardt Recent Advances in Importance Sampling for Statistical Model Checking
12:15 Lunch
13:30 Sylvain Peyronnet Invited talk: Probabilistic model checking and approximation. Chair: Serge Haddad
14:30 Session 4: Advanced SMC I Chair: Cyrille Jegourel
Zuliani Simulation-based Verification for Markov Decision Processes
Ellen, Gerwinn, Fränzle Statistical Model Checking of Stochastic SMT with Continuous Quantifiers
15:30 Coffee
16:00 Session 5: Advanced SMC II Chair: Sean Sedwards
Reijsbergen, de Boer, Scheinhardt, Haverkort Reliable Sequential Testing For Statistical Model Checking
Grosu Uniform Lasso Sampling
17:00 Session 6: Applications II Chair: Paolo Zuliani
Poulsen Statistical Model Checking of Event Patterns using Test Automata
Ballarini Analysis of oscillatory trends through HASL statistical model checking
Wognsen, Hansen, Larsen Evaluating Battery-Aware Soft Real-Time Schedulers Using Statistical Model Checking
18:30 Program ends

Submission and Publication

The SMC'13 workshop proceedings will be published as a volume of the EPTCS series.

Submission of papers to SMC'13 is handled through EasyChair. The submission link is

SMC'13 Sponsors