Under-Approximation Generation using Partial Order Reduction

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BRIM Luboš ČERNÁ Ivana MORAVEC Pavel ŠIMŠA Jiří
Year of publication	2005
Type	Monograph
MU Faculty or unit	Faculty of Informatics
Citation
Description	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.
Related projects:	Automated Verification of Parallel and Distributed Systems