Towards automatic determination of problem bounds for object instantiation in static model verification
Mathias Soeken, Robert Wille, Rolf Drechsler · 2011
The application of formal methods in the detection of inconsistencies and design flaws within models has been intensely studied in recent years. Since consistency checking is in principle undecidable due to the infinite number of possible system states, problem bounds have to be defined making the analysis tractable. However, defining these problem bounds requires detailed design knowledge and, thus, impedes an automatic verification flow.