Related papers: On the Monniaux Problem in Abstract Interpretation
We show that the problem of determining the existence of an inductive invariant in the language of quantifier free linear integer arithmetic (QFLIA) is undecidable, even for transition systems and safety properties expressed in QFLIA.
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…
Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties.For numerical properties, a classical class of invariants is convex polyhedra: solution sets of system of linear…
Decidability and synthesis of inductive invariants ranging in a given domain play an important role in many software and hardware verification systems. We consider here inductive invariants belonging to an abstract domain $A$ as defined in…
We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary…
We consider the decidability of state-to-state reachability in linear time-invariant control systems over discrete time. We analyse this problem with respect to the allowable control sets, which in general are assumed to be defined by…
We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification…
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…
One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is…
We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyse this problem with respect to the allowable control sets, which are assumed to be the image under a linear…
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…
Termination analysis of linear loops plays a key r\^{o}le in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination…
The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the…
We consider the problem of determining, given x, y in Z^k and a finite set F of affine functions on Z^k, whether y is reachable from x by applying the functions F. We also consider the analogous problem over N^k. These problems are known to…
An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compiler optimization, and program verification. While simple, the…
We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century. While the…
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for…
When the inverse of an algorithm is well-defined -- that is, when its output can be deterministically transformed into the input producing it -- we say that the algorithm is invertible. While one can describe an invertible algorithm using a…
We establish the undecidability of conditional affine information inequalities, the undecidability of the conditional independence implication problem with a constraint that one random variable is binary, and the undecidability of the…
The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant…