Towards Smaller Invariants for Proving Coverability
In this paper, we explore a possibility of improving existing methods for verification of parallel systems. We particularly concentrate on safety properties of well-structured transition systems. Our work has relevance mainly to recent methods that are based on finding an inductive invariant by a sequence of refinements learned from counterexamples. Our goal is to improve the overall efficiency of this approach by concentrating on choosing refinements that lead to a more succinct invariants. For this, we propose to analyze so called minimal counterexample runs. They are digests of counterexamples concise enough to allow for a more detailed analysis. We experimented with a simple refinement algorithm based on analysing minimal runs and succeeded in generating significantly more succinct invariants than the state-of-the-art methods.
- 2.Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: IEEE Computer Society LICS 1996, pp. 313–321 (1996)Google Scholar
- 6.Kaiser, A., Kroening, D., Wahl, T.: Bfc - a widening approach to multi-threaded program verification. http://www.cprover.org/bfc/