Dr. Clarke has worked in the area of software engineering, particularly on software
analysis and testing for many years. She was one of the primary developers of symbolic
execution, a technique used to reason about the behavior of software systems and for
selecting test data, and made contributions in the areas of software architecture and
object management. Recently her work has focused on analysis of concurrent systems. With
colleagues, she has developed FLAVERS, a static analysis tool that uses data-flow
analysis techniques to verify user-specified properties. FLAVERS automatically creates a
concise, but perhaps imprecise, model of the software system and then allows users to
selectively improve the accuracy of the program model as needed to improve the accuracy
of the results. The PROPEL system complements FLAVERS, and other event-based finite-state
verification systems, by helping users elucidate the details of the properties to be
proven. FLAVERS allows users to simultaneously view and construct properties from
templates of English language phrases or finite-state automata. The long-term goal is to
develop techniques that well-trained software engineers can use to improve the quality of
software systems.

Other

PDF

Improving the Accuracy of Petri Net-based Analysis of Concurrent Programs (with A. T. Chamillard), Computer Science Department Faculty Publication Series (1996)

Spurious results are an inherent problem of most static analysis methods. These methods, in an...