—This paper summarizes our research findings on optimizing the symbolic execution of evolving state machines using incremental analysis. I. PROBLEM AND MOTIVATION Model Driven Engineering (MDE) is a model-centric software engineering approach that aims at improving the productivity and the quality of software artifacts by focusing on models as first-class artifacts in place of code. MDE has been widely used for over a decade in many domains such as automotive and telecommunication industries. Iterativeincremental development and model-based analysis are central to MDE in which artifacts typically undergo several iterations and refinements during their lifetime that may require changes to their initial design versions. As these models evolve, it is necessary to assess their quality by repeating the analysis and the verification of these models after every iteration or refinement. This process, if not optimized, can be very tedious and time consuming. The IBM Rational Rhapsody fra...