PI: Madhusudan Parthasarathy Correct programs are hard to write. Tools that find errors automatically and reliably are essential to ensure engineering of correct software. Automata theory has had a great impact in hardware verification, where it forms the basis of model-checking systems against temporal logics. This project leverages automata-theoretic methods to the field of software verification. Automata theory provides several strikingly new mechanisms for verifying software, including handling of complex control flows of recursion and concurrency, and bridging logical specifications to verification algorithms. The project will develop these mechanisms and apply them to solve key problems in the following areas of software verification: - Developing temporal logics for specifying complex event sequence properties of recursive programs; - Checking atomicity violations in concurrent programs using automata-based monitoring; and - Verifying heap properties of programs manipulating dynamic data, using a novel automata based abstraction. In addition, two tools will be developed: one monitors concurrent programs for atomicity violations, and the second implements an abstraction framework to verify heap-intensive programs. The techniques developed will pave innovative pathways into the fundamental problems of analyzing software. The techniques will have immediate impact on analysis tools built and used in the software industry, and significantly advance the landscape of software verification.
