Vitamin C: A Deductive Framework for Generating Analyzers for C Programs

Utah State University, Logan UT

Investigators

Abstract

0702600 Vitamin C: A Framework for Generating Analyzers for C Programs Jerry James This project intends to increase the level of confidence in software systems deployed in mission-critical environments by providing a comprehensive platform for analyzing various aspects of software correctness. More precisely, it focuses on developing a deductive program transformation framework for automatically generating specialized analyzers for C programs in an aspect-oriented way. In contrast with code analyzers that take arbitrary programs as input, this research will show how to synthesize a code analyzer that is specialized to the program under analysis and the correctness aspect under consideration. Such specialization will open up new vistas for making code analyzers more efficient than is currently possible, as well as providing a platform for experimenting with different program analysis algorithms. The project will lead to the development of a deductive framework for a new class of modal logics. In addition, it will lead to a study of the application of partial evaluation and program transformation techniques for generating efficient program analyzers suited to particular analysis problems. The results of this project will be used to aid open source developers in analyzing their software projects, and to introduce students to mathematically rigorous techniques for reasoning about the correctness of software.