A Case for Behavior-Preserving Actions in Separation Logic
Abstract elided by the publisher.
Related papers
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities TACAS 2020
- Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach ICFP 2025
- The type discipline of behavioral separation POPL 2013
- The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic CPP 2025
- Proof-Directed Parallelization Synthesis by Separation Logic TOPLAS 2013
- Simuliris: a separation logic framework for verifying concurrent program optimizations POPL 2022
- Cosmo: a concurrent separation logic for multicore OCaml ICFP 2020
- Behavior trees in action: a study of robotics applications SLE 2020