SemaWare: Rapid Development of High-Performance Program Verifiers by Abstract Interpretation

Classical methods employed for software verification require considerable human effort that limits their application to small critical parts of a system. Abstract Interpretation is a theoretical framework that provides analytic methods and algorithms for automatically discovering valid properties of a program. The basic properties about the program execution discovered by Abstract Interpretation are used in turn to establish safety properties of the system. While Abstract Interpretation is a powerful technology, it will not play a major role in software verification unless the design and development of specialized, practical analyzers can be streamlined in a process accessible to non-computer science specialists. On the human side, this is clear. On the technical side, this owes to the tradeoff among accuracy, analysis scope, and scalability. To push tradeoff curves into economical and practical regions, it would help if many, smaller scope, higher accuracy analyzers could be built, customized for a given application. We propose to formalize this process and to build generators to create the supporting tools that will enable application specialists to specify and generate dedicated high-performance analyzers on demand.