L773:0925 9856 OR L773:1572 8102
Search: L773:0925 9856 OR L773:1572 8102 > Ranking function sy...
- 9 of 21
- Previous record
- Next record
- To hitlist
- Cook, Byron (author)
Ranking function synthesis for bit-vector relations
- Article/chapterEnglish2013
Publisher, publication year, extent ...
- 2013-03-21
- Springer Science and Business Media LLC,2013
- printrdacarrier
Numbers
- LIBRIS-ID:oai:DiVA.org:uu-204769
- https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-204769URI
- https://doi.org/10.1007/s10703-013-0186-4DOI
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers (bit-vectors) is an open problem. This is particularly relevant for the verification of low-level code. We propose several novel algorithms to generate ranking functions for relations over machine integers: a complete method based on a reduction to Presburger arithmetic, and a template-matching approach for predefined classes of ranking functions based on reduction to SAT- and QBF-solving. The utility of our algorithms is demonstrated on examples drawn from Windows device drivers.
Subject headings and genre
- NATURVETENSKAP Data- och informationsvetenskap hsv//swe
- NATURAL SCIENCES Computer and Information Sciences hsv//eng
- Software verification
- Ranking functions
- Termination
- Bit-vectors
Added entries (persons, corporate bodies, meetings, titles ...)
- Kroening, Daniel (author)
- Rümmer, PhilippUppsala universitet,Datorteknik(Swepub:uu)phiru321 (author)
- Wintersteiger, Christoph M. (author)
- Uppsala universitetDatorteknik (creator_code:org_t)
Related titles
- In:Formal methods in system design: Springer Science and Business Media LLC43:1, s. 93-1200925-98561572-8102
Internet link
Find in a library
- Formal methods in system design (Search for host publication in LIBRIS)
To the university's database
- 9 of 21
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Cook, Byron
- Kroening, Daniel
- Rümmer, Philipp
- Wintersteiger, C ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- Articles in the publication
- Formal methods i ...
- By the university
- Uppsala University
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
