Deterministic Pruning of Program Analysis Tree with Abstraction Learning
Dr Joxan Jaffar, Emeritus Professor, School of Computing
COM1 Level 2
SR7, COM1-02-07
Abstract:
Program Analysis is fundamental problem in Computer Science. Algorithms for program analysis problem often involve complete consideration of program's computation tree. Such tree, however, has worst-case rate of growth exponential to program size, in O(2^n). This makes a straightforward one-by-one consideration of the tree nodes impractical.
This seminar presents a general mechanism of pruning computation trees - abstraction learning. Along with the usual tree traversal, from root to leaves, this mechanism attempts to capture the relationship between the considered nodes in the tree and the answer the program analysis procedure is trying to provide. Once we backtrack from a subtree and switch to another unvisited subtree, the similarity (as defined according to the concrete analysis) between visited subtrees and the forthcoming subtree is examined. If the similarity alone implies the visit of the forthcoming subtree will have the same contribution to the analysis outcome as the visited subtrees, then the forthcoming subtree can safely be pruned without any impact on the soundness and completeness.
With the general idea of abstraction learning presented, we further present two its effective specializations: concurrency verification and probabilistic program inference.
The concurrency verification specialization has the ability to capture the relationship between process interleavings and the safety of the program, for which, allows the irrelevant interleaving subtrees to be soundly pruned. Akin to partial order reduction, but our pruning criteria is more relaxed than the equality of resulting states required by partial order reduction, resulting in more interleavings prunable.
The Probabilistic program inference problem infers the probability of outcomes of probabilistic models that are encoded in the form of programs. Our probabilistic inference specialization has the ability to capture the relationship between the execution context and the resulting probability, for which, allows the probability of the subtrees to be taken into account without the full-blown traversal of them.
Both have been shown to outperform the well-known methods in their respective fields.
This seminar will focus mostly on their high-level ideas. The basic background of concurrency verification and probabilistic program will be briefly provided, with the basic knowledge in program analysis expected.