| Abstract | This research proposes and evaluates techniques for selecting predicates for conditional program properties\,–-\,that is, implications such as $p \Rightarrow q$ whose consequent is true only when the predicate is true. Conditional properties are prevalent in recursive data structures, which behave differently in their base and recursive cases, and in many other situations. The experimental context of the research is dynamic detection of likely program invariants, but the ideas should also be applicable to other domains. \par It is computationally infeasible to try every possible predicate for conditional properties, so we compare procedure return analysis, static analysis, clustering, random selection, and context-sensitive analysis for selecting predicates. \par Even a simple static analysis is fairly effective, presumably because many of the important properties of a program are tested or expressed by programmers. However, important properties are implicit in the program's code or execution. We give examples of important properties discovered by each of the other analyses. We experimentally evaluate the techniques on two tasks: statically proving the absence of run-time errors with a theorem-prover, and detecting errors by separating erroneous from correct executions. We show that the techniques improve performance on both tasks, and we evaluate their costs. |
