Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design
Inigo Incer, Apurva Badithela, Josefine B. Graebener, Piergiuseppe Mallozzi, Ayush Pandey, Sheng-Jung Yu, Albert Benveniste, Benoı̂t Caillaud, Richard M. Murray, Alberto Luigi Sangiovanni-Vincentelli, Sanjit A. Seshia · arXiv (Cornell University) · 2023
Contract-based design is a method to facilitate modular system design. While there has been substantial progress on the theory of contracts, there has been less progress on scalable algorithms for the algebraic operations in this theory. In this paper, we present: 1) principles to implement a contract-based design tool at scale and 2) Pacti, a tool that can efficiently compute these operations. We then illustrate the use of Pacti in a variety of case studies.