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
|