Abstract: Microcode is used to facilitate new technologies in Intel CPU designs. A critical requirement is that new designs be backwardly compatible with legacy code when new functionalities are disabled. Several features distinguish microcode from other software systems, such as: interaction with the external environment, sensitivity to exceptions, and the complexity of instructions. The talk will describe the ideas behind Microformal, a technology for fully automated formal verification of functional backward compatibility of microcode.

Lenore Zuck is an associate professor at the University of Illinois at Chicago. Her background is in formal methods. Her recent work includes methodologies for automatic verification of infinite-state systems and translation validation of optimizing compilers and microcode. Lenore has recently moved to UIC from NYU. Before that, she was on the Computer Science faculty at Yale University. Lenore holds a PhD in Computer Science from the Weizmann Institute of Science.