Under-Approximation Generation using Partial Order Reduction
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Monograph |
| MU Faculty or unit | |
| 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: |