Sökning: onr:"swepub:oai:DiVA.org:uu-204769" > Ranking function sy...
Fältnamn | Indikatorer | Metadata |
---|---|---|
000 | 02333naa a2200385 4500 | |
001 | oai:DiVA.org:uu-204769 | |
003 | SwePub | |
008 | 130812s2013 | |||||||||||000 ||eng| | |
024 | 7 | a https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-2047692 URI |
024 | 7 | a https://doi.org/10.1007/s10703-013-0186-42 DOI |
040 | a (SwePub)uu | |
041 | a engb eng | |
042 | 9 SwePub | |
072 | 7 | a ref2 swepub-contenttype |
072 | 7 | a art2 swepub-publicationtype |
100 | 1 | a Cook, Byron4 aut |
245 | 1 0 | a Ranking function synthesis for bit-vector relations |
264 | c 2013-03-21 | |
264 | 1 | b Springer Science and Business Media LLC,c 2013 |
338 | a print2 rdacarrier | |
520 | a 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. | |
650 | 7 | a NATURVETENSKAPx Data- och informationsvetenskap0 (SwePub)1022 hsv//swe |
650 | 7 | a NATURAL SCIENCESx Computer and Information Sciences0 (SwePub)1022 hsv//eng |
653 | a Software verification | |
653 | a Ranking functions | |
653 | a Termination | |
653 | a Bit-vectors | |
700 | 1 | a Kroening, Daniel4 aut |
700 | 1 | a Rümmer, Philippu Uppsala universitet,Datorteknik4 aut0 (Swepub:uu)phiru321 |
700 | 1 | a Wintersteiger, Christoph M.4 aut |
710 | 2 | a Uppsala universitetb Datorteknik4 org |
773 | 0 | t Formal methods in system designd : Springer Science and Business Media LLCg 43:1, s. 93-120q 43:1<93-120x 0925-9856x 1572-8102 |
856 | 4 | u http://www.winterstiger.at/christoph/papers/ckrw10.pdf |
856 | 4 8 | u https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-204769 |
856 | 4 8 | u https://doi.org/10.1007/s10703-013-0186-4 |
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.