CAREER: Fast Provers for Extended Static Checking of Software

点击翻译按钮获取中文摘要

ABSTRACT0237422Cesare TinelliUniv of IowaThe 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 extendedstatic 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 uncoveringas 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 professionalsbetter 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.