Name:Professor Thomas Melham
Designation:Professor of Computer Science
Title:Effective Validation of Low-Level Firmware

Abstract: Today’s microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware.  These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is required that takes them into account.  This talk explores a new approach to co-validation of hardware/software interfaces by formal, symbolic co-execution of an executable hardware model combined with the software that interacts with it. Biography: Tom Melham is a Professor of Computer Science at the University of Oxfordand a Fellow of Balliol College.  He received his Ph.D. from the Universityof Cambridge in 1990 for his foundational  research in formal hardwareverification and mechanised reasoning. Professor Melham is the author of numerous scientific publications and a regular speaker at international scientific conferences. His research contributions include results in deductive theorem proving; software architectures for formal reasoning tools; software, firmware and hardwareverification; formal modelling of systems; combined model checking andtheorem proving; abstraction techniques; integrating formal verificationinto industrial design methodologies and the foundations of systemsbiology.  He works closely with leading companies in microelectronicsdesign on advanced tools and methods for chip design validation, and serveson the Technical Advisory Board of Jasper Design Automation.

Formal Verification Seminar Presentation                      Recording unavailable at the request of the speaker