A major effort in our center focuses on embedded and autonomous systems. We would like to create a new generation of formal verification tools that can be integrated into design environments for the development of complex, high-assurance embedded and autonomous systems. Embedded systems are increasingly distributed, complex dynamic systems that must operate with a high degree of autonomy and survivability in diverse and unpredictable environments. Our focus is on inventing new verification methods and tools to provide a rigorous means for checking the integrity and correctness of designs for these systems. Our initiative has three broad research thrusts: