The SPIN98 workshop was held on Monday November 2, 1998, the day before IFIP FORTE/PSTV98, at ENST in Paris, France. Below is the list of papers presented at the workshop, in order of presentation, with links to the postscript for online versions where available.
Abstract:
When verifying temporal properties of reactive systems, the common
wisdom is: if it is finite-state, model-check it, otherwise one must
use temporal deduction, supported by theorem provers such as STEP,
PVS, etc.
The study of abstraction as an aid to verification demonstrated that, in some interesting cases, one can abstract an infinite-state system into a finite-state one. This suggests an alternative approach to the temporal verification of infinite-state systems: abstract first and model check later.
In this talk, we explore the generality of this alternative approach. Namely, is it the case that everything that can be verified using temporal deduction can also be verified by abstraction followed by finite-state model checking? We will identify classes of properties and abstractions for which the VFA (Verification by Finitary Abstraction) approach is sound and complete.
Elie Najm: [email protected] Ahmed Serhrouchni: [email protected] Gerard Holzmann: [email protected]