Related papers: Towards Bounded Infeasible Code Detection

Control synthesis under constraints is at the forefront of research on autonomous systems, in part due to its broad application from low-level control to high-level planning, where computing control inputs is typically cast as a constrained…

The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical…

We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The…

We develop a new numerical method for approximating the infinite time reachable set of strictly stable linear control systems. By solving a linear program with a constraint that incorporates the system dynamics, we compute a polytope with…

This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time…

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…

Motivated by algorithmic information theory, the problem of program discovery can help find candidates of underlying generative mechanisms of natural and artificial phenomena. The uncomputability of such inverse problem, however,…

The linear programming (LP) approach is, together with value iteration and policy iteration, one of the three fundamental methods to solve optimal control problems in a dynamic programming setting. Despite its simple formulation,…

We introduce a set of eight universal Rules of Inference by which computer programs with known properties (axioms) are transformed into new programs with known properties (theorems). Axioms are presented to formalize a segment of Number…

We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurrence equations with constant coefficients. We turn the task of…

There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these…

We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other…

Intelligent systems sometimes need to infer the probable goals of people, cars, and robots, based on partial observations of their motion. This paper introduces a class of probabilistic programs for formulating and solving these problems.…

Code coverage is a widely used metric for quantifying the extent to which program elements, such as statements or branches, are executed during testing. Calculating code coverage is resource-intensive, requiring code building and execution…

In this paper, we present a domain specific process to assist the verification of observer-based fault detection software. Observer-based fault detection systems, like control systems, yield invariant properties of quadratic types. These…

For multiparametric mixed-integer convex programming problems such as those encountered in hybrid model predictive control, we propose an algorithm for generating a feasible partition of a subset of the parameter space. The result is a…

We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to…

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…

Executing various sequences of system functions in a system under test represents one of the primary techniques in software testing. The natural way to create effective, consistent and efficient test sequences is to model the system under…

One of the first steps in learning how to program is reading and tracing existing code. In order to avoid the error-prone task of generating variations of a tracing exercise, our tool Tatsu generates instances of a given code skeleton…