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 |
|---|---|
| Přispěvatelé: | 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), Microsoft Research, École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL), Programming securely with cryptography (PROSECCO ), École normale supérieure - Paris (ENS Paris) |
| Rok vydání: | 2017 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Cryptography and Security Computer science Monotonic function 02 engineering and technology Hoare logic computer.software_genre Mathematical proof [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Monad (non-standard analysis) 020204 information systems Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Monotonic-State Monad Safety Risk Reliability and Quality Modular Reasoning Program Verification Soundness [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Computer Science - Programming Languages State Continuity Programming language Formal Foundations ACM: I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE/I.2.2: Automatic Programming/I.2.2.4: Program verification Preorder Monotonic References 020207 software engineering Hoare Logic Data structure Secure File Transfer TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS State (computer science) Cryptography and Security (cs.CR) computer Software Programming Languages (cs.PL) |
| Zdroj: | 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⟩ |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3158153 |
| Popis: | 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. POPL'18 camera ready |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|