Termination Analysis of Programs with Multiphase Control-Flow
| Autor: | Jesús J. Doménech, Samir Genaim |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Horn clause Control flow Theoretical computer science Computer Science - Programming Languages Termination analysis Computer science Partial evaluation Ranking (information retrieval) Programming Languages (cs.PL) Logic in Computer Science (cs.LO) |
| DOI: | 10.48550/arxiv.2109.04630 |
| Popis: | Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions. Comment: In Proceedings HCVS 2021, arXiv:2109.03988 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|