利用条件写入领域生成依赖-保证条件
Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
AI总结：
本文提出一种条件写入领域结构，用于生成依赖-保证条件，以提高并发程序验证的效率和模块化程度。
摘要：
抽象解释已被证明是并发程序线程模块验证的有前景的技术。其核心在于生成干扰，以依赖-保证条件的形式，符合用户所选择的结构。在本工作中，我们引入了一种称为条件写入领域的结构，适用于仅需建立特定变量由每个线程写入的条件的程序。我们将在一种新的抽象解释框架内正式化我们的分析，该框架高度模块化，可以轻松扩展以捕捉其他依赖-保证条件的结构。我们正式化了我们方法的两个版本，并在一种简单的编程语言上评估了它们的实现。
英文摘要：
Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
