Computer Science Colloquia
April 24, 2012
Advisor: John Knight
Attending Faculty: Jack Davidson, Chair; David Evans; Westley Weimer; and Joanne Bechta Dugan, Minor representative
2:30 PM, Rice Hall, Rm. 242
Ph.D. Dissertation Presentation
Echo: Practical Formal Verification by Reverse Synthesis
Current approaches to formal verification are powerful but not sufficiently practical. Verification techniques are difficult and time-consuming to apply, tools are of limited capabilities and cannot be integrated, and the process requires high levels of expertise. Current approaches also impose limitations on developers that make it difficult to fit formal verification into the existing development cycle.
To address these problems, I develop a practical and effective approach to formal verification of the functional correctness of computer software. My approach, named Echo, relies upon and incorporates a number of powerful existing notations, tools and techniques, and distributes the verification burden over separate levels. At the core of the approach is a process called reverse synthesis in which semantic-preserving transformations are applied on the software implementation to reduce the verification complexity, and in which a high-level abstract specification is synthesized mechanically from the software source code documented with a low-level, detailed specification to support the verification.
This new approach to analysis alleviates the verification difficulty by separating the verification proofs, introducing a scalable proof structure, and exploiting automated reasoning and program transformation to increase the practicality. It dovetails with standard development processes more easily than existing approaches to formal verification. In effect, verification in Echo proceeds in a direction opposite to that of traditional verification approaches. Relatively few limitations are imposed on developers and many existing software engineering development methods can continue to be used, yet formal verification and all of its benefits can be applied.
In addition, when combined with other types of analysis such as run-time checks, Echo increases the expressive power of formal verification, allowing whole-system assurance arguments to be constructed for richer properties.