Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Constrained monotonic abstraction: A CEGAR for parameterized verification
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Visa övriga samt affilieringar
2010 (Engelska)Ingår i: CONCUR 2010 – Concurrency Theory, Berlin: Springer-Verlag , 2010, 86-101 s.Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Berlin: Springer-Verlag , 2010. 86-101 s.
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6269
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:uu:diva-130923DOI: 10.1007/978-3-642-15375-4_7ISI: 000285373500007ISBN: 978-3-642-15374-7 (tryckt)OAI: oai:DiVA.org:uu-130923DiVA: diva2:352101
Konferens
21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010
Projekt
UPMARCautomated verification of highly concurrent algorithms
Tillgänglig från: 2010-09-17 Skapad: 2010-09-17 Senast uppdaterad: 2011-04-07Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Abdulla, Parosh AzizHaziza, FrédéricRezine, Ahmed
Av organisationen
Datorteknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

Altmetricpoäng

Totalt: 602 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf