L773:0925 9856 OR L773:1572 8102
Sökning: L773:0925 9856 OR L773:1572 8102 > Ranking function sy...
LIBRIS Formathandbok (Information om MARC21)
| 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 |
Hitta via bibliotek
- Formal methods in system design (Sök värdpublikationen i LIBRIS)
Till lärosätets databas
Hitta mer i SwePub
- Av författaren/redakt...
- Cook, Byron
- Kroening, Daniel
- Rümmer, Philipp
- Wintersteiger, C ...
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- Artiklar i publikationen
- Formal methods i ...
- Av lärosätet
- Uppsala universitet
Sök utanför SwePub
- Sök vidare i:
- 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 - Nationella bibliotekssystem
- LIBRIS.kb.se
