Name
Abstract | ||
|---|---|---|
This paper proposes a framework for detecting termination of programs handling infinite and complex data domains, such as
pointer structures. In this framework, the user has to specify a finite number of well-founded relations on the data domain
manipulated by these programs. Our tool then builds an initial abstraction of the program, which is checked for existence
of potential infinite runs, by testing emptiness of its intersection with a predefined Büchi automaton. If the intersection
is non-empty, a lasso-shaped counterexample is found. This counterexample is checked for spuriousness by a domain-specific
procedure, and in case it is found to be spurious, the abstraction is refined, again by intersection with the complement of
the Büchi automaton representing the lasso. We have instantiated the framework for programs handling tree-like data structures,
which allowed us to prove termination of programs such as the depth-first tree traversal, the Deutsch-Schorr-Waite tree traversal,
or the linking leaves algorithm.
|
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-02979-0_20 | Computing and Informatics |
Keywords | Field | DocType |
automata-based termination proofs,data domain,lasso-shaped counterexample,depth-first tree traversal,chi automaton,deutsch-schorr-waite tree traversal,complex data domain,predefined b,potential infinite,initial abstraction,tree-like data structure,complex data,data structure | Pointer (computer programming),Data structure,Tree traversal,Programming language,Data domain,Automaton,Theoretical computer science,Tree automaton,Counterexample,Mathematics,Büchi automaton | Journal |
Volume | Issue | ISSN |
32 | 4 | 1335-9150 |
Citations | PageRank | References |
2 | 0.41 | 15 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Radu Iosif | 1 | 483 | 42.44 |
| Adam Rogalewicz | 2 | 153 | 9.39 |