Refinement orders for quantum programs
Tsinghua University（清华大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
本文研究了量子程序的细化顺序，揭示了不同规范类型与经典域论概念的对应关系，以及确定性和非确定性程序的细化特性。
2026-02-19 cs.LO quant-ph
Toward Automatic Verification of Quantum Programs
本文总结了作者和他的合作者在量子程序的程序逻辑验证方法中所获得的结果，包括量子Hoare逻辑，量子程序的不变量生成和终止分析。为了更方便地对量子程序进行推理，还引入了证明大纲的概念和一些辅助规则。文章最后提出了今后研究的一些问题。
2018-07-31 cs.LO quant-ph
Responsibility and verification: Importance value in temporal logics
我们的目标是测量系统的一部分，它的能力，以满足规格的不确定性的选择的影响。为此，我们应用Shapley值的概念来验证作为一种手段来评估系统的一部分是多么重要。组件的重要性是通过将其控制权单独或与其他组件一起交给对手，并测试系统是否仍然可以满足规范来衡量的。我们研究这个想法的框架中的模型检查与各种经典类型的线性时间规范，并提出了几种方法来转置分支。我们还提供了严格的复杂性界限，几乎在每一种情况下。
2021-04-20 cs.LO
symQV: Automated Symbolic Verification of Quantum Programs
我们提出了symQV，一个符号执行框架，用于在量子线路模型中编写和验证量子计算。symQV可以自动验证量子程序是否符合一阶规范。我们正式介绍了一个符号量子程序模型。这允许在SMT公式中编码验证问题，然后可以使用delta-完全决策过程进行检查。我们还提出了一个抽象技术，以加快验证过程。实验结果表明，该抽象将symQV的可扩展性提高了一个数量级，可以扩展到具有24个量子比特（2^24维状态空间）的量子程序。
2022-12-05 cs.LO quant-ph
Verification of Quantum Programs
本文发展了量子程序的验证方法学，其贡献有两个方面：1。Sharir，Pnueli and Hart [SIAM J. Comput. 13（1984）292 - 314]提出了一种证明概率程序性质的一般方法，该方法用马尔可夫链对概率程序进行建模，并将关于输出分布的断言扩展为关于所有中间分布的不变断言。他们的方法本质上是经典弗洛伊德归纳断言方法的概率推广。在本文中，我们考虑的量子程序模型的量子马尔可夫链的超算子定义。它表明，Sharir-Pnueli-Hart方法可以优雅地推广到量子程序，利用薛定谔-海森堡对偶量子态和可观测量。特别地，建立了量子程序的Sharir-Pnueli-Hart验证方法的完备性定理。2.正如完备性定理所指出的，Sharir-Pnueli-Hart方法原则上对于验证量子程序的所有性质都是有效的，这些性质可以用厄米算符（可观测量）来表示。但由于验证过程中涉及的计算复杂，在许多实际应用中并不可行。对于有限维状态空间的情形，我们利用超算子的矩阵表示和矩阵的Jordan分解，找到了一种比Sharir-Pnueli-Hart方法简单得多的量子程序验证方法.特别是，这种方法使我们能够很容易地计算平均运行时间，甚至可以分析量子程序在有限维状态空间中的一些有趣的长期行为。
2011-06-21 cs.LO quant-ph
Proof complexity of systems of (non-deterministic) decision trees and branching programs
本文研究命题证明系统中的行序列的决策树或分支程序-确定性和非确定性。系统LDT和LNDT是命题证明系统，其中线表示确定性或非确定性决策树。分支程序被建模为决策dags。将扩展添加到LDT和LNDT给出系统eLDT和eLNDT，其中行分别表示确定性和非确定性分支程序。确定性和非确定性分支程序分别对应于对数空间（L）和非确定性对数空间（NL）。因此系统eLDT和eLNDT是用（非一致）L和NL属性推理的命题证明系统。本文的主要结果是仿真和非仿真结果的树型和dag样的证明系统LDT，LNDT，eLDT，和eLNDT。并与Frege系统、常深度Frege系统和扩展Frege系统作了比较
2019-10-18 cs.CC cs.LO math.LO
Bounded Model Checking for Asynchronous Hyperproperties
对机密性的许多类型的攻击源于计算机程序在其中操作的环境的不确定性（例如，同步器和异步通信信道）。在本文中，我们专注于验证的机密性在不确定性环境中的异步超属性的推理。首先，我们概括的时间逻辑A-HLTL允许嵌套的轨迹量化，其中的轨迹确定不同的执行轨迹可能会推进和口吃。我们提出了一个有界的模型检验算法A-HLTL的基础上QBF解决的一个片段的广义A-HLTL和评估并发程序，调度攻击，编译器优化，投机执行，和缓存定时攻击的各种案例研究。我们还严格分析了A-HLTL不同片段的模型检验的复杂性。
2023-01-26 cs.LO
Combining nondeterminism, probability, and termination: equational and metric reasoning
我们研究单子的组合产生的不确定性和概率行为的可能性终止，这是必不可少的程序语义。我们的主要贡献是单子的演示结果，提供等式推理工具，建立等价和距离的程序。
2021-04-21 cs.LO
The Epistemology of Nondeterminism
本文提出了新的语义不确定性程序执行，取代命题动态逻辑（PDL）的标准关系语义。在这些新语义下，程序执行被表示为基本上确定性的（即，功能性），而非决定论则表现为主体与系统之间的认识关系：直观地说，给定过程的非决定性结果恰恰是那些不能事先排除的结果。我们正式这些概念使用拓扑和动态拓扑逻辑（DTL）的框架。我们表明，DTL可以用来解释的PDL语言的方式，捕捉上面的直觉，而且，在这种设置中的连续功能完全对应于确定性的过程。我们还证明了某些公理化的PDL保持健全和完整的动态拓扑模型的相应类别。最后，我们使用子集空间逻辑机制扩展了该框架以纳入知识，并表明公告的拓扑解释与测试程序的自然解释完全一致。
2018-03-22 cs.LO
Extracting total Amb programs from proofs
Swansea University（斯旺西大学）；Kyoto University（京都大学）
本文提出CFP逻辑系统，用于从证明中提取可证明总正确性的非确定性和并发程序，通过域论语义验证提取程序的正确性，并展示了一个将无限Gray码转换为符号数字表示的非确定性程序。
2026-10-26 cs.LO
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
本文提出一个范畴框架，通过denotational积构造将效应高阶程序的线性时间安全性验证归约为最弱前置条件计算，并实现了首个支持递归概率高阶程序的自动化验证器。
2025-10-17 cs.LO
Graph Based Reduction of Program Verification Conditions
在C程序的演绎验证中，提高证明的自动性是一项具有挑战性的任务。当应用于工业C程序时，已知的生成更简单的验证条件的方法不够有效。这主要是由于它们的规模和大量不相关的假设。这项工作提出了一种策略，以减少程序验证条件，通过选择其相关的假设。一个假设的相关性是由一个句法分析和两个图形遍历的组合来确定的。第一个图用常数标记，第二个图用公理中的谓词标记。该方法被应用于工业程序验证中产生的基准。
2009-07-08 cs.LO
The Semantics of Graph Programs
GP（图形程序）是一种基于规则的、非确定性的程序设计语言，用于在高抽象级别上解决图形问题，使程序员从处理低级别的数据结构中解放出来。GP的核心由四个结构组成：一组条件图转换规则的单步应用，顺序组合，分支和迭代。我们提出了一个形式化的语义GP的结构操作语义的风格。我们的语义的一个特殊功能是使用失败的程序来定义GP的强大的分支和迭代命令。
2010-03-24 cs.LO cs.PL
Automated Verification of Silq Quantum Programs using SMT Solvers
本文提出自动化工具 SilVer，通过量子 RAM 式编程模型连接 Silq 程序与 SMT 证明义务，支持经典/量子条件及测量标志规约，并以纠缠态和 oracle 算法案例验证其有效性。
2024-06-05 cs.LO cs.SE quant-ph
VerifyThis 2019: A Program Verification Competition (Extended Report)
Verify这是一系列程序验证比赛，强调人的方面：参与者解决详细行为属性的验证-超出全自动验证的能力，需要人类的专业知识来适当编码程序，规范和不变量。本文介绍了在布拉格举行的ETAPS 2019上举行的第8版VerifyThis。13个团队参加了比赛，其中包括三个核查挑战，跨越两天的工作。该报告分析了参赛团队如何应对这些挑战，反映了什么使验证挑战或多或少适合典型的VerifyThis参与者，并概述了在专注于人的方面的竞争中比较使用不同验证方法的团队工作的困难。
2021-05-18 cs.LO
A New Method of Verification of Functional Programs
本文研究了字符串上函数程序的验证问题，其中函数程序的性质规范由其它函数程序定义，一个函数程序S1满足另一个函数程序S2定义的规范当且仅当由函数程序S1和S2定义的函数的组合等于常数1.我们引入了一个FP的状态图的概念，并减少了验证问题的FP的状态图的分析问题。所提出的方法是说明了一个排序程序的验证的例子。
2016-04-14 cs.LO
Verification of MPI programs
在本文中，我们概述了一种方法来验证并行程序。介绍了一种新的并行程序数学模型。通过矩阵乘法MPI程序的验证，说明了所引入的模型。
2021-10-16 cs.LO cs.PL
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
反应式程序在现代应用中无处不在，因此验证是非常必要的。我们提出了一个验证策略的反应程序与一个大的或无限的状态空间，利用代数法的反应关系。我们定义了新的运营商来描述相互作用和状态更新，以及相关的方程理论。有了这个，我们可以计算一个反应式程序的指称语义，从而促进自动证明。值得注意的是，我们的推理支持迭代程序与反应不变式，这是支持Kleene代数。我们通过验证反应缓冲区来说明我们的策略。我们的法律和战略在Isabelle/UTP中实现了机械化，提供了可靠的保证和实际的验证支持。
2018-08-07 cs.LO
Craig Interpolation in Program Verification
University of Regensburg（雷根斯堡大学）；Uppsala University（乌普萨拉大学）
该章节介绍程序验证领域中Craig插值技术的近年进展，聚焦插值模理论与数据类型的推导、插值验证算法的基础设计两大方向，服务于循环不变量推断等自动化验证任务。
2026-02-09 cs.LO
Practical Deductive Verification of OCaml Programs (Extended Version)
本文提供使用 GOSPEL 规范语言和 Cameleer 工具对 OCaml 程序进行演绎验证的实践教程，涵盖纯函数式与命令式两类程序，实现大部分自动化验证。
2024-07-20 cs.LO
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
我们展示了如何自动工具的验证线性和分支的时间属性的程序，多线程，和功能的程序，以及程序合成可以自然地和统一地被视为求解器的约束条件的形式（量化）霍恩条款的背景逻辑理论。这样的观点可以提供各种优势，例如。例如，在一个实施例中，约束生成（也称为证明义务的生成）和约束求解（也称为证明发现）之间的关注点的逻辑分离、跨不同验证任务的求解器的重用、以及证明设计者从低级算法关注点中解放出来，反之亦然。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-29 cs.LO
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
本卷包含第三届程序等价和关系推理研讨会（PERR）和第六届验证与综合霍恩子句研讨会（HCVS）的联合后续会议记录，分别于4月6日和7日在捷克共和国布拉格举行，作为ETAPS的附属研讨会。
2019-07-08 cs.LO
A Program Instrumentation Framework for Automatic Verification
针对后端求解器难以处理部分规约语言结构的验证问题，提出统一的程序插桩验证范式，实现于MonoCera工具，可自动处理含数组量化、聚合操作的程序验证，并在含SV-COMP程序的样例上完成评估。
2024-12-09 cs.LO
Debugging Program Verification Proof Scripts (Tool Paper)
交互式程序验证的特征在于未完成的证明尝试的迭代。为了支持构造完整证明的过程，许多交互式程序验证系统提供证明脚本语言作为基于文本的方式来描述证明中的非自动步骤。这样的脚本语言是有益的，但是用户花费了大量的精力来检查证明脚本和他们构造的证明，以在证明尝试不成功并导致意外的证明状态时检测原因。我们提出了一个离线和重放调试器，以支持用户分析证明脚本执行的证明尝试。该调试器将成功的概念从软件调试应用到证明脚本调试领域。该工具是建立在KeY之上的，KeY是一个用于Java程序演绎验证的系统。调试器及其图形用户界面的设计，以支持程序验证特别是，底层的概念和实现，但是，适用于其他证明和证明任务。
2018-04-12 cs.LO
Partial Automation of Verification Condition Proving for Reflex Programs (Draft)
Novosibirsk State University（新西伯利亚国立大学）；Institute of Automation and Electrometry（自动化与电磁学研究所）
针对Reflex语言验证条件过多导致手动证明不可行的问题，提出通过引入注解语言、基于程序结构生成不变量以及使用SMT求解器来自动化部分验证条件的证明。
2026-06-23 cs.LO
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
我们报告的工作进展自动程序证明性能的程序写在高阶函数语言。我们的方法编码高阶程序直接作为一阶SMT问题的霍恩条款。将一阶程序的Hoare式验证简化为Horn子句的可满足性是很直接的。闭包的存在带来了一些挑战：相对完整的证明系统必须考虑闭包;在实践中，搜索过程的有效性取决于编码策略和底层求解器的能力。我们在这里使用代数数据类型来编码闭包，并依赖于支持代数数据类型的求解器。该方法的可行性进行检查使用的例子从文献中高阶程序验证。
2013-06-21 cs.LO
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
概率程序验证的基本任务包括约束期望结果和证明有限期望运行时间内的终止性。我们贡献了一个简单而有效的归纳合成方法，证明这种定量的可达性属性生成归纳不变的源代码级。我们的实施显示了承诺：它为有限状态程序找到不变量，可以击败最先进的概率模型检查器，并且与致力于不变量合成和预期运行时推理的现代工具竞争。
2023-02-08 cs.LO
Proceedings Seventh International Workshop on Verification and Program Transformation
本卷包含第七届验证和程序转换国际研讨会（VPT 2019）上提交的论文的最终和修订版，该研讨会于2019年4月2日在意大利热那亚举行，隶属于Programming 2019。
2019-08-16 cs.LO cs.PL
External Behavior of a Logic Program and Verification of Refactoring
本文为一种简单回答集编程语言精确定义外部行为，并提出一个证明助手来验证程序重构的正确性。
2023-05-27 cs.LO
Sharper and Simpler Nonlinear Interpolants for Program Verification
联合不可行谓词的插值在不变量综合、CEGAR等程序验证技术中起着重要的作用。Dai等人最近的研究结果引起了我们的兴趣。结合实代数几何和SDP优化的多项式插值综合方法，本文对该方法进行了改进，得到了更尖锐、更简单的插值。增强是可能的：在真正的代数几何的理论观察;和我们继续分数为基础的算法，四舍五入（潜在的错误）的SDP求解器的数值解。实验结果支持我们的工具的有效性，我们也证明了尖锐和简单的插值程序验证的例子中的好处。
2017-09-01 cs.LO
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
有界验证已被证明是有用的，以检测错误，并增加在程序的正确性的信心。与无界验证相比，通过（有界）内联进行调用和通过（有界）展开进行循环的推理不需要方法规范和循环不变式，因此将注释开销降低到最低限度，即要验证的属性的规范。对于基于传统程序逻辑的验证器，通过内联（和展开）来保存验证：成功的程序w.r.t.某些注释意味着内联程序的成功验证。也就是说，在内联程序中检测到的任何错误都揭示了原始程序中的真正错误。但是，这个基本属性可能不适用于自动分离逻辑验证器，如Caper、GRASShopper、RefinedC、Steel、VeriFast和基于Viper的验证器。在这种情况下，内联通常会更改方法执行所拥有的资源，这可能会影响自动证明搜索算法并引入虚假错误。在本文中，我们提出了第一种技术，验证保持内联自动分离逻辑验证。我们确定了一个语义条件的程序，并证明在Isabelle/HOL，它确保了验证保持内联的最先进的自动分离逻辑验证。我们还证明了一个双重结果：成功验证的内联程序，确保有方法和循环注释，使验证的原始程序有界执行。为了自动检查我们的语义条件，我们提出了两个近似，可以检查语法和程序验证器，分别。我们实现这些检查毒蛇，并证明他们是有效的非平凡的例子，从不同的验证。
2023-03-13 cs.LO
A benchmark for C program verification
我们提出了25个C程序，作为C程序验证使用形式化方法的基准。该基准测试可用于系统演示、系统间验证工作的比较，以及作为一种友好的竞争。对于最后一个目的，我们给出了一个评分公式，允许验证系统得分高达一百分。
2019-04-01 cs.LO cs.PL
From Well Structured Transition Systems to Program Verification
我们描述了使用的WSTS理论验证程序。
2020-08-07 cs.FL cs.LO
Generating Loop Invariants for Program Verification by Transformation
循环不变量在命令式程序的验证中起着核心作用。然而，找到这些不变量对于程序员来说通常是一项困难且耗时的任务。我们以前已经展示了如何程序转换可以用来促进功能程序的验证，但由于需要发现这些循环不变量，命令式程序的验证更具挑战性。在本文中，我们描述了一种自动发现循环不变量的技术。我们的方法类似于归纳迭代法，但避免了使用这种方法和其他方法时可能导致的子句中的潜在指数爆破。我们的方法利用了简化程序转换算法将子句转换为简化形式，便于识别它们之间的相似性和差异性，从而帮助发现不变量。我们证明，我们的技术终止，并证明其成功的应用程序，已被证明是有问题的使用其他方法的例子。我们还讨论了我们的技术未能找到一个不变的情况下，并显示如何可以改善到一定程度。
2017-08-24 cs.LO
Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems
我们给出了“基于知识的程序”的关系和最弱前提语义，即，限制变量的可观测性的程序，以便丰富地表达能够或不能观测所述变量的代理的知识的变化。基于这些知识为基础的程序，我们定义了一个程序的认知逻辑模型复杂的认知属性的多智能体系统的执行。我们翻译的有效性程序认知逻辑公式的一阶有效性，使用我们最弱的前提语义和巧妙的簿记变量分配。我们在Haskell中以一般的方式实现我们的翻译（即，独立于逻辑语句中的程序），并在一系列行之有效的例子上测试我们的新程序-认知逻辑的这种新颖的验证方法。
2022-07-06 cs.LO
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
最优性准则下参数马尔可夫决策过程的多目标验证问题可以自然地表示为非线性规划问题。我们观察到，许多这些计算要求的问题属于子类的符号程序。这种洞察力允许顺序优化算法有效地计算合理但可能次优的解决方案。该算法的每一步都解决了一个几何规划问题。这些几何规划是通过凸化原问题的非凸约束得到的。编码作为非线性程序的直接应用是模型修复和参数综合。我们证明了我们的方法的可扩展性和质量由著名的基准
2017-01-26 cs.LO
Efficient verification of imperative programs using auto2
Auto 2是最近为证明助手Isabelle引入的证明器。它被设计为既可以从Isabelle内部高度定制，又具有强大的证明搜索机制。本文将auto 2应用于命令式程序的验证。我们描述了两个阶段的证明过程中的自动2的设置：验证的功能版本的程序，并使用分离逻辑完善的命令式版本。作为例子，我们验证了几个数据结构，包括红黑树，区间树，优先级队列，和union-find。我们还验证了几个算法利用这些数据结构。这些例子表明，我们的框架是能够有效地验证复杂的算法，并在一个模块化的方式。
2018-02-24 cs.LO
Comparison between CPBPV, ESC/Java, CBMC, Blast, EUREKA and Why for Bounded Program Verification
Université de Nice–Sophia Antipolis（尼斯-索菲亚安提波利斯大学）；Brown University（布朗大学）
本报告描述了一组基准程序验证的实验结果。它比较了CPBVP“有界程序验证的约束编程框架”[4]与以下框架的能力：ESC/Java，CBMC，Blast，EUREKA和Why。
2008-08-11 cs.AI cs.LO cs.SE
A Deductive Verification Framework For Higher Order Programs
在本报告中，我们介绍了为我们的APDC（Area Prática de Desenvolvimento Curriculum）课程研究项目开展的初步工作。这个项目的主要目标是开发一个框架，在Why3工具之上，用于验证有效的高阶程序。我们使用去功能化作为从高阶OCaml实现到一阶OCaml实现的中间转换。我们翻译的目标是WhyML，Why3的程序设计语言。我们相信去功能化可以是一个有趣的路线，高阶程序的自动验证，因为人们可以采用现成的自动程序验证器来证明所生成的一阶程序的正确性。这份报告还向读者介绍了演绎程序验证的主题，以及用于证明高阶有效程序的一些工具和概念。
2020-11-28 cs.LO cs.PL
Modular Verification of Recursive Programs
我们认为，递归程序的C.A.R.断言方法的手段，验证。霍尔可以使用模块化推理在概念上简化。在这种方法中，程序的一些属性首先被建立，然后被用来建立其他程序属性。我们说明了这种方法，通过提供一个模块化的正确性证明的快速排序程序。
2009-07-24 cs.LO cs.PL
Program Verification of Numerical Computation - Part 2
这些说明提出了一些扩展的形式化方法在早期的文件中介绍。形式化方法被设计为数值计算程序验证的工具，并形成了软件包VPC的基础。这里介绍的扩展中包括用于检测不可计算程序的析取和方法。更全面的列表的建设规则，更高的秩序建设也提出。
2014-11-20 cs.LO cs.MS
Software Verification for Weak Memory via Program Transformation
尽管多处理器实现弱内存模型，验证方法往往假设顺序一致性（SC），因此可能会错过错误，由于弱内存。我们提出了一个健全的改造方案进行验证，使SC工具进行验证w.r.t.记忆力差我们提出了各种各样的模型（从x86/TSO到Power/ARM）和各种各样的验证工具的实验，量化了转换的额外成本，并强调了我们可以大幅降低它的情况。
2012-07-30 cs.LO cs.SE
CPBVP: A Constraint-Programming Framework for Bounded Program Verification
Université de Nice–Sophia Antipolis（尼斯大学-索菲亚安提波利斯大学）；Brown University（布朗大学）
研究了如何验证程序是否符合其规范，提出了一种新的约束编程有界程序验证框架（CPBPV）。CPBPV框架使用约束存储来表示规范和程序，并不确定地探索执行路径。如果这样产生的每个约束存储都隐含后置条件，则输入程序是部分正确的。CPBPV不会探索虚假的执行路径，因为它通过检测约束存储不一致来提前增量地修剪执行路径。CPBPV使用约束编程的丰富语言来表示约束库。最后，CPBPV是参数化的求解器，这些求解器按顺序尝试，从最便宜和不太通用的开始。实验结果往往产生数量级的改进，较早的方法，运行时间往往是独立的变量域。此外，CPBPV能够检测到一些程序中的细微错误，而其他基于模型检验的框架则失败了。
2008-07-15 cs.AI cs.LO cs.SE
What's Decidable About Program Verification Modulo Axioms?
我们考虑程序验证问题的可判定性\emph{modulo axioms} --即，当程序使用的函数和关系假设由满足一组一阶公理的任意函数和关系解释时，验证程序是否满足其断言。不幸的是，完全未解释的程序（使用空公理集）的验证已经是不可判定的。最近的工作介绍了一个子类的\emph{coherent}未解释的程序，并表明，他们承认可判定的验证\cite{coherence2019}。我们进行了系统的研究，各种自然公理的关系和功能，并研究的一致性验证问题的可判定性。公理包括关系是自反的、对称的、传递的、或全序关系，%和它们的组合，函数被限制为结合的、幂等的或交换的，以及这些公理的组合。我们的综合研究结果揭示了一个丰富的景观，表明虽然几个公理类承认连贯性程序的可判定性，连贯性不是灵丹妙药，因为其他几个仍然是不可判定的。
2019-10-28 cs.LO cs.PL
Local verification of global proofs
在这项工作中，我们研究了分布式验证的本地和全局证明的成本。在这种设置中，分布式系统的节点被提供了系统状态正确性的非确定性证明，并且节点需要通过仅查看系统中的局部邻域来验证该证明。以前的作品已经研究了模型，其中每个节点都有自己的，可能是唯一的，部分证明作为输入。校样的成本是单个标签的最大尺寸。我们将此模型与每个节点都可以访问相同的全局证明的模型进行比较，并且成本是此全局证明的大小。很容易看出，一个全局证明总是可以包含所有的局部证明，并且每个局部证明都可以是全局证明的副本。我们表明，存在的属性，表现出这些相对的证明大小，也属性介于两者之间。此外，我们引入了一个新的下界技术，并使用它来证明一个严格的下界的复杂性逆转分布式决策和建立之间的联系通信复杂性和分布式证明复杂性。
2018-03-26 cs.DC cs.LO
Efficient Verification of Concurrent Programs Over TSO Memory Model
我们解决的问题，多线程程序运行在总存储顺序（TSO）内存模型的有效验证。它已被证明，即使有限的数据域程序，控制状态可达下TSO的复杂性是非原始递归。在本文中，我们首先提出了一种有界缓冲区验证方法，其中缓冲区的大小上的界限放置，验证是递增地进行，通过增加的缓冲区的大小与验证过程的每次迭代，直到达到所述的界限。对于有限数据域上的程序，我们还证明了存在一个缓冲区的界限K，如果该程序是安全的，那么它也是安全的无界缓冲区。我们已经实现了这种技术在一个工具ProofTraPar。我们的结果对memorax [2]，一个国家的最先进的声音和完整的验证TSO记忆模型，一直令人鼓舞。
2016-06-17 cs.LO cs.PL
The WhyRel Prototype for Relational Verification
程序之间的互操作关系在各种验证环境中作为一项任务出现，例如优化转换，将新版本的程序与旧版本（回归验证）和不干扰。然而，现有的工具，它提供了一个高水平的自动化的成本限制的程序考虑的关系验证的程序动态分配的可变状态的支持并不好。另一方面，自动激活工具需要更多的用户交互，但可以验证更广泛的程序类别。本文介绍了WhyRel，一个基于关系区域逻辑的指针程序关系属性自动验证工具。WhyRel通过验证案例研究进行评估，依赖于由Why3平台编排的SMT求解器。案例研究包括建立表示独立的ADT，显示不干扰，并从最近的文献挑战的问题。
2023-03-25 cs.LO cs.PL
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
本文为含循环、连续分布和条件化的概率程序验证奠定基础，通过黎曼和近似积分实现SMT不变量验证，并证明收敛性与完备性，且可在现有工具中应用。
2025-02-26 cs.LO cs.PL
Algorithmic Verification of Asynchronous Programs
异步编程是一种无处不在的系统编程习惯，用于管理与环境的并发交互。在这种风格中，程序员不是等待耗时的操作完成，而是对操作进行非阻塞调用，并将回调任务发布到任务缓冲区，该任务缓冲区稍后在耗时的操作完成时执行。协作调度器通过从任务缓冲区中挑选并执行回调任务来协调交互（这些回调可以发布更多的回调以供稍后执行）。编写正确的异步程序是困难的，因为回调的使用虽然有效，但模糊了程序控制流。我们提供了一个形式化的异步程序模型，并研究了这个模型的验证问题。我们证明了有限数据异步程序的安全验证问题是expspace完备的。我们证明了有限数据异步程序的活性验证是可判定的，并且多项式时间等价于Petri网的可达性。可判定性并不明显，因为即使数据是有限状态的，异步程序也构成了无限状态转换系统：挂起的异步调用的程序堆栈和任务缓冲区都可能是无限的。我们的主要技术结构是一个多项式时间的语义保持减少从异步程序的Petri网，反之亦然。这种简化允许在Petri网上使用算法技术来验证异步程序。我们还研究了几个扩展的异步程序的基本模型的灵感来自异步库的实现提供的额外功能，并分类这些扩展的验证问题的可判定性和不可判定性。
2011-11-14 cs.FL cs.LO
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Institute of Information Science, Academia Sinica（中央研究院資訊科学研究所）；Graduate Institute of Electronics Engineering, National Taiwan University（国立台湾大学电子工程学研究所）；Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）
本文提出了一种扩展的集合基规范语言和转换算法，通过控制自动机构造和量子位重排，实现线性复杂度的量子程序自动验证。
2026-05-07 cs.FL cs.LO
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
Verification of Object-Oriented Programs: a Transformational Approach
我们表明，验证面向对象的程序，通过断言的方法，可以实现在一个简单的方式，通过利用一个语法导向的转换，从面向对象的程序递归程序。这种转换表明自然的证明规则和它的正确性，帮助我们建立健全和相对完整的证明系统。困难之一是如何在断言语言中正确处理实例变量和别名。所讨论的程序设计语言支持数组、实例变量、失败和带参数的递归方法。
2011-11-08 cs.LO cs.PL
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
本文提出将程序插桩作为统一验证范式，以自动变换方式消除规约语言中后端求解器难以处理的结构，并将数组聚合形式化为幺半群同态，在 MonoCera 工具中实现并验证其有效性。
2023-05-26 cs.LO cs.SE
Proceedings of the Third International Workshop on Verification and Program Transformation
本卷包含2015年4月11日在英国伦敦举行的第三届验证和程序转换国际研讨会（VPT 2015）上发表的论文。讲习班的前两届讲习班分别于2013年在圣彼得堡（俄罗斯）和2014年在维也纳（奥地利）举行。这些论文表明，在程序转换领域中开发的方法和工具，如部分求值和折叠/展开转换，以及超级编译，可以应用于软件系统的验证。他们还展示了一些程序验证方法，如模型检验技术，抽象解释，SAT和SMT解决，自动定理证明，可以用来增强程序转换技术，从而使这些技术在实践中更强大和有用。
2015-12-06 cs.LO cs.PL cs.SE
