Stratified Guarded First-Order Transition Systems

First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of first-order variables, or the number of required instances of input predicates remains bounded, or the number of occurring negated literals decreases in every iteration. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed.

Filtering False Alarms for Static Detection of Array Bounds Violation via Weakest Precondition

Array bounds violations are a bane of programming in most languages. Static analysis provides a powerful approach to detect such bugs, but it always suffers high rate of false alarms. We propose a local, demand-driven approach based on weakest preconditions propagation to filter false alarms for static detection of array bounds violations. A concrete example is presented to show that our method is effective.