多线程程序的 CARET 分析
计算机科学中的逻辑
2017-09-27 v1 形式语言与自动机理论
摘要
动态下推网络（DPN）是具有（递归）过程调用和线程创建的多线程程序的自然模型。另一方面，CARET 是一种时序逻辑，允许在考虑调用与返回之间匹配的同时编写线性时序公式。在本文中，我们考虑了 DPN 针对 CARET 公式的模型检验问题。我们证明该问题可以通过归约为 Büchi 动态下推系统的空性问题来有效求解。随后我们证明，对于使用锁进行通信的 DPN，CARET 模型检验也是可判定的。我们的结果特别可用于并发恶意软件的检测。
引用
@article{arxiv.1709.09006,
title = {CARET analysis of multithreaded programs},
author = {Huu-Vu Nguyen and Tayssir Touili},
journal= {arXiv preprint arXiv:1709.09006},
year = {2017}
}
备注
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)