Hypercontracts

Sanjit A. Seshia Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli. Hypercontracts. In Proceedings of the 14th NASA Formal Methods Symposium (NFM), pp. 674–692, June 2022.

Download

[pdf] 

Abstract

Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. We propose hypercontracts, a general model with a richer structure for its underlying model of components, subsuming simulation preorders. While general, the new model provides a richer algebra for its notions of refinement, parallel composition, and quotient. Further, it allows the introduction of new operations. Building on top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description.

BibTeX

@inproceedings{incer-nfm22,
  author    = {Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia},
  title     = {Hypercontracts},
 booktitle = {Proceedings of the 14th NASA Formal Methods Symposium (NFM)},
 month = "June",
 year = {2022},
 pages = {674--692},
 abstract = {Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. We propose hypercontracts, a general model with a richer structure for its underlying model of components, subsuming simulation preorders. While general, the new model provides a richer algebra for its notions of refinement, parallel composition, and quotient. Further, it allows the introduction of new operations. Building on top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description.},
}