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...
| المؤلفون الرئيسيون: | , , , |
|---|---|
| مؤلفون آخرون: | |
| التنسيق: | Conference item |
| منشور في: |
Springer
2010
|