Ä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
Verification of heap manipulating programs with ordered data by extended forest automata
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Algorithmic Program 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. (Algorithmic Program Verification)
Visa övriga samt affilieringar
2016 (Engelska)Ingår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, nr 4, 357-385 s.Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.

Ort, förlag, år, upplaga, sidor
2016. Vol. 53, nr 4, 357-385 s.
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:uu:diva-295451DOI: 10.1007/s00236-015-0235-0ISI: 000376978100003OAI: oai:DiVA.org:uu-295451DiVA: diva2:933735
Projekt
ProFuNUPMARC
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF)
Tillgänglig från: 2015-05-07 Skapad: 2016-06-07 Senast uppdaterad: 2016-07-11Bibliografiskt 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 AzizHolík, LukásJonsson, BengtTrinh, Cong Quy
Av organisationen
Datorteknik
I samma tidskrift
Acta Informatica
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

Altmetricpoäng

Totalt: 256 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