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
|