Lazy Constrained Monotonic Abstraction
2016 (English)In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings / [ed] Barbara Jobstmann; K. Rustan M. Leino, Springer Berlin/Heidelberg, 2016, Vol. 9583, 147-165 p.Conference paper (Refereed)
We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016. Vol. 9583, 147-165 p.
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online)
Constrained monotonic abstraction, Lazy exploration, Well structured systems, Safety properties, Counter machines reachability
IdentifiersURN: urn:nbn:se:liu:diva-123739DOI: 10.1007/978-3-662-49122-5_7ISI: 000375148800007ISBN: 9783662491218 (print)ISBN: 9783662491225 (online)OAI: oai:DiVA.org:liu-123739DiVA: diva2:892797
17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016