• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>European joint conferences on theory and practice of software;International conference on tools and algorithms for the construction and analysis of systems;TOOLympics conference >Jay Horn: A Java Model Checker (Competition Contribution)
【24h】

Jay Horn: A Java Model Checker (Competition Contribution)

机译：杰伊·霍恩（Jay Horn）：Java模型检查器（竞争贡献）

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

JayHorn is a model checker for verifying sequential Java programs annotated with assertions expressing safety conditions. JayHorn uses the Soot library to read Java bytecode and translate it to the Jimple three-address format, then converts the Jimple code in several stages to a set of constrained Horn clauses, and solves the Horn clauses using solvers like SPACER and Eldarica. JayHorn uses a novel, invariant-based representation of heap data-structures, and is therefore particularly useful for analyzing programs with unbounded data-structures and unbounded run-time. JayHorn is open source and distributed under MIT license (https://github.com/jayhorn/jayhorn).
机译：JayHorn是一个模型检查器，用于验证用表示安全条件的声明注释的顺序Java程序。 JayHorn使用Soot库读取Java字节码并将其转换为Jimple三地址格式，然后将Jimple代码分几个阶段转换为一组受约束的Horn子句，并使用诸如SPACER和Eldarica的求解器来求解Horn子句。 JayHorn使用新颖的，基于不变的堆数据结构表示形式，因此对于分析具有无限制数据结构和无限制运行时的程序特别有用。 JayHorn是开源的，并根据MIT许可（https://github.com/jayhorn/jayhorn）进行分发。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号