Related papers: On Deciding Constant Runtime of Linear Loops
This paper performs the analysis necessary to bound the running time of known, efficient algorithms for generating all longest common subsequences. That is, we bound the running time as a function of input size for algorithms with time…
Existential rules, long known as tuple-generating dependencies in database theory, have been intensively studied in the last decade as a powerful formalism to represent ontological knowledge in the context of ontology-based query answering.…
Temporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications is mostly limited to formulas without quantifier…
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (\emph{e.g.}, non-reachability) specification $\varphi$, and an abstract domain of invariants…
Autonomous systems embedded with machine learning modules often rely on deep neural networks for classifying different objects of interest in the environment or different actions or strategies to take for the system. Due to the…
The Levy Walk is the process with continuous sample paths which arises from consecutive linear motions of i.i.d. lengths with i.i.d. directions. Assuming speed 1 and motions in the domain of beta-stable attraction, we prove functional limit…
Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model in advance. It is particularly useful for partially…
In previous work we describe a novel approach to dependent typing based on a multivalued term language. In this technical report we formalise the runtime, a kind of operational semantics, for that language. We describe a fairly…
The papers~\cite{hatfimmokomi11} and~\cite{azizbrilharr13} propose algorithms for testing whether the choice function induced by a (strict) preference list of length $N$ over a universe $U$ is substitutable. The running time of these…
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to…
We show that, for all reasonable functions $T(n)=o(n\log n)$, we can algorithmically verify whether a given one-tape Turing machine runs in time at most $T(n)$. This is a tight bound on the order of growth for the function $T$ because we…
We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is simple in the sense that loop body semantics need to…
Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment…
This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on…
The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure termination (AST), while also providing quantitative answers…
Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also…
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.…
We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational…
Interrupts have been widely used in safety-critical computer systems to handle outside stimuli and interact with the hardware, but reasoning about interrupt-driven software remains a difficult task. Although a number of static verification…
This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by quantifier-free difference bounds arithmetic. We start by…