Modular verification of programs with effects and effects handlers - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Article Dans Une Revue Formal Aspects of Computing Année : 2020

Modular verification of programs with effects and effects handlers

Résumé

Modern computing systems have grown in complexity, and even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. Inconsistencies between components’ assumptions on the rest of the system can have significant repercussions on this system, and may ultimately lead to safety or security issues. In this article, we introduce FreeSpec, a formalismbuilt upon the key idea that components can bemodeled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modeling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.

Mots clés

Fichier non déposé

Dates et versions

hal-03107526 , version 1 (12-01-2021)

Identifiants

Citer

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet. Modular verification of programs with effects and effects handlers. Formal Aspects of Computing, 2020, ⟨10.1007/s00165-020-00523-2⟩. ⟨hal-03107526⟩
114 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More