Unrestricted termination and non-termination arguments for bit-vector programs
Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking functions over mathemat...
| Κύριοι συγγραφείς: | , , |
|---|---|
| Άλλοι συγγραφείς: | |
| Μορφή: | Conference item |
| Έκδοση: |
Springer
2015
|