From model checking to a temporal proof
2001
Model checking is used to automatically verify temporal properties of finite state systems. It is usually considered to be `sucessful', when an error, in the form of a counterexample to the checked property, is found. We present the dual approach, where, in the presence of no counterexample, we automatically generate a proof that the checked property is satisfied by the given system. Such a proof can be used to obtain intuition about the verified system. This approach can be added as a simple extension to existing model checking tools.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
10
References
0
Citations
NaN
KQI