Related papers: Characterization of Termination for Linear Loop Pr…
We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for bounded terminiation (i.e., bounded expected termination…
Modern program verifiers use logic-based encodings of the verification problem that are discharged by a back end reasoning engine. However, instances of such encodings for large programs can quickly overwhelm these back end solvers. Hence,…
While loops are present in virtually all imperative programming languages. They are important both for practical reasons (performing a number of iterations not known in advance) and theoretical reasons (achieving Turing completeness). In…
We propose a trust-region method that solves a sequence of linear integer programs to tackle integer optimal control problems regularized with a total variation penalty. The total variation penalty allows us to prove the existence of…
We consider linear single-path loops of the form \[ \textbf{while} \quad \varphi \quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \] where $\vec{x}$ is a vector of variables, the loop guard $\varphi$ is a…
We propose an early termination technique for mixed integer conic programming for use within branch-and-bound based solvers. Our approach generalizes previous early termination results for ADMM-based solvers to a broader class of…
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our…
Given a generic semidefinite program, specified by matrices with rational entries, each coordinate of its optimal solution is an algebraic number. We study the degree of the minimal polynomials of these algebraic numbers. Geometrically,…
Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a…
A method of embedding partially ordered sets into linear spaces is presented. The problem of finding all orthocomplementations in a finite lattice is reduced to a linear programming problem.
This paper studies the problem of testing whether a system of linear equality and inequality constraints admits a solution when the coefficients of that system may have to be estimated. We show that a wide range of inferential questions in…
We present a new characterization of termination of general logic programs. Most existing termination analysis approaches rely on some static information about the structure of the source code of a logic program, such as modes/types,…
In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as…
Termination properties of actual Prolog systems with constraints are fragile and difficult to analyse. The lack of the occurs-check, moded and overloaded arithmetical evaluation via is/2 and the occasional nontermination of finite domain…
The completely bounded trace and spectral norms in finite dimensions are shown to be expressible by semidefinite programs. This provides an efficient method by which these norms may be both calculated and verified, and gives alternate…
Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial…
In this paper, we investigate finite representations of DatalogMTL models. First, we discuss sufficient conditions for detecting programs that have finite models. Then, we study infinite models that eventually become constant and introduce…
We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of…
The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear…
We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover,…