Formal Verification: Can we move beyond academic toys to practitioners' tools?

Abstract: Software verification was originally advocated as a panacea for all programming ills. Although it greatly influenced programming language design, from structured programming to object oriented, it has never succeeded as a widely used technique. In this talk I will first explore why distributed systems make formal verification more important than ever. I will then describe FLAVERS, a finite state verification tool that builds upon efficient data flow analysis techniques. With FLAVERS, practitioners can form queries about important safety properties of their system and either receive assurances that the properties can never be violated by any execution of the system or be shown traces where such violations might occur. We believe that FLAVERS can bridge the gulf between the mathematical sophistication required for formal verification and the capabilities and time constraints of practicing software engineers. Our goal is to hide the "formal" in formal verification, yet provide powerful reasoning tools that can deal with complex, distributed systems.

Biography: Lori A. Clarke received a B.A. degree in mathematics from the University of Rochester and a Ph.D. degree in Computer Science from the University of Colorado. She joined the Computer Science faculty at the University of Massachusetts, Amherst in 1975 where she has continued to pursue research on a broad range of software engineering issues including verification of distributed systems and distributed object technology.