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.

翻译：抽象解释已被证明是并发程序线程模块化验证的一种有前景的技术。其核心在于生成符合用户选定结构的干扰条件，这些条件以依赖-保证条件的形式呈现。本文提出了一种称为条件写入域的结构，该结构专为以下程序设计：仅需确定每个线程在何种条件下会写入特定变量即可完成验证。我们在一种新颖的抽象解释框架内形式化分析了该方法，该框架具有高度模块化特性，可轻松扩展以支持其他类型的依赖-保证条件结构。我们形式化了该方法的两个版本，并在一种简单编程语言上对其实现进行了评估。