Graph Based Reduction of Program Verification Conditions
在C程序的演绎验证中，提高证明的自动性是一项具有挑战性的任务。当应用于工业C程序时，已知的生成更简单的验证条件的方法不够有效。这主要是由于它们的规模和大量不相关的假设。这项工作提出了一种策略，以减少程序验证条件，通过选择其相关的假设。一个假设的相关性是由一个句法分析和两个图形遍历的组合来确定的。第一个图用常数标记，第二个图用公理中的谓词标记。该方法被应用于工业程序验证中产生的基准。
2009-07-08 cs.LO
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
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
Proceedings Seventh International Workshop on Verification and Program Transformation
本卷包含第七届验证和程序转换国际研讨会（VPT 2019）上提交的论文的最终和修订版，该研讨会于2019年4月2日在意大利热那亚举行，隶属于Programming 2019。
2019-08-16 cs.LO cs.PL
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
A benchmark for C program verification
我们提出了25个C程序，作为C程序验证使用形式化方法的基准。该基准测试可用于系统演示、系统间验证工作的比较，以及作为一种友好的竞争。对于最后一个目的，我们给出了一个评分公式，允许验证系统得分高达一百分。
2019-04-01 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
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
From Well Structured Transition Systems to Program Verification
我们描述了使用的WSTS理论验证程序。
2020-08-07 cs.FL 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
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
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
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 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
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
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
What's Decidable About Program Verification Modulo Axioms?
我们考虑程序验证问题的可判定性\emph{modulo axioms} --即，当程序使用的函数和关系假设由满足一组一阶公理的任意函数和关系解释时，验证程序是否满足其断言。不幸的是，完全未解释的程序（使用空公理集）的验证已经是不可判定的。最近的工作介绍了一个子类的\emph{coherent}未解释的程序，并表明，他们承认可判定的验证\cite{coherence2019}。我们进行了系统的研究，各种自然公理的关系和功能，并研究的一致性验证问题的可判定性。公理包括关系是自反的、对称的、传递的、或全序关系，%和它们的组合，函数被限制为结合的、幂等的或交换的，以及这些公理的组合。我们的综合研究结果揭示了一个丰富的景观，表明虽然几个公理类承认连贯性程序的可判定性，连贯性不是灵丹妙药，因为其他几个仍然是不可判定的。
2019-10-28 cs.LO cs.PL
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
本文提出一个范畴框架，通过denotational积构造将效应高阶程序的线性时间安全性验证归约为最弱前置条件计算，并实现了首个支持递归概率高阶程序的自动化验证器。
2025-10-17 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
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
Compositional Safety Verification with Max-SMT
我们提出了一种基于条件归纳不变量的安全属性自动组合程序验证技术。对于给定的程序部分（例如，一个单一的循环）和一个后置条件$φ$，我们展示了如何使用Max-SMT求解器，一个归纳不变连同一个先决条件可以合成，使先决条件确保有效性的不变量和不变量意味着$φ$。由此，我们建立了一个自下而上的程序验证框架，传播小程序部分的先决条件作为前程序部分的后置条件。该方法从失败中恢复以证明前提的有效性，使用所获得的中间结果来限制搜索空间以进行进一步的证明尝试。由于一次只需要处理小的程序部分，因此我们的方法是可扩展和可分发的。导出的条件可以被看作是程序不同部分之间的隐式契约，从而使增量程序分析成为可能。
2015-08-03 cs.LO
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 Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
本研究提出一种嵌入简单类型高阶逻辑的并发命令式程序建模、验证与转换框架，可支持对交错计算命令式程序模型性质的可靠结构化推理，并通过Peterson互斥算法案例验证了其适用性。
2024-07-14 cs.LO
Operational semantics and program verification using many-sorted hybrid modal logic
Faculty of Mathematics and Computer Science, University of Bucharest（布加勒斯特大学数学与计算机科学学院）
本文提出基于多类型混合模态逻辑的框架，用于描述编程语言操作语义并验证程序正确性，相较于传统方法具有更自然的执行描述和更清晰的语义编码。
2025-11-27 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
Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
本文展示了基于Gospel规范语言，协同使用Ortac、Cameleer和CFML等动态与静态分析工具，对一个非平凡OCaml程序进行验证的案例研究，揭示了不同工具的互补性及规范编写差异。
2024-07-26 cs.LO
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
Lemur: Integrating Large Language Models in Automated Program Verification
Stanford University（斯坦福大学）；VMware Research（威睿研究院）；VMware by Broadcom（博通旗下威睿公司）
本文提出一种将大型语言模型与自动化推理器结合用于自动化程序验证的通用方法，将其形式化为一组转换规则并证明其可靠性，在合成与竞赛基准上取得实际改进。
2024-04-25 cs.AI cs.FL cs.LG
Proceedings Fifth International Workshop on Verification and Program Transformation
本卷包含第五届验证和程序转换国际研讨会（VPT 2017）的会议记录。研讨会于2017年4月29日在瑞典乌普萨拉举行，隶属于欧洲软件理论与实践联合会议（ETAPS）。VPT研讨会系列的目的是提供一个论坛，来自程序转换和程序验证领域的人们可以富有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。在研讨会上宣读了七篇论文。此外，Javier Esparza（德国慕尼黑工业大学）、Manuel Hermenegildo（西班牙马德里IMDEA软件研究所）和Alexey Khoroshilov（俄罗斯莫斯科ISPRAS Linux验证中心）也应邀进行了三次演讲。
2017-08-23 cs.LO cs.PL cs.SE
Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
University of Twente（特温特大学）；TU Delft（代尔夫特理工大学）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出在VerCors中编码弱内存并发的方案，通过扩展原子操作支持并引入协议自动机概念，实现基于许可的分离逻辑，用于验证弱内存并发程序的正确性。
2026-04-22 cs.LO
Verification Logics for Quantum Programs
我们调查景观的霍尔逻辑的量子程序。我们回顾三篇论文：Chadha，Mateus和Sernadas的“Reasoning about imperative quantum programs”; Yoshihiko Kakutani的“A logic for形式化验证of quantum programs”; Mingsheng Ying的“Floyd-霍尔逻辑for quantum programs”。我们比较了逻辑的数学基础，它们的底层语言，以及它们的断言的表达能力。我们还使用这些语言对Deutsch-Jozsa算法进行了验证，并讨论了它们在实际中的相对可用性。
2019-04-08 cs.ET cs.LO cs.PL
Decidable Verification of Uninterpreted Programs
我们研究的问题是完全自动验证未解释的程序--程序工作在任意的数据模型，提供了一个解释的常数，功能和程序使用的关系。验证问题询问给定的程序是否满足使用无量词公式编写的后置条件，在最终状态上具有相等性，没有提供循环不变式，合同等。我们证明了这个问题在一般情况下是不可判定的。本文的主要贡献是一个子类的程序，称为一致的程序，承认可判定的验证，并可以决定在PSPACE。然后，我们扩展这类程序的程序，是$k$ -连贯的，其中$k \in \mathbb{N}$，通过（自动）添加$k$鬼变量和分配，使它们连贯。我们还扩展了可判定性的结果与递归函数调用的程序，并证明了几个不可判定性的结果，表明为什么我们的限制，以获得可判定性似乎是必要的。
2020-08-26 cs.FL cs.LO cs.PL
Higher-Order Weakest Precondition Transformers via a CPS Transformation
本文针对具有一般计算效应和递归的高阶函数式语言，提出了最弱前置条件变换器与 CPS 变换之间的一般关系，将含效应程序验证归约为纯程序验证，并展示了该框架在多种验证方法中的实例化与扩展能力。
2025-07-01 cs.LO
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
Verification of Programs by Combining Iterated Specialization with Interpolation
我们提出了一个程序安全的验证技术，结合迭代专业化和插值霍恩子句求解。我们的新方法组合在一起，这两种技术在一个模块化的方式，利用共同的霍恩子句表示的验证问题。迭代专业化验证器通过使用展开/折叠等价保持转换规则来转换验证条件的初始集合。在转换过程中，程序不变量是通过应用加宽运算符来发现的。然后通过插值霍恩子句求解器分析专用验证条件的输出集，从而将插值的效果添加到加宽的效果中。特殊化和插值阶段可以迭代，也可以与其他改变约束传播方向的转换（从程序前提条件向前或从错误条件向后）相结合。我们已经实现了我们的验证技术集成VeriMAP验证器与FTCLP霍恩条款求解器，迭代专业化和插值的基础上，分别。我们的实验结果表明，集成验证器提高了每个单独运行的组件的精度。
2014-12-03 cs.LO cs.SE
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
Constraint-based automatic verification of abstract models of multithreaded programs
我们提出了一种多线程程序的抽象模型的自动验证技术，提供新鲜的名称生成，名称移动性和无界控制。作为高级规约语言，我们在这里采用了一个扩展的通信有限状态机的局部变量范围在一个无限的域名，称为TDL程序。通信机已被证明是非常有效的表示通信协议，以及表示多线程软件的抽象。我们提出的验证方法是基于编码的TDL程序成一个低级语言的基础上多集重写和约束，可以被看作是一个扩展的Petri网。通过这种编码，符号验证过程中开发的低级语言在我们以前的工作，现在可以应用到TDL程序。此外，编码使我们能够隔离TDL程序，仍然提供新鲜的名称生成，名称移动性和无界控制的可判定类的验证问题。我们的语法限制实际上是在线程的内部结构上定义的：为了获得一个完整的终止方法，线程最多只能有一个局部变量（范围在无限的域名上）。
2006-01-10 cs.LO cs.PL
A case study in formal verification of a Java program
我们描述了一个成功的尝试，正式验证一个简单的遗传算法编写的Java。为此，我们比较了几个为Java设计的形式化验证工具，并选择Krakatoa作为最适合的任务。根据我们的经验，我们提出了几个建议，使工具更加用户友好，我们希望这将导致更广泛地采用正式的方法。特别是，我们将详细讨论证明者进行某种形式的溯因推理是多么有用，也就是说，让他们猜测他们需要哪些额外的假设来证明一个陈述。我们认为，这一领域的进展将极大地改善形式化验证工具的可用性。
2018-09-10 cs.LO
