• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >Integration of a Software Model Checker into Isabelle
【24h】

Integration of a Software Model Checker into Isabelle

机译：将软件模型检查器集成到Isabelle中

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

摘要

The paper presents a combination of interactive and automatic tools in the area of software verification. We have integrated a newly developed software model checker into an interactive verification environment for imperative programming languages. Although the problems in software verification are mostly too hard for full automation, we could increase the level of automated assistance by discharging less interesting side conditions. That allows the verification engineer to focus on the abstract algorithm, safely assuming unbounded arithmetic and unlimited buffers.
机译：本文介绍了在软件验证领域中交互式和自动工具的组合。我们已经将新开发的软件模型检查器集成到用于命令式编程语言的交互式验证环境中。尽管对于完全自动化而言，软件验证中的问题大多过于棘手，但我们可以通过消除不太有趣的附带条件来提高自动化协助的水平。这使验证工程师可以专注于抽象算法，安全地假定无限制的算术和无限的缓冲区。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号