Related papers: (Un)Solvable Loop Analysis
The dynamics of many systems from physics, economics, chemistry, and biology can be modelled through polynomial functions. In this paper, we provide a computational means to find positively invariant sets of polynomial dynamical systems by…
Many correct-by-construction control synthesis methods suffer from the curse of dimensionality. Motivated by this challenge, we seek to reduce a correct-by-construction control synthesis problem to subproblems of more modest dimension. As a…
The analysis of infeasible subproblems plays an import role in solving mixed integer programs (MIPs) and is implemented in most major MIP solvers. There are two fundamentally different concepts to generate valid global constraints from…
This paper deals with the computation of polytopic invariant sets for polynomial dynamical systems. An invariant set of a dynamical system is a subset of the state space such that if the state of the system belongs to the set at a given…
We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning. Loops pose the main difficulty in this setting: even if exact Bayesian inference is possible,…
A program invariant is a property that holds for every execution of the program. Recent work suggest to infer likely-only invariants, via dynamic analysis. A likely invariant is a property that holds for some executions but is not…
A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such…
We describe the LoopInvGen tool for generating loop invariants that can provably guarantee correctness of a program with respect to a given specification. LoopInvGen is an efficient implementation of the inference technique originally…
Recent results in control systems and numerical integration literature utilize invariant set theory to lift dynamical systems evolving on nonlinear manifolds to those evolving on vector spaces. We leverage this technique to propose an…
We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a…
When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stopping theorem in order to infer…
We introduce the concept of structured synthesis for Markov decision processes where the structure is induced from finitely many pre-specified options for a system configuration. The resulting synthesis problem is in general a nonlinear…
The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was…
We present a new method for inferring complexity properties for a class of programs in the form of flowcharts annotated with loop information. Specifically, our method can (soundly and completely) decide if computed values are polynomially…
Funnel synthesis refers to a procedure for synthesizing a time-varying controlled invariant set and an associated control law around a nominal trajectory. The computation of the funnel involves solving a continuous-time differential…
Debugging is difficult. Recent studies show that automatic bug localization techniques have limited usefulness. One of the reasons is that programmers typically have to understand why the program fails before fixing it. In this work, we aim…
We study possibilities for automated invariant generation in parametric systems. We use (a refinement of) an algorithm for symbol elimination in theory extensions to devise a method for iteratively strengthening certain classes of safety…
Naive approaches to amortized inference in probabilistic programs with unbounded loops can produce estimators with infinite variance. This is particularly true of importance sampling inference in programs that explicitly include rejection…
Program synthesis has seen many new applications in recent years, in large part thanks to the introduction of SyGuS. However, no existing SyGuS solvers have support for synthesizing recursive functions. We introduce an multi-phase algorithm…
We present an algorithm to find invariant poynomial transformations of integer sequences, using the classical invariant theory approach.