Constrained monotonic abstraction: A CEGAR for parameterized verification
2010 (English)In: CONCUR 2010 – Concurrency Theory, Berlin: Springer-Verlag , 2010, 86-101 p.Conference paper (Refereed)
In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterexamples Our CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a "Safety Zone" and uses it to refine the abstract transition system of the next iteration We have developed a prototype based on this idea, and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.
Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2010. 86-101 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 6269
IdentifiersURN: urn:nbn:se:uu:diva-130923DOI: 10.1007/978-3-642-15375-4_7ISI: 000285373500007ISBN: 978-3-642-15374-7OAI: oai:DiVA.org:uu-130923DiVA: diva2:352101
21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010
ProjectsUPMARCautomated verification of highly concurrent algorithms