{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:23:47Z","timestamp":1773840227398,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,1,13]],"date-time":"2025-01-13T00:00:00Z","timestamp":1736726400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF and ASEE","award":["FA8750-20-C-0156"],"award-info":[{"award-number":["FA8750-20-C-0156"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-22-1-0316 and FA9550-22-1-0333"],"award-info":[{"award-number":["FA9550-22-1-0316 and FA9550-22-1-0333"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2025,1,31]]},"abstract":"<jats:p>Contract-based design is a method to facilitate modular design of systems. While there has been substantial progress on the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this article, 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 illustrate the use of Pacti in a variety of case studies.<\/jats:p>","DOI":"10.1145\/3704736","type":"journal-article","created":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T15:18:32Z","timestamp":1731943112000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7933-692X","authenticated-orcid":false,"given":"Inigo","family":"Incer","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9788-2702","authenticated-orcid":false,"given":"Apurva","family":"Badithela","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1376-0741","authenticated-orcid":false,"given":"Josefine B.","family":"Graebener","sequence":"additional","affiliation":[{"name":"California Institute of Technology, Pasadena, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4438-6107","authenticated-orcid":false,"given":"Piergiuseppe","family":"Mallozzi","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3590-4459","authenticated-orcid":false,"given":"Ayush","family":"Pandey","sequence":"additional","affiliation":[{"name":"University of California, Merced, Merced, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3137-8690","authenticated-orcid":false,"given":"Nicolas","family":"Rouquette","sequence":"additional","affiliation":[{"name":"Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2585-9586","authenticated-orcid":false,"given":"Sheng-Jung","family":"Yu","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3352-4137","authenticated-orcid":false,"given":"Albert","family":"Benveniste","sequence":"additional","affiliation":[{"name":"INRIA\/IRISA Rennes, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3234-5033","authenticated-orcid":false,"given":"Benoit","family":"Caillaud","sequence":"additional","affiliation":[{"name":"INRIA\/IRISA Rennes, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5785-7481","authenticated-orcid":false,"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[{"name":"California Institute of Technology, Pasadena, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1298-8389","authenticated-orcid":false,"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC45484.2021.9683611"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS55552.2023.10342465"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2002.1011427"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1072266"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_34"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.5.463"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693137"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_13"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.818119"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_4"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.2307\/1967869"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0121242"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/bf01583784"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.159701"},{"key":"e_1_3_2_21_2","first-page":"317","article-title":"Solution d\u2019une question particuli\u00e8re du calcul des in\u00e9galit\u00e9s","volume":"99","author":"Fourier Joseph","year":"1826","unstructured":"Joseph Fourier. 1826. Solution d\u2019une question particuli\u00e8re du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des sciences par la Soci\u00e9t\u00e9 philomathique de Paris 99 (1826), 317\u2013319.","journal-title":"Nouveau Bulletin des sciences par la Soci\u00e9t\u00e9 philomathique de Paris"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-021-06120-5"},{"key":"e_1_3_2_23_2","first-page":"117","volume-title":"Principles and Practices of Constraint Programming","author":"Imbert Jean-Louis","year":"1993","unstructured":"Jean-Louis Imbert. 1993. Fourier\u2019s elimination: Which to choose?. In Principles and Practices of Constraint Programming, Vol. 1, Citeseer, 117\u2013129."},{"key":"e_1_3_2_24_2","volume-title":"The Algebra of Contracts","author":"Incer Inigo","year":"2022","unstructured":"Inigo Incer. 2022. The Algebra of Contracts. Ph.D. Dissertation. EECS Department, University of California, Berkeley."},{"key":"e_1_3_2_25_2","unstructured":"Inigo Incer Apurva Badithela Josefine Graebener Piergiuseppe Mallozzi Ayush Pandey Sheng-Jung Yu Albert Benveniste Benoit Caillaud Richard M. Murray Alberto Sangiovanni-Vincentelli et al. 2023. Pacti: Scaling assume-guarantee reasoning for system analysis and design. arXiv:2303.17751. Retrieved from https:\/\/arxiv.org\/abs\/2303.17751"},{"key":"e_1_3_2_26_2","unstructured":"Inigo Incer Albert Benveniste Richard M. Murray Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia. 2023b. Context-aided variable elimination for requirement engineering. arXiv:2305.17596. Retrieved from https:\/\/arxiv.org\/abs\/2305.17596"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_36"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.326.14"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556872"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/0024-3795(85)90271-X"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.1998.655893"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/82.735357"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245296"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"e_1_3_2_35_2","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch Nancy A.","year":"1989","unstructured":"Nancy A. Lynch and Mark R. Tuttle. 1989. An introduction to input\/output automata. CWI Quarterly 2 (1989), 219\u2013246.","journal-title":"CWI Quarterly"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE51338.2020.9315065"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_20"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41589-018-0168-3"},{"key":"e_1_3_2_39_2","volume-title":"Beitr\u00e4ge zur Theorie der linearen Ungleichungen","author":"Motzkin Theodore Samuel","year":"1936","unstructured":"Theodore Samuel Motzkin. 1936. Beitr\u00e4ge zur Theorie der linearen Ungleichungen. Ph.D. Dissertation. University of Basel."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342122"},{"key":"e_1_3_2_41_2","volume-title":"Modeling Frameworks for Modular and Scalable Biological Circuit Design","author":"Pandey Ayush","year":"2024","unstructured":"Ayush Pandey. 2024. Modeling Frameworks for Modular and Scalable Biological Circuit Design. Ph.D. Dissertation. California Institute of Technology."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1021\/acssynbio.2c00534"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358216"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503914"},{"key":"e_1_3_2_45_2","first-page":"III","volume-title":"Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS)","volume":"3","author":"Shi Changchun","year":"2004","unstructured":"Changchun Shi and Robert W. Brodersen. 2004. A perturbation theory on statistical quantization effects in fixed-point DSP with non-stationary inputs. In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS), Vol. 3, IEEE, III\u2013373."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-92124-8_25"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/78.476465"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1287\/mnsc.29.10.1209"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704736","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704736","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:58Z","timestamp":1750295878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704736"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,13]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,1,31]]}},"alternative-id":["10.1145\/3704736"],"URL":"https:\/\/doi.org\/10.1145\/3704736","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,13]]},"assertion":[{"value":"2023-09-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-26","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}