Automated verification of multi-threaded programs requires keeping track of a very large number of possible interactions between the program threads. Different reasoning methods have been proposed that alleviate the explicit enumeration of all thread interleavings, e.g., Lipton's theory of reduction or Owicki-Gries method for compositional reasoning, however their synergistic interplay has not yet been fully explored. In this paper we explore the applicability of the theory of reduction for pruning of equivalent interleavings for the automated verification of multi-threaded programs with infinite-state spaces. We propose proof rules for safety and termination of multi-threaded programs that integrate into an Owicki-Gries based compositional verifier. The verification conditions of our method are Horn clauses, thus facilitating automation by using off-the-shelf Horn clause solvers. We present preliminary experimental results that show the advantages of our approach when compared to state-of-the-art verifiers of C programs.

We present a constraint-based approach to computing winning strategies in two-player graph games over the state space of infinite-state programs. Such games have numerous applications in program verification and synthesis, including the synthesis of infinite-state reactive programs and branching-time verification of infinite-state programs. Our method handles games with winning conditions given by safety, reachability, and general Linear Temporal Logic (LTL) properties. For each property class, we give a deductive proof rule that --- provided a symbolic representation of the game players --- describes a winning strategy for a particular player. Our rules are sound and relatively complete. We show that these rules can be automated by using an off-the-shelf Horn constraint solver that supports existential quantification in clause heads. The practical promise of the rules is demonstrated through several case studies, including a challenging "Cinderella-Stepmother game" that allows infinite alternation of discrete and continuous choices by two players, as well as examples derived from prior work on program repair and synthesis.

Automatically generated tools can significantly improve programmer productivity. For example, parsers and dataflow analyzers can be automatically generated from declarative specifications in the form of grammars, which tremendously simplifies the task of implementing a compiler. In this paper, we present a method for the automatic synthesis of software verification tools. Our synthesis procedure takes as input a description of the employed proof rule, e.g., program safety checking via inductive invariants, and produces a tool that automatically discovers the auxiliary assertions required by the proof rule, e.g., inductive loop invariants and procedure summaries. We rely on a (standard) representation of proof rules using recursive equations over the auxiliary assertions. The discovery of auxiliary assertions, i.e., solving the equations, is based on an iterative process that extrapolates solutions obtained for finitary unrollings of equations. We show how our method synthesizes automatic safety and liveness verifiers for programs with procedures, multi-threaded programs, and functional programs. Our experimental comparison of the resulting verifiers with existing state-of-the-art verification tools confirms the practicality of the approach.

Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment transitions, to enable scalable, compositional reasoning. Once the environment transitions are identified, we can prove program properties by considering each program thread in isolation, as the environment transitions keep track of the interleaving with other threads. Finding adequate environment transitions that are sufficiently precise to yield conclusive results and yet do not overwhelm the verifier with unnecessary details about the interleaving with other threads is a major challenge. In this paper we propose a method for safety verification of multi-threaded programs that applies (transition) predicate abstraction-based discovery of environment transitions, exposing a minimal amount of information about the thread interleaving. The crux of our method is an abstraction refinement procedure that uses recursion-free Horn clauses to declaratively state abstraction refinement queries. Then, the queries are resolved by a corresponding constraint solving algorithm. We present preliminary experimental results for mutual exclusion protocols and multi-threaded device drivers.

Embedded systems are becoming more widely used but these systems are often resource constrained. Programming models for these systems should take into formal consideration resources such as stack and heap. In this paper, we show how memory resource bounds can be inferred for assembly-level programs. Our inference process captures the memory needs of each method in terms of the symbolic values of its parameters. For better precision, we infer path-sensitive information through a novel guarded expression format. Our current proposal relies on a Presburger solver to capture memory requirements symbolically, and to perform fixpoint analysis for loops and recursion. Apart from safety in memory adequacy, our proposal can provide estimate on memory costs for embedded devices and improve performance via fewer runtime checks against memory bound.

Arrays are intensively used in many software programs, including those in the popular graphics and game programming domains. Although the problem of eliminating redundant array bound checks has been studied for a long time, there are few works that attempt to be both aggressively precise and practical. We propose an inference mechanism that achieves both aims by combining a forward relational analysis with a backward precondition derivation. Our inference algorithm works for a core imperative language with assignments, and analyses each method once through a summary-based approach. Our inference is precise as it is both path and context sensitive. Through a novel technique that can strengthen preconditions, we can selectively reduce the sizes of formulae to support a practical inference algorithm. Moreover, we subject each inferred program to a flexivariant specialization that can achieve good tradeoff between elimination of array checks and code explosion concerns. We have proven the soundness of our approach and have also implemented a prototype inference and specialization system. Initial experiments suggest that such a desired system is viable.

10.1145/1167473.1167498

Many software properties can be analysed through a relational size analysis on each function's inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted imperative programs; but it has been elusive for object-based programs. The main challenge is that objects may mutate and they may be aliased. In this paper, we show how safety policies of programs can be analysed by tracking size properties of objects and be enforced by objects' invariants and the preconditions of methods. We propose several new ideas to allow both mutability and sharing of objects, whilst aiming for precision in our analysis. We introduce the concept of size-immutability to facilitate sharing, and also a set of alias controls to track unaliased objects whose size properties may change. We formalise our results through a set of advanced type checking rules for an object-based imperative language. We re-affirm the utility of the proposed type system by showing how a variety of software properties can be automatically verified according to size-inspired safety policies.

We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are captured by annotated types and conditions on invariance and final states. The protocol itself is specified through a set of pre-defined methods, whose pre-condition and post-condition together, enforce the correct temporal usage of each resource type. We design a simple language together with a type system that shows how resource protocol verification can be achieved. We formalise an operational semantics for the language and provide a correctness proof which confirms that well-typed programs conform to the specified protocol of each resource type.

Regularity constraints may be added in the design of compaction filters in two ways, named by us explicit and implicit. Most of the previous work used the explicit approach. We show that the implicit form is much more appropriate in terms of numerical accuracy. We also integrate the implicit approach in the semidefinite programming (SDP) framework, guaranteeing thus global optimality.

This paper presents an algorithm for designing an FIR paraunitary filter bank when one or several filters are given. The algorithm is based on the properties of the balanced state-space representation of the polyphase matrix. We show that this representation may be computed via a single RQ decomposition thus gaining significant efficiency with respect to previous work. Application of the algorithm to signal-adapted filter banks is also discussed.

We propose a new technique for finding the optimum FIR compaction filter adapted to signal statistics. The main novelty of our approach is the transformation of the original problem into the maximum eigenvalue minimization of a parameterized Toeplitz matrix, with only O(N) variables. This is a typical application of semidefinite programming (SDP) and may be solved with reliable interior-point algorithms. Our algorithm is to be compared with the method of Tuqan and Vaidyanathan (1998), which has O(N/sup 2/) variables. The numerical experiments show that the optimum compaction filter is obtained with good numerical accuracy and convenient execution time for filters of order up to 100.