Techniques for finding faults in software systems, such as crashes, security vulnerabilities, and deadlocks, have become increasingly powerful over the past two decades. This is due in no small part to the development of efficient automated satisfiability solvers. The interest in applying these solvers to an ever wider class of software analysis applications has pushed solvers to their limits. As a result, analysis developers are currently forced to approximate analysis?s queries to make use of existing solvers. Because of this software analyses can mistakenly diagnose an error, miss reporting a true error, and suffer unnecessarily poor performance. This research seeks to establish accuracy as an important missing dimension of solver support and its success will lead to broader and more cost-effective use of solvers to produce high-quality software.
This project is the first to systematically explore and link the accuracy requirements of a software analysis to the accuracy provided by a solver. This project does this by exploring approaches to specify the accuracy requirements of solver clients and detect, recover and report solution accuracy for integer and string constraints. These capabilities are being implemented in an existing solver interface framework, called Green, which is applied to perform symbolic execution of Java programs, using Symbolic Pathfinder. The project will evaluate the extent to this approach simplifies client analysis development, enables clients to use a variety of solvers - even those that do not perfectly match accuracy requirements, and improves analysis performance.
