Making Relational Hoare Logic Alignment Complete
针对关系验证中的对齐完备性问题，提出基于带测试克林代数的语义保持重写规则，证明RHL相对于通用对齐自动机具有对齐完备性，打通了语法推理与自动机验证的壁垒。
2023-07-20 cs.LO
Alignment complete relational Hoare logics for some and all
本文针对关系验证中的计算步骤对齐问题，提出并证明了针对∀∀和∀∃性质的关系型霍尔逻辑的对齐完备性，同时讨论了对齐在关系推理中的局限性并提出蕴含完备性作为评估手段。
2025-11-07 cs.LO
Alignment Completeness for Relational Hoare Logics
关系霍尔逻辑（RHL）提供了推理程序之间关系的规则。几个RHL包括一个我们称之为序贯积的规则，它从普通霍尔逻辑（HL）的判断中推断出关系正确性判断。其他规则体现了合理的推理模式，并已被发现在实践中很有用，但连续产品是相对完整的本身（与HL）。作为一种更令人满意的方法来评估RHL，对齐完整性的概念，引入的归纳断言方法和产品自动机。对齐完整性的结果，考虑到几个不同的规则集。该概念可以用于指导RHL和关系验证器的设计，以用于更丰富的程序设计语言和对齐模式。
2021-04-30 cs.LO cs.PL
A New Perspective for Hoare's Logic and Peano's Arithmetic
Hoare逻辑是证明程序正确性的公理系统，它已被扩展为一种分离逻辑，用于对可变堆结构进行推理。我们在Peano算术$PA$中发展了Hoare逻辑最基本的最强后置条件逻辑结构。设$p\in L$和$S$为任意while程序。$\textbf{N}$ -可计算函数$f_S^{\textbf{N}}$的算术可定义性导致$S$与$SP(p,S)$分离，它定义了$p$和$S$在$\textbf{N}$上的最强后置条件，从而在$PA$中得到等价但更有意义的形式.从Hoare逻辑到PA的约化，再加上定义良好的底层语义，可以得出Hoare逻辑相对于$PA$理论是健全和完备的，这与Cook意义上的相对完备性不同。最后，我们讨论了两种方法来扩展可计算性从标准结构的非标准模型的$PA$。
2013-11-19 cs.LO
Thirty-seven years of relational Hoare logic: remarks on its principles and history
关系霍尔逻辑扩展了模块化演绎验证的适用性，以涵盖重要的2-运行属性，包括依赖性要求，如机密性和程序关系，如程序版本之间的等效性或相似性。相当数量的最近的作品介绍了不同的关系霍尔逻辑尚未收敛到一套核心的证明规则。本文回顾了鲜为人知的早期工作。这揭示了一些原则，澄清和组织的规则，以及建议一个新的规则和完整性的新概念。
2022-07-16 cs.LO cs.PL
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
我们推导出一个霍尔弗洛伊德逻辑的非本地跳转和可变的高阶程序变量从一个formula-as-types概念的控制经典逻辑。这项工作的主要贡献是设计了一个强制依赖型系统的非本地跳转对应于经典逻辑，但著名的后果规则仍然是可推导的。
2011-12-13 cs.LO
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
本文提出将断言提升至任意状态集合性质的超霍尔逻辑，可在同一框架内证明和否证包括现有逻辑无法表达的任意程序超性质，且已证明其可靠性与完备性，所有结果均在Isabelle/HOL中验证。
2024-04-11 cs.LO
On Completeness Results of Hoare Logic Relative to the Standard Model
Cook研究了霍尔逻辑相对于Peano算术的标准模型$N$的一般完备性问题，它允许使用任意算术公式作为断言。在实践中，断言将是简单的算术公式，例如算术层次中的低级别。此外，我们发现，通过限制$N$的输入，最小断言理论的复杂性，霍尔逻辑的完整性，以保持可以降低。本文进一步研究了霍尔逻辑相对于$N$的完备性，将断言限制在算术公式的子类中（并将输入限制在$N$中）。我们的完整性结果完善库克的结果，降低了复杂性的断言理论。
2017-03-01 cs.LO
A quantitative probabilistic relational Hoare logic
本文提出定量关系概率程序逻辑 eRHL，利用扩展非负实数断言突破 PRHL 与 apRHL 的随机性对齐限制，并证明其在程序等价、统计距离和差分隐私上的可靠完备性。
2025-01-08 cs.LO
Quantum Relational Hoare Logic
我们提出了一个逻辑的推理对互动的量子程序-量子关系霍尔逻辑（qRHL）。这种逻辑遵循概率关系霍尔逻辑（Barthe et al. 2009）的精神，并允许我们在给定输入关系的情况下，用公式表示两个量子程序的输出如何相关。概率RHL被广泛用于经典密码协议的计算机验证安全性证明。由于pRHL不适合分析量子密码，我们提出qRHL作为替代，适合后量子密码和量子协议的安全性分析。qRHL的设计对量子设置提出了一些独特的挑战，例如，量子寄存器上相等的定义。最后，我们实现了一个工具来验证qRHL中的证明，并在其中开发了几个示例安全证明。
2019-01-14 cs.LO quant-ph
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
我们提出了简单的新的霍尔逻辑和精化演算的混合系统的风格的微分动态逻辑。（细化）Kleene代数与测试用于推理程序结构和生成验证条件在这一级。透镜以通用代数方式捕获混合程序存储。该方法已正式与伊莎贝尔/霍尔证明助手。一些示例解释了工作流程和最终的验证组件。
2019-10-29 cs.LO
Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism
我们研究了霍尔逻辑的一个命题变体，它可以用于推理表现出天使和恶魔非决定论的程序。我们在一个未解释的环境中工作，其中原子动作的意义是使用某种形式的假设公理化地指定的。我们的逻辑形式主义是完全合成的，它包含了有限图上的安全游戏的非合成形式主义。我们提出了声音和完整的霍尔式演算，是有用的建立部分正确性断言，以及合成实现。利用运算模型研究了Hoare对偶不确定性理论的计算复杂性，证明了该理论在指数时间上是完备的.
2016-09-02 cs.LO
A Hybrid Hoare Logic for Gene Network Models
基因网络建模的主要困难是确定控制其动态的参数。对于时间连续的模型来说，这是特别困难的：参数具有无法枚举的实值。普遍的想法是推断新的约束，减少可能值的范围。在这里，我们提出了一个新的工作的基础上的一个特定的类的混合自动机（灵感来自托马斯离散模型），离散参数被替换为签署celerities。我们提出了一种新的方法，涉及霍尔逻辑和最弱的前提演算（一拉Dijkstra），产生的参数值的约束。事实上，一旦从具有持续时间信息的生物痕迹（在文献或生物实验中发现）中提取出适当的规范，它们就扮演着类似于经典霍尔逻辑中的命令程序的角色。我们说明我们的混合霍尔逻辑上的一个小模型控制乳糖操纵子的lacI阻遏物。
2016-10-21 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
A Hoare Logic for Domain Specification (Full Version)
针对现有程序规约与验证方法仅关注计算层面正确性的问题，研究提出整合实现与领域断言的双层霍尔逻辑，采用描述逻辑和语义提升方法，通过两类断言转换的演算实现关注点分离并支持验证中使用描述逻辑。
2024-02-01 cs.LO
Scope Logic: Extending Hoare Logic for Pointer Program Verification
本文提出了一种扩展霍尔逻辑的指针程序验证方法。首先，对VDM使用的部分函数逻辑（LPF）进行扩展，以指定使用指针的存储器访问和复合类型的存储器布局。然后，本文介绍了数据检索函数（DRF）和内存作用域函数（MSF）的概念。人们可以定义DRF来从互连的具体数据对象中检索抽象值。DRF的对应MSF的定义可以从DRF的定义在语法上导出。这个MSF计算当DRF检索抽象值时访问的内存单元集。这个内存单元集称为抽象值的内存范围。最后，对Hoare逻辑中赋值语句的证明规则进行了修改，使之适用于指针。其基本思想是，只要其作用域中没有内存单元被重写，虚值就保持不变。另一个证明规则是为内存分配语句添加的。结果规则和控制流语句的规则略有修改。它们与霍尔逻辑中的原始版本基本相同。一个例子来显示这种逻辑的有效性。并给出了指针程序验证的一些技巧。
2009-12-21 cs.LO
Functions as types or the "Hoare logic" of functional dependencies
受程序设计理论统一化趋势的启发，本文说明了标准数据依赖理论的代数处理如何为关系数据配备函数类型和相关类型系统，这对数据库操作的类型检查和查询优化是有用的。这种类型化的方法，数据库编程，然后被证明是同一个家庭的其他编程逻辑，如例如。霍尔逻辑或最强不变函数的逻辑，用于分析while语句。使用自动演绎系统，如Prover9的类型检查和查询优化上这样一个代数方法的前景被认为是。
2012-10-17 cs.LO
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
我们提出了一个工具，用于验证的混合系统表示的顺序片段的HCSP（混合通信顺序进程）。该工具允许注释HCSP程序与前，后条件，不变量，并证明规则的推理常微分方程。验证条件是根据混合霍尔逻辑的规则从注释中生成的。我们设计了标记和突出显示机制来区分和可视化不同的验证条件。该工具使用Python实现，并具有基于Web的用户界面。我们评估了翻译的Simulink/Stateflow模型和KeYmaera X基准工具的有效性。
2023-02-21 cs.LO
Automatic Function Annotations for Hoare Logic
本文提出一种自动存储并复用中间推理的函数注解逻辑，扩展 Hoare 逻辑以减少多性质验证中的重复证明，并在 Isabelle/HOL 与 seL4 微内核实验中显著降低证明规模与复杂度。
2012-11-27 cs.LO
Graded Hoare Logic and its Categorical Semantics
基于程序逻辑的演绎验证技术（即，Floyd-霍尔逻辑族）是用于程序推理的强大方法。最近，有一种趋势是增加这种逻辑的表达能力，通过增加额外的信息来推断程序的副作用。例如，一般的程序逻辑已经增加了成本分析，逻辑的概率计算已经增加了估计措施，和逻辑的差分隐私与不可否认的界限。在这项工作中，我们统一这些不同的方法，通过分级的范例，适应世界的功能演算和语义。我们提出了分级霍尔逻辑（GHL），一个参数化的框架，用于增强程序逻辑与一个预序monoidal分析。我们开发了一个语义框架GHL建模，使分级，逻辑断言（前和后条件）和潜在的有效语义的命令式语言可以集成在一起。我们的框架的核心是一个分级的范畴，我们在这里扩展的概念，引入分级Freyd类别，提供了一个语义，可以解释许多例子，从文献中的增强程序逻辑。我们利用相干纤维化来建模基本断言语言，因此整体设置也是纤维化的。
2021-01-26 cs.LO
Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond
该研究聚焦程序逻辑的整体视角构建，通过推广Hoare逻辑与不正确性逻辑得到多类性质，并将其与带顶元素和测试的Kleene代数的可表达性质做对比，为程序逻辑领域的统一研究提供了代数层面的参考。
2023-12-15 cs.LO cs.PL
On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
本文提出首个带while循环的相对完备的基于满足性的量子霍尔逻辑，通过构造最弱前置项演算证明完备性，并成功验证Deutsch算法和量子隐形传态的正确性。
2024-05-03 cs.LO
A foundational characterization of Hoare Logic
Computer Science Department, Indiana University Bloomington（印第安纳大学布卢明顿分校计算机科学系）
本文证明了迭代程序的部分正确性断言在霍尔逻辑中可证明当且仅当其在标准二阶逻辑中可证明，且二阶谓词的范围限制为一阶谓词。
2026-05-13 cs.LO math.LO
Access Hoare Logic
Swansea University（斯旺西大学）
本文提出访问霍尔逻辑，用于分析计算机程序的访问安全，证明其正确性和完备性，并与标准霍尔逻辑建立联系，展示其与其它方法的根本差异。
2026-03-30 cs.CR cs.LO cs.SC
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
抽象解释、霍尔逻辑和不正确（或反向霍尔）逻辑是静态分析计算机程序的强大技术。所有这些都已成功地扩展到量子设置，但在很大程度上是并行开发的。在本文中，我们研究这些技术之间的关系，在验证量子while程序的背景下，其中的抽象域和一组断言的量子状态是结构良好的。特别地，我们证明了任何完全的量子抽象解释都可以导出一个量子霍尔逻辑和一个量子不正确逻辑，这两个逻辑都是合理的和相对完备的。与文献中提出的逻辑不同，诱导逻辑系统是以向前的方式，使它们在某些应用中更有用。相反，任何健全的和相对完整的量子霍尔逻辑或量子不正确逻辑都导出一个完整的量子抽象解释。作为应用，我们证明了当局部子空间元组作为断言时，不存在任何可靠的、相对完备的量子霍尔逻辑或不正确逻辑.
2022-06-28 cs.LO quant-ph
Nested Hoare Triples and Frame Rules for Higher-order Store
分离逻辑是一种霍尔风格的逻辑，用于对具有堆分配的可变数据结构的程序进行推理。作为一个步骤，扩展分离逻辑的高级语言ML风格的一般（高阶）存储，我们调查的兼容性嵌套霍尔三元组与几个变化的高阶框架规则。嵌套三元组和框架规则的相互作用可能是微妙的，并且包含某些框架规则实际上是不合理的。一个特定的规则组合可以通过克里普克模型来证明是一致的，在克里普克模型中，世界生活在一个递归定义的超度量空间中。由此产生的逻辑允许我们优雅地证明涉及存储代码的程序。特别是，使用递归定义的断言，它导致了自然的规范和通过存储处理递归所需的不变量的证明。
2011-09-27 cs.LO
A Theorem Prover for Quantum Hoare Logic and Its Applications
量子霍尔逻辑（QHL）在Ying的工作中被引入来描述和推理量子程序。在本文中，我们实现了一个定理证明QHL基于Isabelle/HOL。通过应用定理证明器，验证一个量子程序的规格等价地转化为矩阵之间的顺序关系。由于Isabelle/HOL的局限性，顺序关系的计算通过调用外部Python语言的oracle来解决。据我们所知，这是量子程序的第一个定理证明器。为了证明它的力量，两个著名的量子算法，即，Grover量子搜索和量子相位估计是Shor的多项式时间分解量子算法的关键步骤，利用定理证明器证明了这两个步骤。这是他们两人的第一次机械化证明。
2016-01-15 cs.LO
A Generalized Hybrid Hoare Logic
针对现有规范逻辑难以处理通信并发式混合系统建模的问题，本文提出面向HCSP的广义混合霍尔逻辑，证明其两类相对完备性，并在Isabelle/HOL中实现且通过案例验证了其能力与可扩展性。
2024-07-13 cs.LO
Completeness of Hoare Logic over Nonstandard Models
程序语义的非标准方法成功地解决了Floyd-霍尔逻辑的完备性问题。非标准语义学的已知版本，匈牙利语义学和公理语义学，是如此的普遍，以至于它们要么缺乏数学的优雅性，要么缺乏实际的实用性。本文的目的是展示一个不仅在数学上优雅，但实际上有用的非标准语义。Peano算术$PA$的标准模型$N$中可计算函数的一个基本性质是$Σ_1$ -可定义性。然而，在$PA$的非标准模型$M$中，由while程序$S$的标准解释导出的函数并不总是算术的。问题在于$M$中$S$的标准终止使用了$N$中的有限性，而这不是$M$中的有限性。为此，我们将给出一个新的解释$S$在$M$，$S$的终止使用$M$ -有限性，和$S$产生的功能在所有的$PA$模型具有统一的$Σ_1$ -可定义性。在此基础上，定义了$PA$非标准模型中霍尔逻辑的新语义，并证明了霍尔逻辑的标准公理系统是可靠的、完备的.新的语义在$PA$中，匈牙利语义学和公理语义学与while程序的新语义学相一致。此外，各种比较与以前的结果，有用的非标准的语义，并评论的完整性问题。
2017-03-01 cs.LO
Quantum Hoare Logic with Ghost Variables
量子霍尔逻辑允许我们对量子程序进行推理。我们提出了一个扩展的量子霍尔逻辑，引入“鬼变量”，以扩展前/后条件的表达能力。幽灵变量是程序中实际上不存在的变量，允许它们具有任意的量子态（在某种意义上，它们是存在性量化的），并与程序变量纠缠在一起。Ghost变量允许我们表达诸如程序变量的分布或变量具有经典内容的事实之类的属性。作为一个案例研究，我们展示了如何量子霍尔逻辑与幽灵变量可以用来证明量子一次性密码本的安全性。
2019-02-01 cs.LO quant-ph
A General Framework for Sound and Complete Floyd-Hoare Logics
本文将霍尔逻辑抽象为可追踪的对称monoidal范畴，这是系统理论的一个非常一般的框架。我们的抽象是基于一个跟踪monoidal函子从任意跟踪monoidal范畴到范畴的前序和单调关系。我们给出了几个例子，我们的理论如何概括通常的霍尔逻辑（部分正确的，而程序，部分正确的指针程序），并提供了一些案例研究，它可以用来开发新的霍尔逻辑（运行时分析，而程序和流电路）。
2008-07-07 cs.LO cs.OH
A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
本文提出在概率关系霍尔逻辑中直接证明惰性采样程序不可区分性的新方法，无需急切采样转换及相关假设，并在EasyCrypt中实现验证。
2023-11-28 cs.CR cs.FL cs.LO
On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop
本文针对带While循环的基于满足的概率Hoare逻辑的相对完备性这一长期开放问题，构建新型PHL系统，通过两步证明其相对完备性，为随机化程序的概率性质验证提供了理论基础。
2024-06-23 cs.LO
A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --
定义了一种简单的动态类型、（纯粹的）面向对象语言。给出了一种结构化的操作语义和一种Hoare式的程序逻辑，用于在多个正确性概念中对语言中的程序进行推理。霍尔逻辑被证明是合理的和（相对）完整的，是-尽我们所知-第一个这样的逻辑动态类型的语言。
2016-01-08 cs.LO cs.PL
Proof systems for partial incorrectness logic (partial reverse Hoare logic)
本文为部分不正确性逻辑（部分反向霍尔逻辑）定义了普通和循环两种证明系统，证明其可靠且相对完备，并通过循环不变式及循环证明转化方法完成完备性证明。
2025-02-28 cs.LO cs.PL
Quantum Hoare logic with classical variables
霍尔逻辑提供了一种面向语法的方法来推理程序的正确性，并已被证明是有效的经典和概率程序的验证。现有的量子霍尔逻辑方案要么缺乏完整性，要么只支持量子变量，从而限制了它们在实际应用中的能力。在本文中，我们提出了一个量子霍尔逻辑的一个简单的while语言，其中涉及到经典和量子变量。它的健全性和相对完整性证明了部分和全部正确性的量子程序编写的语言。值得注意的是，通过经典量子态的新定义和相应的断言，逻辑系统非常简单，类似于经典程序的传统霍尔逻辑。此外，为了简化实际应用中的推理，提供了辅助证明规则，其在断言的经典部分中支持标准逻辑运算，并且在量子部分中支持超算子应用。最后，一系列实际的量子算法，特别是整个算法的Shor的因式分解，形式化验证，以显示逻辑的有效性。
2021-04-30 cs.LO quant-ph
A Genetically Modified Hoare Logic
在对基因网络建模时，一个重要的问题在于参数的识别，即使我们考虑一个纯粹的离散框架作为René Thomas的框架。在这里，我们感兴趣的是与基因网络的观察行为一致的所有参数值的穷举搜索。在这篇文章中，我们提出了一种新的方法，霍尔逻辑和最弱的前提演算的基础上产生的可能的参数值的约束。观察到的行为的经典霍尔逻辑的“程序”的作用，和计算的最弱的先决条件表示的所有兼容的参数化表示为参数的约束。最后给出了基因网络霍尔逻辑的正确性证明以及基于最弱前提计算的完备性证明。
2015-06-19 cs.CE cs.LO
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
该研究通过谓词变换器和TopKAT视角分析多种霍尔类逻辑，构建其关系分类法并关注不同程序假设下的关联，还首次得到里斯本逻辑的TopKAT刻画。
2024-11-28 cs.LO cs.PL
Reasoning about call-by-value: a missing result in the history of Hoare's logic
我们提供了一个健全的和相对完整的Hoare-like证明系统的推理部分正确性的递归过程中存在的局部变量和按值调用参数机制，其中的正确性证明是线性的程序长度。我们认为，尽管事实上，霍尔样证明系统的递归程序进行了深入研究，没有这样的证明系统已被提出在文献中。
2019-09-13 cs.LO cs.PL
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
该研究提出渐进精确逻辑，通过新的渐进验证定义和精确逻辑渐进化，统一霍尔逻辑、不正确性逻辑与渐进验证，为同时开发验证、错误查找工具提供基础。
2024-11-30 cs.LO cs.PL
A Hoare logic for the coinductive trace-based big-step semantics of While
在寻找一个基本的框架，推理可观察到的行为的程序，可能不会终止，我们以前设计了一个基于跟踪的大步骤的语义虽然。在这种语义中，轨迹和评估（将程序运行的初始状态与它们产生的轨迹相关联）都是共归纳定义的。在终止运行时，这种语义与标准的基于归纳状态的语义一致。在这里，我们提出了一个霍尔逻辑对应我们的共归纳基于迹的语义，并证明它的声音和完整的。我们的逻辑包括标准的部分正确性状态为基础的霍尔逻辑以及总正确性的变化：他们是可嵌入的。在相反的方向上，投影可以被构造：在我们的基于迹的逻辑中的霍尔三元组的推导可以被转换为在基于状态的逻辑中的转换的、较弱的霍尔三元组的推导。由于我们使用的是建设性的底层逻辑，因此我们可以推理的程序属性范围具有良好的结构;特别是，我们可以区分终止性和非发散性，例如，无界经典全搜索不能终止，但仍然是无发散的。我们的元理论也是完全建设性的，我们已经在Coq中将其形式化了。
2015-02-08 cs.LO cs.PL
Tutorial implementation of Hoare logic in Haskell
使用程序设计语言Haskell，我们介绍了命题演算，数论和一个简单的命令式语言，可以评估算术和布尔表达式的实现。最后，我们提供了一个实现霍尔的逻辑，这将使我们能够推断事实的程序，而不需要一个完整的评估。
2021-12-26 cs.LO cs.PL
A Hoare-like logic of asserted single-pass instruction sequences
我们提出了一个正式的系统证明的部分正确性的单遍指令序列考虑在程序代数分解成部分正确性的证明单遍指令序列的有关部分。该系统类似于霍尔逻辑，但是考虑到由于跳转指令的存在，单遍指令序列的段可以具有多个入口点和多个出口点。它旨在支持对低级程序设计语言的Hoare类逻辑问题的全面理解。
2017-05-03 cs.LO cs.PL
Relational Parametricity and Separation Logic
分离逻辑是霍尔逻辑的一个新的扩展，用于推理引用共享可变数据结构的程序。在本文中，我们提供了一个新的解释逻辑的程序设计语言具有更高的类型。我们的解释是基于雷诺的关系参数化，它提供了一个正式的连接之间的分离逻辑和数据抽象。
2008-05-15 cs.LO
Cyclic Proofs in Hoare Logic and its Reverse
University College London（伦敦大学学院）；Tohoku University（东北大学）
本文研究了霍尔逻辑及其逆向逻辑的循环证明系统，探讨了其正确性条件及与公理化系统的转换关系。
2026-02-27 cs.LO cs.PL
A Hoare Logic with Regular Behavioral Specifications
我们提出了一个霍尔逻辑，扩展程序规范与正则表达式，捕获的行为在执行过程中出现的事件序列。这个想法类似于会话类型或类流程行为契约，这是两个目前流行的研究方向。这里提出的方法在表现力和证明自动化之间取得了特定的平衡，值得注意的是，它可以在多次循环迭代中捕获有趣的顺序行为。该方法是模块化的，并与自动演绎验证工具集成良好。我们描述和演示我们的原型实现SecC使用两个案例研究：匹配的电子邮件地址和规范的游戏步骤中的VerifyThis赌场的挑战。
2022-05-13 cs.FL cs.LO
Deciding KAT and Hoare Logic with Derivatives
带测试的Kleene代数（KAT）是布尔代数（BA）和正则表达式代数Kleene代数（KA）的结合，是一个用于程序验证的方程系统。特别地，KAT包含了霍尔逻辑（PHL）的命题片段，该逻辑是用于程序的规范和验证的形式化系统，并且是当前大多数用于检查程序正确性的工具的基础。KAT的方程理论和PHL在KAT中的编码都是可判定的。在本文中，我们提出了一个新的决策过程的基础上的概念偏导数的两个KAT表达式的等价性。我们还介绍的概念，衍生模特定的方程组。有了这个，我们扩展了以前的程序来决定PHL。最后给出了一些实验结果。
2012-10-09 cs.FL cs.LO
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
具有寄存器和语音的交互式系统（简称“rv系统”）是一种用于交互式计算的模型，该模型相对于时空对偶变换获得了闭寄存器机（“语音”是“寄存器”的时间对偶对应物）。同样的，AGAPIA v0.1，一种用于rv系统的结构化程序设计语言，是经典while程序（针对特定类型的数据）的时空对偶闭包。典型的AGAPIA程序描述了位于不同地点的开放过程，并具有对环境做出适当反应的时间窗口。该语言自然地支持流程迁移、结构化交互和在异构机器上部署组件。本文介绍了一种用于验证AGAPIA v0.1程序的类Hoare时空逻辑。作为一个案例研究，一个流行的分布式终止检测协议的形式化验证证明。
2008-10-19 cs.LO cs.PL
A Relational Program Logic with Data Abstraction and Dynamic Framing
饰Tony Hoare霍尔在1972年发表的一篇论文中阐述了隐藏不变量和模拟的基本概念。隐藏：封装数据表示的不变量不需要在包含模块API的规范中提及。模拟：可以通过使用封装状态上定义的耦合关系证明旧实现和新实现之间的模拟来确定新数据表示和实现的正确性。这些结果在语义上被形式化，并且是针对一个简单的状态模型，尽管该论文声称这可以扩展到包含动态分配的对象。近年来，已经取得了进展，正式的索赔，模拟，虽然主要是在语义的发展。在这篇文章中，隐藏和模拟结合了Hoare 1969年论文中的思想：程序逻辑。对于一个基于对象的语言与动态分配，我们引入了一个关系霍尔逻辑与状态框架条件，形式化封装，隐藏的不变量，和耦合，涉及两个实现。关系和其他断言用一阶逻辑表示。规范可以表达广泛的关系属性，如条件等价和不干扰解密。证明规则通过方便的对齐来促进关系推理，并且相对于传统的操作语义被示出为合理的。导出的链接程序等价性证明规则直接体现了表示独立性。具有代表性的例子的适用性证明使用基于SMT的实现。
2022-07-19 cs.LO cs.PL
A Practical Quantum Hoare Logic with Classical Variables, I
Centre for Quantum Software and Information, University of Technology Sydney（悉尼科技大学量子软件与信息中心）
本文提出一种量子程序验证的霍尔逻辑，支持经典变量，改进了表达能力、规范清晰度和证明系统简化，便于量子程序验证。
2026-04-18 cs.LO cs.PL quant-ph
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More
最近，作者提出了下近似逻辑推理的程序。到目前为止，所有这些逻辑都局限于对单个程序行为的推理。然而，存在许多过度近似的关系逻辑，用于对程序对进行推理并将其行为关联起来。我们提出了第一个下近似关系逻辑，简单的命令式语言IMP。我们证明了我们的逻辑是健全的和完整的。此外，我们展示了如何在这个逻辑推理可以分解成非关系推理下近似霍尔逻辑，反映Beringer的结果过近似的关系逻辑。我们说明了我们的逻辑在一些小的例子中，我们证明了不安全的存在。
2020-03-11 cs.LO
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
本文提出一种扩展一阶逻辑，以 Hoare 三元组风格对抽象状态进行推理，并通过可实现性解释将证明提取为混合函数式/命令式程序，同时给出基于状态单子的语义解释及 Heyting 算术单子扩展。
2024-01-25 cs.LO math.LO
On Hoare-McCarthy algebras
我们讨论了一个代数方法命题逻辑的副作用。为此，我们使用霍尔的条件[1985]，这是一个三元连接可比的if-then-else。从麦卡锡的概念顺序评价[1963年]，我们讨论了一些价值的同余，我们介绍Hoare-McCarthy代数的结构，这些同余的特点。
2010-12-22 cs.LO math.LO
