Ranking function synthesis for bit-vector relations
Ranking function synthesis is a key aspect to the success of modern termination provers for imperative programs. While it is wellknown how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers...
| Main Authors: | , , , |
|---|---|
| 其他作者: | |
| 格式: | Conference item |
| 出版: |
Springer
2010
|