The growing role of software in civic infrastructure and the potentially huge costs of software failure make dependable software a pressing need. Technology for developing dependable software will be vital to the US economy in the coming decades.
This project is developing a new approach for checking software to ensure that it has the desired high-level properties. In industry, two techniques are widely used: testing, which cannot achieve sufficient coverage to find the defects responsible for low-probability failures, and static analysis (such as type checking), which can typically handle only very limited properties, such as the absence of certain kinds of overflow or exception. In research, there has been a renewed interest in deeper techniques that are capable of finding the most subtle defects and thus dramatically increasing the developer's confidence in the correctness of the code. Unfortunately, these have tended not be scalable, since they often require more resources (either in computation or in human effort) than is economical. This project is exploring a new approach that promises both depth and scalability, in which a program is checked not for every possible case (which seems to lead to scalability problems), but rather for every case within some finite bounds. The key idea is to generate a logical formula (representing the behaviours of the code), and to present it with a similar formula (characterizing failure to satisfy a required property) to a constraint solver, which then uses powerful search techniques to explore a huge space of potential executions for those that would result in failures.
