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.