Dr. Ting Zhang, Assistant Professor of Computer Science, has received an NSF CAREER Grant for his project on advanced decision procedures for words, trees, and lists.
The NSF Faculty Early Career Development (CAREER) Program is a Foundation-wide activity that offers the NSF's most prestigious awards in support of junior faculty who exemplify the role of teacher-scholars through outstanding research, excellent education and the integration of education and research within the context of the mission of their organizations.
Project Title: CAREER: Advanced Decision Procedures for Words, Trees, and Lists
Project Description: 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.