Principles of program verification for arbitrary monadic effects

Autor: Kenji Maillard
Přispěvatelé: Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Programming securely with cryptography (PROSECCO ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris sciences et lettres, Cătălin Hriţcu, Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Programming securely with cryptography (PROSECCO), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Université Paris sciences et lettres (PSL), ENS Paris - Ecole Normale Supérieure de Paris, STAR, ABES
Jazyk: angličtina
Rok vydání: 2019
Předmět:
Zdroj: Programming Languages [cs.PL]. Université Paris sciences et lettres, 2019. English. ⟨NNT : 2019PSLEE081⟩
Computer Science [cs]. ENS Paris-Ecole Normale Supérieure de Paris, 2019. English
HAL
Popis: Computational monads are a convenient algebraic gadget to uniformly represent side-effects in programming languages, such as mutable state, divergence, exceptions, or non-determinism. Various frameworks for specifying programs and proving that they meet their specification have been proposed that are specific to a particular combination of side-effects. For instance, one can use Hoare logic to verify the functional correctness of programs with mutable state with respect to pre/post-conditions specifications, which are predicates on states. The goal of this thesis is to devise a principled semantic framework for verifying programs with arbitrary monadic effects in a generic way with respect to such rich specifications. One additional challenge is supporting various interpretations of effects, for instance total vs partial correctness, or angelic vs demonic nondeterminism. Finally, the framework should also accommodate relational verification, for properties such as program equivalence.
Les effets de bord présent dans les langages de programmation tel que l'état mutable, la divergence ou le non-déterminisme sont capturés de manière élégante par des monades. Plusieurs systèmes ont été proposés pour spécifier et prouver que des programmes manipulant une certaine combinaison d'effets respectent leur spécification. Par exemple, la logique de Hoare permet de vérifier la correction de programmes manipulant la mémoire en stipulant des prédicats sur les états initiaux et finaux. Le but de cette thèse est de définir un cadre sémantique générique pour vérifier que des programmes avec des effets monadique arbitraire respectent de telles spécifications. Les interprétations diverses des effets tels que la correction totale ou partielle, ou encore le non-déterminisme angélique ou démonique, introduisent un défi supplémentaire. Ce cadre sémantique devra aussi considérer la vérification de propriétés relationnelles, par exemple la simulation ou l'équivalence de programmes.
Databáze: OpenAIRE
Externí odkaz: