uu.seUppsala universitets publikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet 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)
Vise andre og tillknytning
2016 (engelsk)Inngår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, nr 4, s. 357-385Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
2016. Vol. 53, nr 4, s. 357-385
HSV kategori
Identifikatorer
URN: urn:nbn:se:uu:diva-295451DOI: 10.1007/s00236-015-0235-0ISI: 000376978100003OAI: oai:DiVA.org:uu-295451DiVA, id: diva2:933735
Prosjekter
ProFuNUPMARC
Forskningsfinansiär
Swedish Foundation for Strategic Research Tilgjengelig fra: 2015-05-07 Laget: 2016-06-07 Sist oppdatert: 2018-01-10bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Personposter BETA

Abdulla, Parosh AzizHolík, LukásJonsson, BengtTrinh, Cong Quy

Søk i DiVA

Av forfatter/redaktør
Abdulla, Parosh AzizHolík, LukásJonsson, BengtTrinh, Cong Quy
Av organisasjonen
I samme tidsskrift
Acta Informatica

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 579 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf