Technical Reports
The report FIMU-RS-2005-04
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.
Responsible contact:
vedaXDjbU2LSW@fiQ1T5fpnNE.muni8CVI=SRv5.cz
Please install a newer browser for this site to function properly.