CAREER: Fast Provers for Extended Static Checking of Software

University Of Iowa, Iowa City IA

Investigators

Abstract

ABSTRACT 0237422 Cesare Tinelli Univ of Iowa The unifying research and education theme of this project is improving the reliability of software by cost-effective automated reasoning techniques and tools. The project concentrates on extended static checking (ESC), a powerful form of static checking aimed at detecting insidious run-time errors such as null-dereferencing and out-of-bounds errors. Because of its limited goal of just uncovering as many run-time errors as possible, ESC is easier to automate effectively than full software verification. However, its wide adoption is presently hindered by the low speed of existing checkers. The overall research objective of this project is to develop new automated reasoning techniques and tools for ESC, with the expectation that they will make ESC an attractive and cost-effective technology for software development. Routine use of ESC will help uncover more errors during the debugging phase of the software life cycle, leading to a more reliable final product. The overall education objective of the project is to expose students to specification/verification techniques and tools that have proved effective with real-word problems. A new generation of professionals better prepared and predisposed to the use of these tools will facilitate their adoption by the software industry, making it possible for our society to reap the benefits of more reliable software.