Synthesising interprocedural bit-precise termination proofs
Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities such as denial-of-service attacks. To make termination checks scale to large systems, interprocedural termination analysis seems essential, which is a large...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
IEEE
2016
|