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
|