Lazy Constrained Monotonic Abstraction
Verification, Model Checking, and Abstract Interpretation (VMCAI) ,Florida, USA, 17-19 Jan. 2016
ABSTRACT
We propose the first reachability techniques for lazily performing constrained monotonic abstraction (lazy CMA for short). CMA makes use of possibly infinite abstractions that are well structured 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 well structured systems based analysis techniques. In this paper, we consistently improve on the existing eager 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.
[GREP16] Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng, "Lazy Constrained Monotonic Abstraction", Verification, Model Checking, and Abstract Interpretation (VMCAI) ,Florida, USA, 17-19 Jan. 2016 |
|
