Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design
Logic in Computer Science
2024-11-22 v1 Systems and Control
Systems and Control
Abstract
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.
Cite
@article{arxiv.2303.17751,
title = {Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design},
author = {Inigo Incer and Apurva Badithela and Josefine Graebener and Piergiuseppe Mallozzi and Ayush Pandey and Sheng-Jung Yu and Albert Benveniste and Benoit Caillaud and Richard M. Murray and Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:2303.17751},
year = {2024}
}