多线程程序文件安全性的动态验证
计算机科学中的逻辑
2012-06-07 v1 编程语言
摘要
在本文中，我们提出了一种用于检查多线程程序文件安全性的新语义。文件安全程序是指在所提出的语义下能够到达最终配置的程序。我们用文件操作和多线程命令扩展了 While 语言，并将新语言称为 whilef。本文表明，对于 whilef 而言，文件安全性是一个不可判定的性质。在本文展示的一种特殊情况下，文件安全性成为了可判定的性质。这种情况发生在用户提供指针信息时。如果文件是安全的，我们将其称为强安全文件程序。我们修改了该语言的语法和语义，并将其称为 SafeWhilef。
引用
@article{arxiv.1206.1090,
title = {Dynamic Verification for File Safety of Multithreaded Programs},
author = {Mohamed A. El-Zawawy and Nagwan M. Daoud},
journal= {arXiv preprint arXiv:1206.1090},
year = {2012}
}
备注
7 pages, http://paper.ijcsns.org/07_book/201205/20120503.pdf