Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs
复制标题
让这张图为你见证吧！
DOI：
10.1007/978-3-319-96142-2_1
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Thomas Noll
中科院分区：
文献类型：
--
作者：
Hannah Arndt;Christina Jansen;Joost-Pieter Katoen;Christoph Matheja;Thomas Noll
我们提出了一个基于图的工具，用于分析动态数据结构上运行的Java程序。它涉及使用用户定义的图文法生成抽象状态空间。然后将LTL模型检查应用于该状态空间，支持结构和功能的正确性属性。分析是完全自动化的，程序模块化，并提供信息丰富的视觉反馈，包括在财产违规情况下的反例。
We present a graph-based tool for analysing Java programs operating on dynamic data structures. It involves the generation of an abstract state space employing a user-defined graph grammar. LTL model checking is then applied to this state space, supporting both structural and functional correctness properties. The analysis is fully automated, procedure-modular, and provides informative visual feedback including counterexamples in the case of property violations.
登录
查看更多内容
树状语法和分离逻辑
DOI：
--
发表时间：
2015
期刊：
Asian Symposium on Programming Languages and Systems
影响因子：
--
作者：
Christoph Matheja;Christina Jansen;T. Noll
通讯作者：
T. Noll
DOI：
10.1007/978-3-662-54434-1_23
发表时间：
2017
期刊：
ArXiv
影响因子：
--
作者：
Christina Jansen;Jens Katelaan;Christoph Matheja;Thomas Noll;Florian Zuleger
通讯作者：
Florian Zuleger
改进 TVLA：使参数形状分析具有竞争力
影响因子：
3.3
作者：
Igor Bogudlov;T. Lev;T. Reps;Shmuel Sagiv
通讯作者：
Shmuel Sagiv
验证 Java 程序 - 图语法方法
DOI：
--
发表时间：
2015
期刊：
影响因子：
--
作者：
J. Heinen
通讯作者：
J. Heinen
为指针程序生成基于抽象图的过程摘要
影响因子：
2.2
作者：
Christina Jansen;T. Noll
通讯作者：
T. Noll