# Some Algebraic Aspects of Assume-Guarantee Reasoning

arXiv: https://arxiv.org/abs/2309.08875 · HTML: https://mlsanity.com/paper/2309.08875/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Sep 2023.

## Built on by (most cited first, 1 of 1)

- [ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems](https://mlsanity.com/paper/2511.02164/) (2025)

## Abstract (arXiv)

We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra -- and the mappings between such structures. We discuss the actions of a Boolean algebra on its contract algebra.