Name
Abstract | ||
|---|---|---|
Termination of a heap-manipulating program generally de- pends on preconditions that are heap assumptions (i.e., assertions de- scribing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The al- gorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis pro- duces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our pro- totypical implementation indicate its practical potential. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-70545-1_31 | Computer Aided Verification |
Keywords | Field | DocType |
abstract computation,heap assumptions,abstract termination checker,express heap assumption,heap assumption,shape analysis,prototype implementation,unique interplay,heap-manipulating program,practical potential | Programming language,Computer science,Inference,Algorithm,Theoretical computer science,Reachability,Heap (data structure),Binary heap,Counterexample,Binomial heap,Shape analysis (digital geometry),Computation | Conference |
Volume | ISSN | Citations |
5123 | 0302-9743 | 13 |
PageRank | References | Authors |
0.85 | 19 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Podelski | 1 | 2760 | 197.87 |
| Andrey Rybalchenko | 2 | 1439 | 68.53 |
| Thomas Wies | 3 | 515 | 28.26 |