The Next 700 Separation Logics
VSTTE'10: Proceedings of the Third international conference on Verified software: theories, tools, experiments(2010)
摘要
In recent years, separation logic has brought great advances in the world of verification. However, there is a disturbing trend for each new library or concurrency primitive to require a new separation logic. I will argue that. we shouldn't be inventing new separation logics, but should find the right logic to reason about interference, and have a powerful abstraction mechanism to enable the library's implementation details to be correctly abstracted. Adding new concurrency libraries should simply be a matter of verification, not of new logics or metatheory.
更多查看译文
关键词
Shared State, Language Feature, Separation Logic, Garbage Collector, Abstract Data Type
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络