Recalling a witness: foundations and applications of monotonic state

Autor: Nikhil Swamy, Aseem Rastogi, Cătălin Hriţcu, Danel Ahman, Cédric Fournet, Kenji Maillard

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), ⟨10.1145/3158153⟩

We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorde

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::96c4ad18cd51e1e9c86681b3b7f880c4