Model and proof generation for heap-manipulating programs
Existing heap analysis techniques lack the ability to supply counterexamples in case of property violations. This hinders diagnosis, prevents test-case generation and is a barrier to the use of these tools among non-experts. We present a verification technique for reasoning about aliasing and reacha...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2014
|