As complex computer systems become ever more pervasive in our society, especially with the increasing deployment of multi-core processors and clusters of servers in the nation's cyber infrastructure, the demand to advance techniques on program analysis and verification has ever been more intensive. Logic-based reasoning techniques have played a fundamental role in assurance of correctness, reliability and security of computer systems. These techniques divide into two categories: general-purpose theorem proving and specialized decision algorithms. Theorem provers, enjoying a high degree of inference completeness, can prove sophisticated properties but require human guidance in general. On the other hand, decision algorithms, though confined within specialized domains, can automatically discharge a large amount of constraints. It has long been a challenge to combine the merits of the two kinds of techniques to produce a new generation of analysis tools that can handle a wide range of constraints with a high degree of automation. This research is to answer this challenge by building powerful decision theories as well as practical tools for reasoning about high-level data structures that are widely used in advanced programming languages and algorithms. The results would have wide and immediate applications in system analysis, improving the precision and scope of static and runtime analysis techniques.
