Publication at MEMOCODE 2016

Another publication has been accepted at MEMOCODE’16.

Bernhard K. Aichernig and Richard Schumi. Towards Integrating Statistical Model Checking into Property-Based Testing. In 14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE, Kanpur, India, Nov. 18–20, 2016, pages 71–76. IEEE Computer Society, 2016. (PDF)(doi:10.1109/MEMCOD.2016.7797748)


In recent years statistical model checking (SMC) became increasingly popular, mainly because it does not suffer from one of the major problems that limits traditional model checking, the so called state-space-explosion problem. SMC solves this problem by simulating a stochastic model for finitely many executions. There exist a number of SMC tools, but they require the user to learn a specific modelling language and a particular (temporal) logic to express properties. In this paper we propose a more flexible application of SMC, where both the model and the properties can be defined in a programming language. The technique builds upon the well-known property-based testing approach. We use the programming language C\# and its associated tool FsCheck to demonstrate our approach. A stochastic counter serves as illustrating example.

Leave a Reply

Your email address will not be published. Required fields are marked *


You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>