A logic and decision procedure for verification of heap-manipulating programs
Heap-manipulating programs (HMPs), which manipulate unbounded linked data structures via pointers, are a major frontier for formal verification of software. Formal verification is the process of proving (or disproving) the correctness of a system with respect to some kind of formal specification or...
| Main Author: | |
|---|---|
| Language: | English |
| Published: |
2010
|
| Online Access: | http://hdl.handle.net/2429/18130 |