Ranking function synthesis for bit-vector relations
<p style="text-align:justify;">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...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Published: |
Springer
2013
|
| _version_ | 1826283265024065536 |
|---|---|
| author | Cook, B Kroening, D Rummer, P al., E |
| author_facet | Cook, B Kroening, D Rummer, P al., E |
| author_sort | Cook, B |
| collection | OXFORD |
| description | <p style="text-align:justify;">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.</p> |
| first_indexed | 2024-03-07T00:56:18Z |
| format | Journal article |
| id | oxford-uuid:8834480e-7b99-49a6-b269-277116cc2b44 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:56:18Z |
| publishDate | 2013 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:8834480e-7b99-49a6-b269-277116cc2b442022-03-26T22:15:31ZRanking function synthesis for bit-vector relationsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:8834480e-7b99-49a6-b269-277116cc2b44Symplectic Elements at OxfordSpringer2013Cook, BKroening, DRummer, Pal., E<p style="text-align:justify;">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.</p> |
| spellingShingle | Cook, B Kroening, D Rummer, P al., E Ranking function synthesis for bit-vector relations |
| title | Ranking function synthesis for bit-vector relations |
| title_full | Ranking function synthesis for bit-vector relations |
| title_fullStr | Ranking function synthesis for bit-vector relations |
| title_full_unstemmed | Ranking function synthesis for bit-vector relations |
| title_short | Ranking function synthesis for bit-vector relations |
| title_sort | ranking function synthesis for bit vector relations |
| work_keys_str_mv | AT cookb rankingfunctionsynthesisforbitvectorrelations AT kroeningd rankingfunctionsynthesisforbitvectorrelations AT rummerp rankingfunctionsynthesisforbitvectorrelations AT ale rankingfunctionsynthesisforbitvectorrelations |