Publication details

Under-Approximation Generation using Partial Order Reduction

Investor logo
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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info