Recalling a witness: foundations and applications of monotonic state

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 preorder, and (2) the property is preserved by this preor...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2018-01, Vol.2 (POPL), p.1-30
Main Authors: Ahman, Danel, Fournet, Cédric, Hriţcu, Cătălin, Maillard, Kenji, Rastogi, Aseem, Swamy, Nikhil
Format: Article
Language:English
Subjects:
Computer Science
Cryptography and Security
Programming Languages
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 preorder, and (2) the property is preserved by this preorder. In many scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the monotonic-state monad , a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F ⋆ verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.
ISSN:2475-1421
2475-1421
DOI:10.1145/3158153