Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTermination Analysis of Programs with Multiphase Control-Flow
136
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Jesus J. Domenech
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $Pi^0_2$-complete. We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.
The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions - including the constraints on supermartingales - of a proof rule. Our software tool Amber can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.
We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the best of our knowledge, the considered family of MPPs is hitherto the largest one for which termination is decidable. We present an explicit recursive function which is essentially Ackermannian, to compute the maximal length of ascending chains of polynomial ideals under a control function, and thereby obtain a complete answer to the questions raised by Seidenberg. This maximal length facilitates a precise complexity analysis of our algorithms for computing the NTI and deciding termination of MPPs. We extend our method to programs with polynomial guarded commands and show how an incomplete procedure for MPPs with inequality guards can be obtained. An application of our techniques to invariant generation of polynomial programs is further presented.
We extend a technique called Compiling Control. The technique transforms coroutining logic programs into logic programs that, when executed under the standard left-to-right selection rule (and not using any delay features) have the same computational behavior as the coroutining program. In recent work, we revised Compiling Control and reformulated it as an instance of Abstract Conjunctive Partial Deduction. This work was mostly focused on the program analysis performed in Compiling Control. In the current paper, we focus on the synthesis of the transformed program. Instead of synthesizing a new logic program, we synthesize a CHR(Prolog) program which mimics the coroutining program. The synthesis to CHR yields programs containing only simplification rules, which are particularly amenable to certain static analysis techniques. The programs are also more concise and readable and can be ported to CHR implementations embedded in other languages than Prolog.
The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gamblers Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
