Abstract
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.
This work was supported by the Czech Science Foundation project 16-24707Y, the BUT FIT project FIT-S-17-4014, and the IT4IXS: IT4Innovations Excellence in Science project (LQ1602).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Optimizations like this are rather orthogonal to the choice of the main algorithm.
References
Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16(4), 457–515 (2010)
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)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7
Clarke, E.M.: SAT-based counterexample guided abstraction refinement. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 1–1. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46017-9_1
Ganty, P., Raskin, J.-F., Van Begin, L.: A complete abstract interpretation framework for coverability properties of WSTS. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 49–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_4
Kaiser, A., Kroening, D., Wahl, T.: Bfc - a widening approach to multi-threaded program verification. http://www.cprover.org/bfc/
Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 500–515. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_35
Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_10
McMillan, K.L.: Interpolation and SAT-Based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_1
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Turoňová, L., Holík, L. (2018). Towards Smaller Invariants for Proving Coverability. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds) Computer Aided Systems Theory – EUROCAST 2017. EUROCAST 2017. Lecture Notes in Computer Science(), vol 10672. Springer, Cham. https://doi.org/10.1007/978-3-319-74727-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-74727-9_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74726-2
Online ISBN: 978-3-319-74727-9
eBook Packages: Computer ScienceComputer Science (R0)