uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Constrained monotonic abstraction: A CEGAR for parameterized verification
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2010 (English)In: CONCUR 2010 – Concurrency Theory, Berlin: Springer-Verlag , 2010, 86-101 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6269
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-130923DOI: 10.1007/978-3-642-15375-4_7ISI: 000285373500007ISBN: 978-3-642-15374-7 (print)OAI: oai:DiVA.org:uu-130923DiVA: diva2:352101
Conference
21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010
Projects
UPMARCautomated verification of highly concurrent algorithms
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2011-04-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Abdulla, Parosh AzizHaziza, FrédéricRezine, Ahmed

Search in DiVA

By author/editor
Abdulla, Parosh AzizHaziza, FrédéricRezine, Ahmed
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 615 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf