• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Partial Orders for Efficient Bounded Model Checking of Concurrent Software
【24h】

Partial Orders for Efficient Bounded Model Checking of Concurrent Software

机译：并行软件的有效有界模型检查的部分订单

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The number of interleavings of a concurrent program makes automatic analysis of such software very hard. Modern multiprocessors' execution models make this problem even harder. Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient encoding into integer difference logic for bounded model checking that enables first-time formal verification of deployed concurrent systems code. We implemented the encoding in the CBMC tool and present experiments over a wide range of memory models, including SC, Intel x86 and IBM Power. Our experiments include core parts of PostgreSQL, the Linux kernel and the Apache HTTP server.
机译：并发程序的交错次数使这种软件的自动分析变得非常困难。现代多处理器的执行模型使这个问题更加棘手。用部分顺序而不是交错对程序执行进行建模解决了两个问题：我们获得了有效的整数差分逻辑编码，用于有边界的模型检查，从而可以对部署的并发系统代码进行首次形式验证。我们在CBMC工具中实现了编码，并针对包括SC，Intel x86和IBM Power在内的各种内存模型进行了实验。我们的实验包括PostgreSQL，Linux内核和Apache HTTP服务器的核心部分。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号