Low-Level Code Verification Based on CSP Models
Low-Level Code Verification Based on CSP Models
复制标题
基于CSP模型的低级代码验证
DOI：
10.1007/978-3-642-10452-7_18
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
S. Helke
中科院分区：
文献类型：
--
作者：
M. Kleine;S. Helke
本文提出了一种方法，使用CSP来验证现实生活中的多线程应用程序的实现，从而有助于软件验证的广泛领域。因此，我们使用CSP来形式化程序的编译器中间表示。我们的方法将低级表示分为三个部分：特定于应用程序的部分，描述线程的行为;特定于域的部分，封装低级软件概念，如调度;和特定于平台的部分，这是硬件模型。这三个部分形成了一个低层次的CSP模型，使我们能够通过模型检查或定理证明来证明属性，例如模型中不存在竞争条件。特定于应用程序的部分是从多线程程序的LLVM中间表示合成的。
This paper contributes to the broad field of software verification by proposing a methodology that uses CSP to verify implementations of real-life multithreaded applications. We therefore use CSP to formalize the compiler intermediate representation of a program. Our methodology divides the low-level representation into three parts: an application-specific part, describing the behavior of threads; a domain-specific part, which encapsulates low-level software concepts such as scheduling; and a platform-specific part, which is the hardware model. These three parts form a low-level CSP model that enables us to prove properties, e.g. the absence of race conditions in the model, by either model checking or theorem proving. The application-specific part is synthesized from the LLVM intermediate representation of a multithreaded program.
登录
查看更多内容
如何通过细化对CSP进行FDR Spin LTL模型检验
DOI：
10.1007/3-540-45251-6_6
发表时间：
2001
期刊：
Proceedings of the eighth annual ACM Symposium on Principles of distributed computing
影响因子：
--
作者：
M. Leuschel;T. Massart;A. Currie
通讯作者：
A. Currie
使用 MCP 模型检查器验证 C Flight 软件
DOI：
--
发表时间：
2008
期刊：
IEEE Aerospace Conference
影响因子：
--
作者：
S. Thompson;G. Brat
通讯作者：
G. Brat
自动生成 CSP 规范
DOI：
--
发表时间：
2003
期刊：
Journal of universal computer science (Online)
影响因子：
--
作者：
Frantisek Scuglik;M. Svéda
通讯作者：
M. Svéda
不相交数据结构的自动池分配
DOI：
--
发表时间：
2003
期刊：
Memory System Performance
影响因子：
--
作者：
Chris Lattner;Vikram S. Adve
通讯作者：
Vikram S. Adve