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
|