一句话：证明上下文限界下多栈下推系统对 Dyck 等上下文无关规范的精化验证可判定且 coNP 完全。
精化验证要求实现的行为包含于规范。本文研究实现为多线程共享内存系统（多栈下推自动机）、规范为输入确定多栈下推语言时的精化验证。核心结果：仅考虑上下文切换次数有界的运行，并要求行为属于 Dyck 语言规范时，问题可判定且 coNP 完全；对更一般的输入确定语言亦然。证明引入形式语言与计数器程序技术，将反例搜索在非确定多项式时间内归约到存在 Presburger 算术可满足性。由于无界多栈下推自动机空性不可判定，该结果可验证正则规范之外的非正则性质，并应用于多线程程序的引用计数与可重入锁分析。
A fundamental problem in refinement verification is to check that the language of behaviors of an implementation is included in the language of the specification. We consider the refinement verification problem where the implementation is a multithreaded shared memory system modeled as a multistack pushdown automaton and the specification is an input-deterministic multistack pushdown language. Our main result shows that the context-bounded refinement problem, where we ask that all behaviors generated in runs of bounded number of context switches belong to a specification given by a Dyck language, is decidable and coNP-complete. The more general case of input-deterministic languages follows, with the same complexity. Context-bounding is essential since emptiness for multipushdown automata is already undecidable, and so is the refinement verification problem for the subclass of regular specifications. Input-deterministic languages capture many non-regular specifications of practical interest and our result opens the way for algorithmic analysis of these properties. The context-bounded refinement problem is coNP-hard already with deterministic regular specifications; our result demonstrates that the problem is not harder despite the stronger class of specifications. Our proof introduces several general techniques for formal languages and counter programs and shows that the search for counterexamples can be reduced in non-deterministic polynomial time to the satisfiability problem for existential Presburger arithmetic. These techniques are essential to ensure the coNP upper bound: existing techniques for regular specifications are not powerful enough for decidability, while simple reductions lead to problems that are either undecidable or have high complexities. As a special case, our decidability result gives an algorithmic verification technique to reason about reference counting and re-entrant locking in multithreaded programs.
@article{paperbot2104,
title = {Context-Bounded Verification of Context-Free Specifications},
author = {Pascal Baumann and Moses Ganardi and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571266}
}