liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Lazy Constrained Monotonic Abstraction
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
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)
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online)
Keyword [en]
Constrained monotonic abstraction, Lazy exploration, Well structured systems, Safety properties, Counter machines reachability
National Category
Computer Science
Identifiers
URN: 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
Conference
17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016
Available from: 2016-01-11 Created: 2016-01-11 Last updated: 2016-06-20Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Ganjei, ZeinabRezine, AhmedEles, PetruPeng, Zebo
By organisation
Software and SystemsFaculty of Science & EngineeringThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 611 hits
ReferencesLink to record
Permanent link

Direct link