Technical Reports

A List by Author: Pavel Moravec

e-mail:

xmoravec(a)fi.muni.cz

home page:

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

Under-Approximation Generation using Partial Order Reduction

by Lubo¹ Brim, Ivana Èerná, Pavel Moravec, Jiøí ©im¹a, A full version of the paper submitted to conference CAV05 February 2005, 21 pages.

FIMU-RS-2005-04. Available as Postscript, PDF.

Abstract:

We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.

Accepting Predecessors are Better than Back Edges in Distributed LTL Model Checking

by Lubo¹ Brim, Ivana Èerná, Pavel Moravec, Jiøí ©im¹a, A full version of the paper accepted to the conference FMCAD 2004. November 2004, 22 pages.

FIMU-RS-2004-09. Available as Postscript, PDF.

Abstract:

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.