Technical Reports

A List by Author: Václav Rosecký

e-mail:

xrosecky(a)fi.muni.cz

home page:

https://www.fi.muni.cz/~xrosecky/

Verification Manager: Automating the Verification Process

by Radek Pelánek, Václav Rosecký, March 2009, 17 pages.

FIMU-RS-2009-02. Available as Postscript, PDF.

Abstract:

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. With the aim of automating the verification process, we elaborate on a concept of a verification manager. The manager automates some step of the verification process and enables efficient parallel combination of different verification techniques. We describe a realization of this concept for explicit model checking and discuss practical experience. Particularly, we discuss the problem of selection of input problems for evaluation of this kind of tool.

Evaluation of State Caching and State Compression Techniques

by Radek Pelánek, Václav Rosecký, Jaroslav ©edìnka, February 2008, 19 pages.

FIMU-RS-2008-02. Available as Postscript, PDF.

Abstract:

We study two techniques for reducing memory consumption of explicit model checking - state caching and state compression. In order to evaluate these techniques we review the literature, discuss trends in relevant research, and perform experiments over a large benchmark set (more than 100 models). The conclusion of our evaluation is that it is more important to combine several simple techniques in an appropriate way rather than to tune a single sophisticated technique.