Speaker:

Kedar Namjoshi

Abstract:

Consider a program with many (say, N) concurrently active processes, which communicate via shared memory. Algorithmically checking a correctness property on the full state space is often impractical, due to an exponential blowup in the number of global states with increasing values of N.

An alternative is to prove a number of local (per-process) properties, which together imply the desired global property. But: (1) can this always work? (2) can the local properties be chosen algorithmically? and (3) what if N is a parameter? (e.g., mutual exclusion is desired for all values of N.)

The first question was answered affirmatively by Owicki & Gries and Lamport 30 years ago. I will present a simple derivation of their proof method for safety properties, which also results in a fixpoint algorithm to compute the strongest vector of local invariants (a "split-invariant"), providing a solution to (2). Under some technical assumptions, the split invariant computed for small values of N can be generalized to an invariant which holds for all N, providing a partial solution to (3). These methods are particularly applicable to the analysis of multi-threaded programs, where a number of threads communicate through shared memory.

Speaker:

Tomas Vojnar

Abstract:

We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the $\exists^* \forall^*$ first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints as well as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular, using our logic, one can express constraints on consecutive elements of arrays (e.g. $\forall i ~.~ 0 \leq i < n \rightarrow a[i+1]=a[i]-1$) as well as periodic facts (e.g. $\forall i ~.~ i \equiv_2 0 \rightarrow a[i] = 0$). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B\"uchi counter automata such that any model of a formula corresponds to an accepting run of the automaton, and vice versa.

The emptiness problem for this class of counter automata is shown to be decidable, as a consequence of earlier results on counter automata with a flat control structure and transitions based on difference constraints. We show interesting program properties expressible in our logic, and give an example of invariant verification for programs that handle integer arrays.

Joint work with Peter Habermehl and Radu Iosif

Speaker:

Ahmed Bouajjani

Abstract:

We introduce a uniform framework for reasoning about infinite-state systems with unbounded control structures and unbounded data domains. Our framework is based on constrained rewriting systems on words over an infinite alphabet. We consider several rewriting semantics: factor, prefix, and multiset rewriting. Constraints are expressed in a logic on such words which is parametrized by a first-order theory on the considered data domain.

We show that our framework is suitable for reasoning about various classes of systems such as recursive sequential programs, multithreaded programs, parametrized/dynamic networks of processes with counters, etc. Then, we provide generic results (1) for the decidability of the satisfiability problem of the fragment $\exists^*\forall^*$ of this logic provided that the underlying logic on data is decidable, and (2) for proving inductive invariance and for carrying out Hoare style reasoning within this fragment. We also show that the reachability problem if decidable for a class of prefix rewriting systems with integer data.

Joint work with Peter Habermehl, Yan Jurski and Mihaela Sighireanu