Computers, be it those in mobile phones or servers, are increasingly being designed with heterogeneous processors and memory that is shared across all of these processors. The heterogeneity enables greater performance, with different processors tailored for specific purposes (e.g., graphics), and the shared memory facilitates easier programming. These processors are already being used to support critical computational tasks, including artificial intelligence (AI), robotics, and medical research. While these processors offer great potential, they pose two problems. First, it is difficult to understand how to compose them. Specifically, different types of processors use different communication protocols, and composing these protocols is complicated. Second, it is also challenging to verify that the processors will behave correctly in all situations. The composed protocols have a vast number of possible interactions, and verification techniques do not scale up to meet this challenge. This project addresses both challenges by developing a systematic way to compose processor protocols and a new, scalable technique for verification of these processors. These contributions can offer many benefits, including shorter time to market, confidence that processors will behave as expected, and a lower barrier to entry for startups and researchers seeking to create new processors. By providing a foundation for the correct design of heterogeneous shared memory processors, the project will hel