Approximate Probabilistic Model Checking for Programs

Authors

Jérôme Darbon, Richard Lassaigne, Sylvain Peyronnet

Where

Proceedings of the IEEE 2nd International Conference on Intelligent Computer Communication and Processing (ICCP'06)

Place

Technical University of Cluj-Napoca, Romania

Type

inproceedings

Date

2006-07-27

Abstract

In this paper we deal with the problem of applying model checking to real programs. We verify a program without constructing the whole transition system using a technique based on Monte-Carlo sampling, also called “approximate model checking”. This technique combines model checking and randomized approximation. Thus, it avoids the so called state space explosion phenomenon. We propose a prototype implementation that works directly on C source code. It means that, contrary to others approaches, we do not need to use a specific language nor specific data structures in order to describe the system we wish to verify. Finally, we present experimental results that show the effectiveness of the approach applied to finding bugs in real programs.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  darbon.06.iccp,
  author	= {J\'er\^ome Darbon and Richard Lassaigne and Sylvain
		  Peyronnet},
  title		= {Approximate Probabilistic Model Checking for Programs},
  booktitle	= {Proceedings of the {IEEE} 2nd International Conference on
		  Intelligent Computer Communication and Processing
		  ({ICCP'06)}},
  year		= 2006,
  address	= {Technical University of Cluj-Napoca, Romania},
  month		= sep,
  abstract	= {In this paper we deal with the problem of applying model
		  checking to real programs. We verify a program without
		  constructing the whole transition system using a technique
		  based on Monte-Carlo sampling, also called ``approximate
		  model checking''. This technique combines model checking
		  and randomized approximation. Thus, it avoids the so called
		  state space explosion phenomenon. We propose a prototype
		  implementation that works directly on C source code. It
		  means that, contrary to others approaches, we do not need
		  to use a specific language nor specific data structures in
		  order to describe the system we wish to verify. Finally, we
		  present experimental results that show the effectiveness of
		  the approach applied to finding bugs in real programs.}
}