Cited By
View all- Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022
Symbolic execution as a basis for termination analysis
Pages 142 - 157
Abstract
We present a high-level, language-independent approach to semantics-based termination analysis.Our formulation is useful for understanding the key ingredients and may provide useful insights for designing new tools.The main concepts are illustrated with an imperative and a functional language, so they are accessible to a broader audience. Program termination is a relevant property that has been extensively studied in the context of many different formalisms and programming languages. Traditional approaches to proving termination are usually based on inspecting the source code. Recently, a new semantics-based approach has emerged, which typically follows a two-stage scheme: first, a finite data structure representing the computation space of the program is built; then, termination is analyzed by inspecting the transitions in this data structure using traditional, syntax-based techniques.Unfortunately, this approach is still specific to a programming language and semantics. In this work, we present instead a general, high-level framework that follows the semantics-based approach to proving termination. In particular, we focus on the first stage and advocate the use of symbolic execution, together with appropriate subsumption and abstraction operators, for producing a finite representation of the computations of a program. Hopefully, this higher level approach will provide useful insights for designing new semantics-based termination tools for particular programming languages.
References
[1]
Annual international termination competition. http://www.termination-portal.org/wiki/Termination_Competition
[2]
E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, D. Zanardini, Termination analysis of Java bytecode, in: Lecture Notes in Computer Science, vol. 5051, Springer, 2008, pp. 2-18.
[3]
E. Albert, P. Arenas, S. Genaim, G. Puebla, D. Zanardini, COSTA: design and implementation of a cost and termination analyzer for Java bytecode, in: Lecture Notes in Computer Science, vol. 5382, Springer, 2008, pp. 113-132.
[4]
E. Albert, G. Vidal, The narrowing-driven approach to functional logic program specialization, New Gener. Comput., 20 (2002) 3-26.
[5]
S. Anand, C.S. Pasareanu, W. Visser, Symbolic execution with abstract subsumption checking, in: Lecture Notes in Computer Science, vol. 3925, Springer, 2006, pp. 163-181.
[6]
S. Anand, C.S. Pasareanu, W. Visser, Symbolic execution with abstraction, Int. J. Softw. Tools Technol. Transf., 11 (2009) 53-67.
[7]
T. Arts, J. Giesl, Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236 (2000) 133-178.
[8]
F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.
[9]
M. Brockschmidt, C. Otto, J. Giesl, Modular termination proofs of recursive Java bytecode programs by term rewriting, in: LIPIcs, vol. 10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011, pp. 155-170.
[10]
M. Brockschmidt, C. Otto, C. von Essen, J. Giesl, Termination graphs for Java bytecode, in: Lecture Notes in Computer Science, vol. 6463, Springer, 2010, pp. 17-37.
[11]
L. Clarke, A program testing system, in: Proceedings of the 1976 Annual Conference (ACM'76), 1976, pp. 488-491.
[12]
M. Colón, H. Sipma, Synthesis of linear ranking functions, in: Lecture Notes on Computer Science, vol. 2031, Springer, 2001, pp. 67-81.
[13]
M. Colón, H. Sipma, Practical methods for proving program termination, in: Lecture Notes on Computer Science, vol. 2404, Springer, 2004, pp. 442-454.
[14]
B. Cook, A. Podelski, A. Rybalchenko, Proving program termination, Commun. ACM, 54 (2011) 88-98.
[15]
P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. of Fourth ACM Symp. on Principles of Programming Languages, 1977, pp. 238-252.
[16]
P. Cousot, R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper, in: Lecture Notes in Computer Science, vol. 631, Springer-Verlag, Berlin, Germany, 1992, pp. 269-295.
[17]
D. De Schreye, S. Decorte, Termination of logic programs: the never-ending story, J. Log. Program., 19/20 (1994) 199-260.
[18]
N. Dershowitz, Termination of rewriting, J. Symb. Comput., 3 (1987) 69-115.
[19]
N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Elsevier, Amsterdam, 1990, pp. 243-320.
[20]
S. Falke, D. Kapur, C. Sinz, Termination analysis of C programs using compiler intermediate languages, in: LIPIcs, vol. 10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011, pp. 41-50.
[21]
J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, R. Thiemann, Automated termination proofs for Haskell by term rewriting, ACM Trans. Program. Lang. Syst., 33 (2011) 7.
[22]
J. Giesl, P. Schneider-Kamp, R. Thiemann, AProVE 1.2: automatic termination proofs in the dependency pair framework, in: Lecture Notes on Computer Science, vol. 4130, Springer, 2006, pp. 281-286.
[23]
J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, C. Fuhs, Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs, in: PPDP'12, ACM, 2012, pp. 1-12.
[24]
M. Heizmann, J. Hoenicke, J. Leike, A. Podelski, Linear ranking for linear lasso programs, in: Lecture Notes on Computer Science, vol. 8172, Springer, 2013, pp. 365-380.
[25]
T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, Lazy abstraction, in: Proc. of POPL, 2002, pp. 58-70.
[26]
J.C. King, Symbolic execution and program testing, Commun. ACM, 19 (1976) 385-394.
[27]
J. Kruskal, Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture, Trans. Am. Math. Soc., 95 (1960) 210-225.
[28]
C. Lee, N. Jones, A. Ben-Amram, The size-change principle for program termination, SIGPLAN Not., 28 (2001) 81-92.
[29]
M. Leuschel, Homeomorphic embedding for online termination of symbolic methods, in: Lecture Notes on Computer Science, vol. 2566, Springer, 2002, pp. 379-403.
[30]
M. Leuschel, B. Martens, D. De Schreye, Controlling generalization and polyvariance in partial deduction of normal logic programs, ACM Trans. Program. Lang. Syst., 20 (1998) 208-258.
[31]
J. Lloyd, Foundations of Logic Programming, Springer-Verlag, Berlin, 1987.
[32]
J. Lloyd, J. Shepherdson, Partial evaluation in logic programming, J. Log. Program., 11 (1991) 217-242.
[33]
Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems - Safety, Springer, 1995.
[34]
B. Martens, J. Gallagher, Ensuring global termination of partial deduction while allowing flexible polyvariance, in: Proc. of ICLP'95, MIT Press, 1995, pp. 597-611.
[35]
N. Nishida, G. Vidal, Termination of narrowing via termination of rewriting, Appl. Algebra Eng. Commun. Comput., 21 (2010) 177-225.
[36]
C. Otto, M. Brockschmidt, C. von Essen, J. Giesl, Automated termination analysis of Java bytecode by term rewriting, in: LIPIcs, vol. 6, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010, pp. 259-276.
[37]
G. Plotkin, Building-in equational theories, Mach. Intell., 7 (1972) 73-90.
[38]
A. Podelski, A. Rybalchenko, A complete method for the synthesis of linear ranking functions, in: Lecture Notes on Computer Science, vol. 2937, Springer, 2004, pp. 239-251.
[39]
A. Podelski, A. Rybalchenko, Transition invariants, in: Proc. of LICS'04, IEEE Computer Society, 2004, pp. 32-41.
[40]
A. Podelski, A. Rybalchenko, Transition predicate abstraction and fair termination, ACM Trans. Program. Lang. Syst. 29 (3).
[41]
F. Ramsey, On a problem of formal logic, in: Proc. of the London Mathematical Society, vol. 30, 1930, pp. 264-286.
[42]
P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, R. Thiemann, Automated termination analysis for logic programs with cut, Theory Pract. Log. Program., 10 (2010) 365-381.
[43]
F. Spoto, F. Mesnard, É. Payet, A termination analyzer for Java bytecode based on path-length, ACM Trans. Program. Lang. Syst., 32 (2010).
[44]
G. Stix, Send in the terminator. A Microsoft tool looks for programs that freeze up, Sci. Am., 295 (2006) 37.
[45]
Terese, Term Rewriting Systems, Cambridge University Press, 2003.
[46]
G. Vidal, Termination of narrowing in left-linear constructor systems, in: Lecture Notes on Computer Science, vol. 4989, Springer, 2008, pp. 113-129.
[47]
G. Vidal, Closed symbolic execution for verifying program termination, in: Proc. of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2012), IEEE, 2012, pp. 34-43. http://users.dsic.upv.es/~gvidal
- Symbolic execution as a basis for termination analysis
Recommendations
Closed Symbolic Execution for Verifying Program Termination
SCAM '12: Proceedings of the 2012 IEEE 12th International Working Conference on Source Code Analysis and ManipulationSymbolic execution, originally introduced as a method for program testing and debugging, is usually incomplete because of infinite symbolic execution paths. In this work, we adapt some well-known notions from partial evaluation in order to have a ...
Symbolic execution based on language transformation
We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is generated, with the same ...
Symbolic types for lenient symbolic execution
We present lambda_sym, a typed λ-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V.
Publisher
Elsevier North-Holland, Inc.
United States
Publication History
Published: 01 May 2015
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
Cited By
View all- Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022