Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. However, the state-space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. Even in the case of purely sequential programs, a crucial requirement to make predicate abstraction effective is to use as few predicates as possible. This is because, in the worst case, the state-space of the abstraction generated (and consequently the time and memory complexity of the abstraction process) is exponential in the number of predicates involved. In addition, for concurrent programs, the number of reachable states could grow exponentially with the number of components. We attempt to address these issues in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (predicate abstraction for data and action-guided abstraction for events) within a counterexample-guided abstraction refinement scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Additionally, a key feature of our approach is that if a property can be proved to hold or not hold based on a given finite set of predicates $\mathcal{P}$ , the predicate refinement procedure we propose in this article finds automatically a minimal subset of $\mathcal{P}$ that is sufficient for the proof. This, along with our explicit use of compositionality, delays the onset of state-space explosion for as long as possible. We describe our approach in detail, and report on some very encouraging experimental results obtained with our tool MAGIC.     

Tight Bounds for Distributed Minimum-Weight Spanning Tree Verification

This paper introduces the notion of distributed verification without preprocessing. It focuses on the Minimum-weight Spanning Tree (MST) verification problem and establishes tight upper and lower bounds for the time and message complexities of this problem. Specifically, we provide an MST verification algorithm that achieves simultaneously $\tilde{O}(m)$ messages and $\tilde{O}(\sqrt{n} + D)$ time, where m is the number of edges in the given graph G, n is the number of nodes, and D is G’s diameter. On the other hand, we show that any MST verification algorithm must send $\tilde{\varOmega}(m)$ messages and incur $\tilde{\varOmega}(\sqrt{n} + D)$ time in worst case. Our upper bound result appears to indicate that the verification of an MST may be easier than its construction, since for MST construction, both lower bounds of $\tilde{\varOmega}(m)$ messages and $\tilde{\varOmega}(\sqrt{n} + D)$ time hold, but at the moment there is no known distributed algorithm that constructs an MST and achieves simultaneously $\tilde{O}(m)$ messages and $\tilde{O}(\sqrt{n} + D)$ time. Specifically, the best known time-optimal algorithm (using ${\tilde{O}}(\sqrt {n} + D)$ time) requires O(m+n ^3/2) messages, and the best known message-optimal algorithm (using ${\tilde{O}}(m)$ messages) requires O(n) time. On the other hand, our lower bound results indicate that the verification of an MST is not significantly easier than its construction.     

On the limits of refinement-testing for model-checking CSP

Refinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates. By adopting Clarkson and Schneider’s hyperproperties framework, we show that every refinement-closed denotational predicate of finitely-nondeterministic, divergence-free CSP processes can be written as the conjunction of a safety predicate and the refinement-closure of a liveness predicate. We prove that every safety predicate is refinement-closed and that the safety predicates correspond precisely to the CSP refinement checks in finite linear observations models whose left-hand sides (i.e. specification processes) are independent of the systems to which they are applied. We then show that there exist important liveness predicates whose refinement-closures cannot be expressed as refinement checks in any finite linear observations model ${\mathcal{M}}$ , divergence-strict model ${\mathcal{M}^\Downarrow}$ or non-divergence-strict divergence-recording model ${\mathcal{M}^\#}$ , i.e. in any standard CSP model suitable for reasoning about the kinds of processes that FDR can handle, namely finitely-branching ones. These liveness predicates include liveness properties under intuitive fairness assumptions, branching-time liveness predicates and non-causation predicates for reasoning about authority. We conclude that alternative verification approaches, besides refinement-checking, currently under development for CSP should be further pursued.     

Near-Linear Approximation Algorithms for Geometric Hitting Sets

Given a range space $(X,\mathcal{R})$ , where $\mathcal{R}\subset2^{X}$ , the hitting set problem is to find a smallest-cardinality subset H?X that intersects each set in $\mathcal{R}$ . We present near-linear-time approximation algorithms for the hitting set problem in the following geometric settings: (i)? $\mathcal{R}$ is a set of planar regions with small union complexity. (ii)? $\mathcal{R}$ is a set of axis-parallel d-dimensional boxes in ? ^d . In both cases X is either the entire ? ^d , or a finite set of points in ? ^d . The approximation factors yielded by the algorithm are small; they are either the same as, or within very small factors off the best factors known to be computable in polynomial time.     

A k-Median Algorithm with Running Time Independent of Data Size

We give a sampling-based algorithm for the k-Median problem, with running time O(k $(\frac{{k^2 }}{ \in } \log k)^2 $ log $(\frac{k}{ \in } \log k)$ ), where k is the desired number of clusters and ∈ is a confidence parameter. This is the first k-Median algorithm with fully polynomial running time that is independent of n, the size of the data set. It gives a solution that is, with high probability, an O(1)-approximation, if each cluster in some optimal solution has Ω $(\frac{{n \in }}{k})$ points. We also give weakly-polynomial-time algorithms for this problem and a relaxed version of k-Median in which a small fraction of outliers can be excluded. We give near-matching lower bounds showing that this assumption about cluster size is necessary. We also present a related algorithm for finding a clustering that excludes a small number of outliers.     

On matrices, automata, and double counting in constraint programming

Matrix models are ubiquitous for constraint problems. Many such problems have a matrix of variables $\mathcal{M}$ , with the same constraint C defined by a finite-state automaton $\mathcal{A}$ on each row of $\mathcal{M}$ and a global cardinality constraint $\mathit{gcc}$ on each column of $\mathcal{M}$ . We give two methods for deriving, by double counting, necessary conditions on the cardinality variables of the $\mathit{gcc}$ constraints from the automaton $\mathcal{A}$ . The first method yields linear necessary conditions and simple arithmetic constraints. The second method introduces the cardinality automaton, which abstracts the overall behaviour of all the row automata and can be encoded by a set of linear constraints. We also provide a domain consistency filtering algorithm for the conjunction of lexicographic ordering constraints between adjacent rows of $\mathcal{M}$ and (possibly different) automaton constraints on the rows. We evaluate the impact of our methods in terms of runtime and search effort on a large set of nurse rostering problem instances.     

A unified approximate reasoning theory suitable for both propositional calculus system \mathcal{L}^* and predicate calculus system \mathcal{K}^*

The concepts of metric R ₀-algebra and Hilbert cube of type R ₀ are introduced. A unified approximate reasoning theory in propositional caculus system $\mathcal{L}^* $ and predicate calculus system $\mathcal{K}^* $ is established semantically as well as syntactically, and a unified complete theorem is obtained.     

Model selection in reinforcement learning

We consider the problem of model selection in the batch (offline, non-interactive) reinforcement learning setting when the goal is to find an action-value function with the smallest Bellman error among a countable set of candidates functions. We propose a complexity regularization-based model selection algorithm, $\ensuremath{\mbox{\textsc {BErMin}}}$ , and prove that it enjoys an oracle-like property: the estimator??s error differs from that of an oracle, who selects the candidate with the minimum Bellman error, by only a constant factor and a small remainder term that vanishes at a parametric rate as the number of samples increases. As an application, we consider a problem when the true action-value function belongs to an unknown member of a nested sequence of function spaces. We show that under some additional technical conditions $\ensuremath{\mbox{\textsc {BErMin}}}$ leads to a procedure whose rate of convergence, up to a constant factor, matches that of an oracle who knows which of the nested function spaces the true action-value function belongs to, i.e., the procedure achieves adaptivity.     

Partition Into Triangles on Bounded Degree Graphs

We consider the Partition Into Triangles problem on bounded degree graphs. We show that this problem is polynomial-time solvable on graphs of maximum degree three by giving a linear-time algorithm. We also show that this problem becomes $\mathcal{NP}$ -complete on graphs of maximum degree four. Moreover, we show that there is no subexponential-time algorithm for this problem on graphs of maximum degree four unless the Exponential-Time Hypothesis fails. However, the Partition Into Triangles problem on graphs of maximum degree at most four is in many cases practically solvable as we give an algorithm for this problem that runs in $\mathcal{O}(1.02220^{n})$ time and linear space.