A Mechanically Verified Theory of Contracts

The work

AuthorsStéphane Kastenbaum; Benoît Boyer; Jean-Pierre Talpin
Editors
Typeinproceedings
Year2021
Citekeykastenbaum2021mechanically

Where it appeared

Published inInternational Colloquium on Theoretical Aspects of Computing (ICTAC)
PublisherSpringer International Publishing
SeriesLecture Notes in Computer Science
Pages134--151

Identifiers

arXiv2108.13647
DOI10.1007/978-3-030-85315-0_9
ISSN0302-9743
ISBN978-3-030-85314-3

Access

Landing pagehttps://doi.org/10.1007/978-3-030-85315-0_9
Free full texthttps://arxiv.org/pdf/2108.13647

Related

Distinct fromdumitrescu2003construction
Distinct fromgaravel2009semantics
Distinct fromkan2026interaction
Distinct fromzuccala2025formal

From crossref.

Abstract

Cyber-physical systems (CPS) are assemblies of networked, heterogeneous, hardware, and software components sensing, evaluating, and actuating a physical environment. This heterogeneity induces complexity that makes CPSs challenging to model correctly. Since CPSs often have critical functions, it is however of utmost importance to formally verify them in order to provide the highest guarantees of safety. Faced with CPS complexity, model abstraction becomes paramount to make verification attainable. To this end, assume/guarantee contracts enable component model abstraction to support a sound, structured, and modular verification process. While abstractions of models by contracts are usually proved sound, none of the related contract frameworks themselves have, to the best of our knowledge, been formally proved correct so far. In this aim, we present the formalization of a generic assume/guarantee contract theory in the proof assistant Coq. We identify and prove theorems that ensure its correctness. Our theory is generic, or parametric, in that it can be instantiated and used with any given logic, in particular hybrid logics, in which highly complex cyber-physical systems can uniformly be described.

A copy is held

pdf, 222.1 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via crossref
Added2026-09-16 14:24 UTC
Approved bya person 2026-10-02 10:03 UTC

Filed under

the-discipline-stops-at-the-edge what-one-proves-with who-checks-the-checker

Cite it as

@inproceedings{kastenbaum2021mechanically,
  title        = {A Mechanically Verified Theory of Contracts},
  author       = {Stéphane Kastenbaum and Benoît Boyer and Jean-Pierre Talpin},
  year         = {2021},
  booktitle    = {International Colloquium on Theoretical Aspects of Computing (ICTAC)},
  publisher    = {Springer International Publishing},
  series       = {Lecture Notes in Computer Science},
  pages        = {134--151},
  isbn         = {978-3-030-85314-3},
  issn         = {0302-9743},
  eprint       = {2108.13647},
  doi          = {10.1007/978-3-030-85315-0_9},
}

This record lives at https://refs.drheap.org/kastenbaum2021mechanically/ and will keep doing so.