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...
| Hauptverfasser: | , , |
|---|---|
| Weitere Verfasser: | |
| Format: | Conference item |
| Veröffentlicht: |
Springer
2015
|