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.

Correctness of high-level transformation systems relative to nested conditions

In this paper we introduce the notions of nested constraints and application conditions, short nested conditions. For a category associated with a graphical representation such as graphs, conditions are a graphical and intuitive, yet precise, formalism that is well suited to describing structural properties. We show that nested graph conditions are expressively equivalent to first-order graph formulas. A part of the proof includes transformations between two satisfiability notions of conditions, namely-satisfiability and-satisfiability. We consider a number of transformations on conditions that can be composed to construct constraint-guaranteeing and constraint-preserving application conditions, weakest preconditions and strongest postconditions. The restriction of rule applications by conditions can be used to correct transformation systems by pruning transitions leading to states violating given constraints. Weakest preconditions and strongest postconditions can be used to verify the correctness of transformation systems with respect to pre- and postconditions.