CAREER: Improving Scalability of Finite State Verifiers

Polytechnic University Of New York, Brooklyn NY

Investigators

Abstract

CCR-0093174 CAREER: Improving Scalability of Finite State Verifiers Software quality assurance is a critically important and expensive task. Finite State verification (FSV) is a family of automated approaches for proving that a given software system does not have errors of a specified kind of exposing such errors if they exist. Unfortunately, computing resources needed by FSV techniques are often prohibitive for systems of realistic size, impeding acceptance of FSV in software practice. This research is aimed at improving scalability of FSV techniques. It seeks to generalize the existing optimizations beyond the scope of the FSV techniques for which these optimizations were originally proposed. In addition, new optimization techniques are being developed. The research evaluates, both analytically and experimentally, the impact of each optimization on the scalability of the FSV techniques to which it can be applied. Successful completion of this work will produce scalable and effective SFV techniques. In turn, use of these techniques in software practice can result in improvements in software quality and reduction in software development costs. In addition, case studies with large software systems performed in the course of this work provide valuable experience in applying FSV techniques to real systems in form of guidelines and heuristics.