Propositional reasoning about safety and termination of heap-manipulating programs
This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we p...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2015
|