A double operadic approach to assume-guarantee reasoning

Abstract

In this talk, we’ll take a look at the abstract algebra of assume-guarantee reasoning for certifying that coupled dynamical systems satisfy their specs. We’ll take a step back and consider the compositionality of certification in the abstract, and see how to construct loose right modules of certified systems over symmetric monoidal double categories of certified coupling laws.