多线程程序的CARET分析
CARET analysis of multithreaded programs
摘要：
动态下推网络（DPN）是具有（递归）过程调用和线程创建的多线程程序的自然模型。另一方面，CARET是一种时态逻辑，允许编写线性时态公式，同时考虑调用和返回之间的匹配。本文研究了基于CARET公式的DPN模型检验问题。我们表明，这个问题可以有效地解决减少Büchi动态下推系统的空虚问题。然后，我们表明，CARET模型检验也是可判定的DPN与锁通信。我们的研究结果可以，特别是，可用于并发恶意软件的检测。
英文摘要：
Dynamic Pushdown Networks (DPNs) are a natural model for multithreaded programs with (recursive) procedure calls and thread creation. On the other hand, CARET is a temporal logic that allows to write linear temporal formulas while taking into account the matching between calls and returns. We consider in this paper the model-checking problem of DPNs against CARET formulas. We show that this problem can be effectively solved by a reduction to the emptiness problem of Büchi Dynamic Pushdown Systems. We then show that CARET model checking is also decidable for DPNs communicating with locks. Our results can, in particular, be used for the detection of concurrent malware.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
