SMT-based Formal Unit Testing

Kestrel Technology proposes to develop a system for automated unit testing based on formal methods, including SMT solving. The system will build on Kestrel's powerful underlying formal methods tools but will provide an interface usable by developers with little or no formal methods training. Developers will be able to specify desired program properties in a convenient language. Each property will represent a desired behavior of the program for a particular (potentially very large) set of inputs. By contrast, traditional unit tests cover only a small set of concrete inputs. Our tool will then translate both the properties and the program itself into a formal representation (an SMT formula) and will then call an SMT solver to attempt to prove or disprove the properties. Helpful feedback will be presented to the user. Under the hood, our tool will build on Kestrel's capabilities for lifting code into logic with (our Axe tool, developed under several DARPA programs), our existing connections to SMT solvers, and our existing prototype tool for answering questions about code. We will focus on making these tools more usable and automatic. For usability and convenience, the formal unit testing tool will be integrated into a popular IDE.