首页/论文/1906.02808

arXiv 1906.028082019-06-06cs.LOcs.FL

用Prolog实现面向对象程序的动态分配内存验证

Dynamically Allocated Memory Verification in Object-Oriented Programs using Prolog

René Haberland, Sergey Ivanovskiy

备注：: 5 pages, 4 figures
发表信息：: ISP-RAS, 8th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE), 2014, pp.46-50, ISBN 978-5-91474-020-4, ISSN 2311-7230
DOI：: 10.15514/SYRCOSE-2014-8-7

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

一个基于Prolog的框架，目前正在开发的基于堆的面向对象的数据的全自动验证。动态分配的问题进行了讨论，最近的方法和标准进行了分析。通过实例介绍了该体系结构及其组成。最后，对进一步开展相关工作提出了建议.

英文摘要：

A Prolog-based framework for fully automated verification currently under development for heap-based object-oriented data is introduced. Dynamically allocated issues are discussed, recent approaches and criteria are analysed. The architecture and its components are introduced by example. Finally, propositions to further and related work are given.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

基于Prolog的嵌入式系统Source Code验证

Source Code Verification for Embedded Systems using Prolog

系统相关的嵌入式软件需要可靠，因此需要经过良好的测试，特别是对于航空航天系统。验证程序的一种常用技术是分析程序的抽象语法树（AST）。树结构可以用逻辑程序设计语言Prolog来优雅地分析。此外，Prolog还为全面分析提供了进一步的优势：一方面，它本身提供了多功能选项来有效地处理树或图数据结构。另一方面，Prolog的非确定性和回溯简化了对程序流的不同变体的测试，而不需要付出很大的努力。一个基于规则的方法与Prolog允许验证目标的特点，在一个简洁和声明的方式。在本文中，我们描述了我们的方法来验证的闪存文件系统的源代码与Prolog的帮助。闪存文件系统是用C++编写的，专门为卫星使用而开发。我们将一个给定的抽象语法树的C++源代码转换成Prolog的事实，并推导出调用图和执行序列（树），然后进一步测试验证目标。由于控制结构的不同程序流分支是通过回溯作为完整执行序列的子树而导出的。最后，这些子树在Prolog中进行了验证。我们说明了我们的方法与案例研究，在那里我们搜索不正确的应用程序中使用的实时操作系统RODOS的嵌入式软件中的信号量。我们依赖于计算树逻辑（CTL），并设计了一个嵌入式领域特定语言（DSL）的Prolog来表达的验证目标。

2017-01-03cs.LOcs.PLcs.SE

为Prolog验证的自动定理证明

Automated Theorem Proving for Prolog Verification

université de La Réunion（留尼汪大学）

本文提出通过将LPTP的公理转换为一阶公式并利用自动定理证明器验证Prolog程序属性。

2026-01-07cs.LOcs.PL

使用ProB对Prolog转换系统进行动画制作、验证和可视化

Animation, Verification and Visualisation of Prolog Transition Systems with ProB

Faculty of Mathematics；Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universit\" a tsstr. 1, D-40225 D\" u sseldorf

介绍了基于Prolog的ProB工具，阐述其Prolog动画模式的现有功能及扩展，如统计检查模拟、可靠跟踪重放等，通过四子棋等案例研究展示新功能用途，对Event-B证明及教学演示模型等应用有帮助。

2026-07-24cs.AIcs.GTcs.LO

逻辑+控制：程序构造与验证

Logic + control: On program construction and verification

本文提出了一个例子，形式化推理的语义Prolog程序的实际意义（SAT求解器的豪和国王）。该程序被视为一个带有附加控制的定子句逻辑程序。逻辑程序是通过逐步精化的方法构造的，并与其正确性和完整性证明携手并进。证明是声明性的--它们不引用任何操作语义。逻辑程序构造的每一步都遵循一种系统的方法来构造可证明正确和完整的程序。我们还证明了在最终的Prolog程序中保持了逻辑程序的正确性和完整性。此外，我们证明终止，发生检查自由和非挣扎。我们的例子展示了如何将处理“逻辑”和处理“控制”分开。大多数证明都可以在“逻辑”级别上完成，从任何操作语义中抽象出来。这个例子使用了近似的规格说明;它们在简化逻辑程序的推理中是至关重要的。它还表明，语义保持程序转换的范例可能是不够的。我们建议考虑转换保持正确性和完整性方面的近似规范。

2017-05-12cs.LOcs.PL

关系验证的WhyRel原型

The WhyRel Prototype for Relational Verification

程序之间的互操作关系在各种验证环境中作为一项任务出现，例如优化转换，将新版本的程序与旧版本（回归验证）和不干扰。然而，现有的工具，它提供了一个高水平的自动化的成本限制的程序考虑的关系验证的程序动态分配的可变状态的支持并不好。另一方面，自动激活工具需要更多的用户交互，但可以验证更广泛的程序类别。本文介绍了WhyRel，一个基于关系区域逻辑的指针程序关系属性自动验证工具。WhyRel通过验证案例研究进行评估，依赖于由Why3平台编排的SMT求解器。案例研究包括建立表示独立的ADT，显示不干扰，并从最近的文献挑战的问题。

2023-03-25cs.LOcs.PL

基于不变量的堆编码（技术报告）

Sound and Complete Invariant-Based Heap Encodings (Technical Report)

Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）

本文提出时间索引堆不变量，通过未解释谓词和预言变量减少堆操作程序的验证至整数程序验证，首次实现堆不变量方法的正确性与完备性。

2026-03-13cs.LO

更多相关论文收起更多论文

使用一阶逻辑模拟可达性及其在链接数据结构验证中的应用

Simulating reachability using first-order logic with applications to verification of linked data structures

本文介绍了如何利用现有的一阶逻辑定理证明器自动验证执行动态存储分配和破坏性更新的指针值结构字段的命令式程序的安全属性。其中一个主要的障碍是指定和证明（缺乏）的可达性动态分配的细胞之间的属性。主要的技术贡献是使用一阶公式以保守的方式模拟可达性的方法-该公式描述了一组程序状态的超集，如果有一个精确的方式来表达可达性，则会指定该超集。这些方法用于半自动程序验证（即，使用程序员提供的循环不变量），例如标记并清除垃圾回收和单链表的破坏性反转。(The标记和扫描的例子以前已经被报道为超出了ESC/Java的能力。

2009-05-27cs.LOcs.PL

约束Horn子句的堆理论（扩展技术报告）

A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)

约束Horn子句（CHC）是一种中间程序表示，可以由几个验证工具生成，并且可以由许多Horn求解器处理和求解。在验证中使用CHC时的主要挑战之一是堆分配的数据结构的编码：这种数据结构今天要么使用数组理论显式表示，要么在不变量或细化类型的帮助下转换，击败CHC作为语言独立的表示以及Horn求解器实现的算法的不可知性。本文提出了一种适用于CHC的SMT-LIB堆理论，目的是为具有堆数据结构的程序提供一种标准的交换格式。我们介绍了堆理论的语法，定义其语义的公理和使用减少SMT-LIB数组和数据类型，并讨论其属性和大纲可能的扩展和未来的工作。

2021-04-09cs.LO

单遍堆操作程序的内存安全判定

Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

我们调查的可判定性的自动程序验证的程序，操作堆，特别是，决策程序证明内存安全。我们最近的工作，确定了一个可判定的子类未解释的程序，一类别名感知的程序，可以更新地图。我们应用这一理论来开发验证算法的内存安全-确定如果一个堆操作程序，分配和释放内存位置和操作堆指针不引用未分配的内存位置。我们表明，这个问题是可判定的，当初始分配的堆形成一个森林的数据结构，当程序流一致，直观地限制程序，使一个单一的数据结构通过。我们的一组库例程，操纵森林数据结构的实验评估表明，常见的单通算法的数据结构往往属于可判定类，我们的决策过程是有效的，在验证它们。

2019-12-31cs.FLcs.LOcs.PL

验证基于效应处理程序的按定义运行反向模式自动微分库

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

本文研究基于效应处理程序的按定义运行反向模式自动微分库的验证，通过分离逻辑提供机器检查的正确性证明。

2023-10-20cs.LOcs.PL

一种更简单的堆分离指向逻辑

A Stricter Heap Separating Points-To Logic

动态内存问题很难定位，可能会花费开发项目的大量精力，并且在之后由不同的人独立地重复报告类似的问题。验证作为一种形式化方法可以证明给定程序的堆与指定的动态行为相匹配。动态（或堆）内存，是主内存中的区域，在程序执行期间由程序语句操作，如alloc，free和指针操作。通常，堆内存是为那些在执行前内存使用量未知的问题分配的。堆内的区域可能“以某种方式”彼此相关，通常但不总是通过包含相关堆单元的绝对地址的指针。由所有有效指针变量描述的数据结构表明堆图。堆图是动态内存中的一个有向连通简单图，其中每个顶点代表一个唯一的内存地址，每条边连接两个堆顶点。堆图必须由来自本地堆栈的至少一个变量或最终由至少一个堆栈变量指向的其他堆图链指向。堆顶点不能重叠。堆公式表示动态内存上的断言，可以是heaplet，也可以是递归定义的堆空间或逻辑公式。

2019-06-26cs.LO

在递归存在的情况下通过堆进行交互

Interacting via the Heap in the Presence of Recursion

几乎所有现代命令式程序设计语言都包含动态操作堆的操作，例如通过分配和释放对象，以及通过更新引用字段。在递归过程和局部变量的存在下，程序与堆的交互可能变得相当复杂，因为可以使用局部变量在调用堆栈上分配无限数量的对象，或者匿名地使用引用字段在堆上分配对象。因此，一般来说，静态分析是不可判定的。在本文中，我们研究了验证的递归程序与无界分配的对象，在一个简单的命令式语言堆操作。我们提出了一种改进的语义，这种语言，使用的抽象是精确的。对于任何具有有界可见堆的程序，这意味着在任何执行点从变量可到达的对象数量是有界的，这种抽象是其行为的有限表示，即使在状态中可能出现无限数量的对象。因此，对于这样的程序，模型检验是可判定的。最后，我们介绍了一个规约语言的时间属性的堆，并讨论了模型检验这些属性对堆操作程序。

2012-12-17cs.LOcs.PL