Effective Validation of Firmware

Modern processors comprise an increasing amount of software to simplify in product design. The complex interplay of hardware and software, including concurrent operations, together with rapid growth in size of this software, makes it ever more susceptible undetected design and implementation errors. This is in stark contrast to the reliability requirements, as all applications and devices running on top of the processor depend on its correct operation.

The project consortium includes the University of British Columbia, Princeton University, and Rice University. The goal of this project is the development of automated validation techniques for low-level software that interacts closely with hardware components, e.g., to minimise the power consumption of a processor. The project covers a broad range of topics including the following: 

• hardware/software modelling,
• automated generation of models using machine learning techniques,
• automated software verification for C/C++/SystemC and low-level assembler,
• concurrency
• new programming languages and type systems, especially for resource usage and environment modelling.

The project will cover both theoretical foundations and the implementation of prototype software tools.