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
A Formal Verification Methodology for Checking Data Integrity
形式化验证技术在预硅验证过程中发挥着重要作用。在进行形式化验证时考虑的最重要的一点是定义好的验证范围，我们应该明确定义在测试中的设计要正式验证什么。在定义形式化验证的范围时，我们考虑了以下三个实际需求。它们（a）难以核实（b）小到难以处理（c）容易理解。我们的新方法是将系统的通用属性分解为块级的原型属性，并定义可验证RTL的需求。因此，每个设计者而不是验证专家可以很容易地描述设计的属性，形式化的模型检验可以系统地和彻底地应用到所有的叶子模块。在服务器平台组件芯片的开发过程中，我们专注于RAS（可靠性，可用性和可服务性）功能，并在PSL中描述了2000多个属性。通过形式化验证，我们在有限的时间内发现了几个关键的逻辑错误，并成功地验证了所有这些错误。本文提出了一种功能验证方法的研究。
2007-10-25 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
A case study in formal verification of a Java program
我们描述了一个成功的尝试，正式验证一个简单的遗传算法编写的Java。为此，我们比较了几个为Java设计的形式化验证工具，并选择Krakatoa作为最适合的任务。根据我们的经验，我们提出了几个建议，使工具更加用户友好，我们希望这将导致更广泛地采用正式的方法。特别是，我们将详细讨论证明者进行某种形式的溯因推理是多么有用，也就是说，让他们猜测他们需要哪些额外的假设来证明一个陈述。我们认为，这一领域的进展将极大地改善形式化验证工具的可用性。
2018-09-10 cs.LO
Efficient verification of imperative programs using auto2
Auto 2是最近为证明助手Isabelle引入的证明器。它被设计为既可以从Isabelle内部高度定制，又具有强大的证明搜索机制。本文将auto 2应用于命令式程序的验证。我们描述了两个阶段的证明过程中的自动2的设置：验证的功能版本的程序，并使用分离逻辑完善的命令式版本。作为例子，我们验证了几个数据结构，包括红黑树，区间树，优先级队列，和union-find。我们还验证了几个算法利用这些数据结构。这些例子表明，我们的框架是能够有效地验证复杂的算法，并在一个模块化的方式。
2018-02-24 cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Introducing H, an institution-based formal specification and verification language
这是一个简短的调查的发展，形式规格说明和验证语言H的科学部分的重点。H是一种现代的高度表达性的语言，它牢固地建立在先进的数学理论基础上，例如机构理论中Kripke语义学的内化。
2019-08-26 cs.LO math.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
National Institute of Informatics（信息处理研究所）；Kyoto University（京都大学）；Waseda University（早稻田大学）；Tohoku University（东北大学）
本文提出一个范畴框架，通过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
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
本文提出了一个多元非线性不等式的形式化验证工具。我们的验证方法是基于泰勒近似的区间算术。我们的工具在HOL Light证明助手中实现，它能够验证矩形域上的多元非线性多项式和非多项式不等式。我们的工作的主要特点之一是一个有效的实现的验证过程，可以证明非平凡的高维不等式在几秒钟内。我们开发了验证工具作为Flyspeck项目（开普勒猜想的正式证明）的一部分。Flyspeck项目包括大约1000个非线性不等式。我们成功地测试了我们的方法对100多个Flyspeck不等式，并估计，形式化验证过程是约3000倍，比非正式的验证方法在C++中实现慢。我们还描述了未来的工作和前瞻性的优化我们的方法。
2013-01-08 cs.LO math.LO
A Formal Framework for Noisy Runtime Verification
Rensselaer Polytechnic Institute（伦斯勒理工学院）；Kansas State University（堪萨斯州立大学）；Tohoku University（东北大学）
本文提出认识动态逻辑EDMon，用于形式化建模噪声运行时验证中的可监控性，并证明其能捕捉文献中众多结果，梳理了与邻近逻辑的关系及定理类。
2026-09-10 cs.LO
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
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2015）的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文，这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论，自动机理论，形式化验证，模态和时序逻辑。
2015-09-23 cs.FL cs.LO
Formal Verification of Full-Wave Rectifier: A Case Study
我们提出了一个案例研究的形式化验证的全波整流器的模拟和混合信号的设计。我们使用了CMU的Checkmate工具[1]，这是一个公共领域的混合系统形式化验证工具。由于Checkmate的限制，需要在Checkmate实现中进行更改，以实现复杂的非线性系统。全波整流器已实现使用Checkmate自定义模块和Simulink模块从MATLAB的数学作品。在Checkmate实施中建立所需的更改后，我们能够有效地验证全波整流器的安全特性。
2009-09-29 cs.LO
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
Proceedings of the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷为 GandALF 2025（第十六届国际游戏、自动机、逻辑与形式化验证研讨会）论文集，旨在汇聚相关领域产学研人员，推动从理论到应用的广泛主题交流与交叉融合。
2025-09-16 cs.LO
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
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第12届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2021）的会议记录。Gandalf 2021研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2021-09-16 cs.FL cs.GT 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
{log}: From a Constraint Logic Programming Language to a Formal Verification Tool
CIFASIS-CONICET（国家科学和技术研究委员会联邦应用科学研究所）
{log}通过扩展成为形式验证环境，实现了从约束逻辑编程语言到自动证明系统的无缝集成。
2026-03-12 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
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback
提出了一种低功耗x86浮点乘法器的形式化验证。乘法器迭代操作，并以冗余表示反馈中间结果。它支持各种精度的x87和SSE指令，并可以阻止新指令的发布。该设计已针对低功耗操作进行了优化，并且不受形式化验证工作的约束。通过形式化验证确定了实施的其他改进。设计的形式化验证还包括时钟门控和控制逻辑的实现。验证工作的核心是基于ACL 2定理证明。此外，模型检验已被用于验证与单元的正确操作相关的浮点调度器的某些属性。
2011-10-21 cs.AR cs.LO cs.MS
