$\{log\}$: Applications to Software Specification, Prototyping and Verification
本文档将介绍如何将Z规范转换为$\{log\}$，以及如何使用$\{log\}$运行模拟和自动化证明。这可以帮助其他规约语言（如B和VDM）的用户按照相同的方式使用$\{log\}$。介绍相当非正式，面向用户。更多的技术和正式的介绍可以在作者发表的论文中找到。我们还假设读者至少对Z符号有基本的了解。
2021-03-27 cs.LO cs.SE
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
OpenJML是一个检查Java程序的代码和规范的工具。我们描述了我们的经验，建立在JML，OpenJDK和Eclipse的基础上的工具，以及在基于规范的软件验证的许多进步。该实现展示了直接在软件开发IDE中集成规范工具的价值，以及尽可能多地自动化任务的价值。该工具，虽然仍在进行中，现在已被用于几个大学水平的课程，软件规范和验证，并对现有的Java程序的小规模研究。
2014-04-26 cs.LO cs.PL cs.SE
Verification of Patterns
软件模式为软件系统的设计和实现提供了构件，并试图使软件工程从经验走向科学。软件模式作为设计模式的引入而闻名于世。此后，图案得到了广泛而迅速的研究和发展。面向模式的软件体系结构系列丛书是软件模式发展的标志。正如在这些书中提到的，模式的形式化和一种中间模式语言是需要的，并且应该在模式的未来得到开发。因此，在本书中，我们按照面向模式的软件体系结构系列丛书的分类，对软件模式进行了形式化描述，并基于真正的并发进程代数对模式的正确性进行了验证。一方面，模式被形式化和验证;另一方面，真正的并发进程代数由于其严格的理论，可以起到中间模式语言的作用。
2021-10-25 cs.LO cs.SE
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
The University of Manchester（曼彻斯特大学）；Federal University of Amazonas (UFAM)（亚马孙联邦大学）
本文综述了ESBMC从研究原型发展为工业级形式化验证平台的过程，涵盖其技术演进、语言支持扩展、与LLM及AI代理的集成，并总结了其获奖、经济影响及未来挑战。
2026-05-30 cs.LO cs.SE
Proceedings Fourth International Workshop on Testing, Analysis and Verification of Web Software
本卷包含在第四届国际软件测试、分析和验证研讨会上提交的论文，该研讨会与第25届IEEE/ACM自动化软件工程国际会议（ASE 2010）有关。论文集包括形式规格说明，模型检查，测试和Web软件调试的研究。
2010-09-17 cs.FL cs.LO cs.PL
Proceedings of the Second Workshop on Verification of Objects at RunTime EXecution
本卷包含在阿姆斯特丹举行的第二届运行时对象验证研讨会（VORTEX 2018）的后续活动，与欧洲面向对象编程会议（ECOOP 2018）和ACM SIGSOFT软件测试和分析国际研讨会（ISSTA 2018）共同举办。运行时验证是一种软件验证方法，涉及对软件和硬件系统执行的监控和分析。最近，它已经获得了更多的共识，作为一个有效的和有前途的方法，以确保软件的可靠性，弥合之间的差距形式化验证，和传统的测试，在运行时执行过程中监视系统提供了额外的机会，解决错误恢复，自适应，和其他问题，超越软件的可靠性。VORTEX的目标是将研究人员聚集在一起，研究涉及理论或实践方面的主题的运行时验证，或者最好是两者兼而有之，重点是面向对象的语言和系统。
2019-08-25 cs.LO cs.PL cs.SE
Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
University of Arizona（亚利桑那大学）
本文提出了一种可扩展的方法论，用于通过形式验证微服务系统架构，通过静态建模和SMT约束集实现形式验证，并验证其正确性和适用性。
2025-09-02 cs.LO cs.SE
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
Correct-by-construction model composition: Application to the Invasive Software Composition method
组合技术提高了大型复杂系统开发中的重用性。安全关键系统需要密集的确认和验证活动。这些活动应该是组合的，以减少除了对每个组件进行的验证活动之外，还必须对组合进行的剩余验证活动的数量。为了保证组合验证的正确性和评估剩余验证的最小性，本文提出在组合操作符级别使用形式规格说明和验证。第一个实验在[15]中进行，使用证明助手来形式化通用组合技术ISC，并证明类型检查是组合的。这一贡献扩展了我们早期的工作，以处理完整的模型一致性和研究强制性的剩余验证。它表明ISC操作符在一致性方面不是完全组合的，并提供了确保组合一致性所必需的操作符的最小先决条件。ISC中的相应操作符（尤其是bind）已在COQ4MDE框架中实现，该框架在COQ证明助手中提供了MOF的完整实现。期望的属性，分别剩余验证，表示为后，分别为前，复合运算符的条件。在COQ中证明了组成验证的正确性。
2014-04-03 cs.LO cs.SE
Predicting SMT Solver Performance for Software Verification
Maynooth University（梅努斯大学）
Why 3 IDE和验证系统通过基于驱动程序的架构促进了广泛的可满足性模理论（SMT）求解器的使用。我们提出Where 4：一种基于投资组合的方法来履行Why 3证明义务。我们使用数据分析和机器学习技术对程序源代码的静态指标。我们的方法通过提供一个单一的实用程序来将证明义务委托给最有可能返回有用结果的求解器，从而使软件工程师受益。它使用现有的Why 3和求解器安装以一种高效的方式实现这一点-而不需要用户对SMT求解器操作的低层次知识。
2017-01-30 cs.LG cs.LO cs.SE
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
Modal Verification Patterns for Systems Software
本文提出以模态逻辑中的模态作为底层系统代码规约与验证的首选方法，借助资源上下文指导新模态设计，并用既有成功案例说明其通用验证模式。
2025-09-27 cs.LO
A Tutorial on Using Dafny to Construct Verified Software
本文是自动化验证工具领域的新手教程，尽管我们假设读者对Hoare风格的验证相对熟悉。本文除了介绍语言和验证器Dafny的最基本的特点外，还特别强调了如何使用Dafny作为验证程序开发的助手。我们的主要目标是鼓励软件工程社区使用形式化验证工具。
2017-01-16 cs.LO cs.PL cs.SE
Proceedings of the International Workshop on Verification of Scientific Software
本论文集收录了VSS 2025研讨会的成果，涵盖演绎验证、浮点误差分析等主题，旨在推动大规模科学代码的正确性与可靠性研究。
2025-10-14 cs.CE 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
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
Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
LMU Munich（慕尼黑大学）
本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。
2026-01-15 cs.LO cs.PL cs.SE
Automated Deductive Verification for Ladder Programming
梯形图逻辑是IEC 61131-3标准化的程序设计语言，广泛用于对工业可编程逻辑控制器（PLC）进行编程。PLC程序由输入（其值在运行时由工厂传感器给出），输出（其值在运行时提供给工厂执行器）和从输入值计算输出值的逻辑表达式组成。由于梯形图程序的图形形式，以及典型工业程序中的输入和输出量，调试此类程序既耗时又容易出错。在本文中，我们提出了一个基于Why 3的工具原型，我们已经实现了自动化的演绎验证的使用，以提供一个易于使用和强大的调试工具的阶梯程序员。
2019-12-23 cs.LO cs.PL cs.SE
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
Graph Based Reduction of Program Verification Conditions
在C程序的演绎验证中，提高证明的自动性是一项具有挑战性的任务。当应用于工业C程序时，已知的生成更简单的验证条件的方法不够有效。这主要是由于它们的规模和大量不相关的假设。这项工作提出了一种策略，以减少程序验证条件，通过选择其相关的假设。一个假设的相关性是由一个句法分析和两个图形遍历的组合来确定的。第一个图用常数标记，第二个图用公理中的谓词标记。该方法被应用于工业程序验证中产生的基准。
2009-07-08 cs.LO
Verification of MPI programs
在本文中，我们概述了一种方法来验证并行程序。介绍了一种新的并行程序数学模型。通过矩阵乘法MPI程序的验证，说明了所引入的模型。
2021-10-16 cs.LO cs.PL
Compositional Reasoning for Shared-variable Concurrent Programs
并发系统的可扩展和自动化形式化验证一直是一个迫切的需求。在本文中，我们提出了一个验证框架，以支持自动组合推理的并发程序共享变量。我们的框架模型并发程序作为简洁的自动机，并支持多个重要属性的验证。简洁自动机的安全性验证和仿真是并行组合的，简洁自动机的安全性在精化过程中保持不变。我们以自动化的方式从无限状态并发程序中生成简洁的自动机。此外，我们提出了第一个自动化的方法来检查可靠保证无限状态并发程序之间的模拟。我们已经将我们的算法原型化，并将我们的工具应用于多个改进的验证。
2018-03-26 cs.FL cs.LO cs.SE
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
Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification
嵌入有易受攻击的单片软件的无人机（UAV）的激增最近引起了人们对其安全性的严重关注，这是由于并发方面和脆弱的通信链路。然而，基于传统测试验证无人机软件的安全性仍然是一个开放的挑战，主要是由于可扩展性和部署问题。在这里，我们调查软件验证技术来检测典型的无人机的安全漏洞。特别是，我们调查现有的软件分析器和验证器，实现模糊和有界模型检验（BMC）技术，检测内存安全和并发错误。我们还调查了与无人机通信链路相关的脆弱性方面。所有无人机部件（例如，位置、速度和姿态控制）严重依赖于通信链路。我们的初步结果表明，模糊和BMC技术可以检测各种软件漏洞，这是特别感兴趣的，以确保无人机的安全。我们能够通过对无人机的连接和软件系统进行渗透测试，成功地进行网络攻击。因此，我们展示了真实的网络威胁，并有可能在可预见的未来利用现实世界无人机软件中的进一步安全漏洞。
2019-10-11 cs.CR cs.LO
FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Astrio Labs（阿斯特里奥实验室）
提出 FORALL-LEAN-AGENT 框架，通过隔离工作区、公理审计和独立检查实现可审计的 Lean 证明验证，在 VeriSoftBench 和 PutnamBench 上提升成功率并降低成本。
2026-10-02 cs.AI cs.LO cs.SE
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
Hardware/Software Co-verification Using Path-based Symbolic Execution
用于正式硬件/软件协同验证的常规工具使用有界模型检验技术来构造单个整体命题公式。以这种方式生成的公式非常复杂，并且包含大量不相关的逻辑，因此即使是最先进的Satis能力（SAT）求解器也很难解决。在典型的硬件/软件协同设计中，固件只使用硬件状态空间的一小部分，我们可以使用这个观察结果来生成更简单和更简洁的公式。在本文中，我们提出了一种新的验证算法的硬件/软件协同设计，确定分区的固件和硬件逻辑有关的可行的执行路径，通过基于路径的符号模拟与自定义路径修剪，属性引导切片和增量SAT解决。我们已经在我们的工具COVERIF中实现了这种方法。我们已经通过实验比较了COVERIF与基于单片BMC的协同验证工具HW-CBMC，并观察到HW-CBMC的平均速度提高了5倍，以证明安全属性以及检测开源通用异步接收器发送器设计和大型SoC设计中的关键协同设计错误。
2020-01-05 cs.FL cs.LO
Practical Deductive Verification of OCaml Programs (Extended Version)
本文提供使用 GOSPEL 规范语言和 Cameleer 工具对 OCaml 程序进行演绎验证的实践教程，涵盖纯函数式与命令式两类程序，实现大部分自动化验证。
2024-07-20 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
(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 benchmark for C program verification
我们提出了25个C程序，作为C程序验证使用形式化方法的基准。该基准测试可用于系统演示、系统间验证工作的比较，以及作为一种友好的竞争。对于最后一个目的，我们给出了一个评分公式，允许验证系统得分高达一百分。
2019-04-01 cs.LO cs.PL
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
From Well Structured Transition Systems to Program Verification
我们描述了使用的WSTS理论验证程序。
2020-08-07 cs.FL 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
A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier
本文在mCRL2中对Maeslant风暴潮屏障的BesW软件控制系统进行了完整形式化规范，覆盖手动、测试及故障模式，并基于模态μ演算在受限水位和故障组合条件下验证了全部行为性质。
2025-04-11 cs.LO
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
我们报告的工作进展自动程序证明性能的程序写在高阶函数语言。我们的方法编码高阶程序直接作为一阶SMT问题的霍恩条款。将一阶程序的Hoare式验证简化为Horn子句的可满足性是很直接的。闭包的存在带来了一些挑战：相对完整的证明系统必须考虑闭包;在实践中，搜索过程的有效性取决于编码策略和底层求解器的能力。我们在这里使用代数数据类型来编码闭包，并依赖于支持代数数据类型的求解器。该方法的可行性进行检查使用的例子从文献中高阶程序验证。
2013-06-21 cs.LO
Can ChatGPT support software verification?
Carl-von-Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西特齐大学）
本研究探索ChatGPT能否生成循环不变量以支持软件验证，实验表明其生成的不变量有效且有用，能增强Frama-C的验证能力，并提出结合大语言模型与验证器的方向。
2025-10-14 cs.AI cs.FL cs.LG
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
概率程序验证的基本任务包括约束期望结果和证明有限期望运行时间内的终止性。我们贡献了一个简单而有效的归纳合成方法，证明这种定量的可达性属性生成归纳不变的源代码级。我们的实施显示了承诺：它为有限状态程序找到不变量，可以击败最先进的概率模型检查器，并且与致力于不变量合成和预期运行时推理的现代工具竞争。
2023-02-08 cs.LO
Toward Automatic Verification of Quantum Programs
本文总结了作者和他的合作者在量子程序的程序逻辑验证方法中所获得的结果，包括量子Hoare逻辑，量子程序的不变量生成和终止分析。为了更方便地对量子程序进行推理，还引入了证明大纲的概念和一些辅助规则。文章最后提出了今后研究的一些问题。
2018-07-31 cs.LO quant-ph
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
Software Verification of Hyperproperties Beyond k-Safety
时态超属性是与多个执行跟踪相关的系统属性。对于（有限状态）硬件，时态超属性由模型检验算法支持，并且存在用于一般时态逻辑的工具，如HyperLTL。对于（无限状态）软件，到目前为止，时间超属性的分析仅限于$k$ -安全属性，即，规定任何$k$迹线之间不存在不良交互的属性。在本文中，我们提出了一个自动化的方法来验证$\forall^k\exists^l$ -安全性质的无限状态系统。$\forall^k\exists^l$ -安全属性规定，对于任何$k$迹线，存在$l$迹线，使得所得到的$k+l$迹线不会不良地交互。这种泛量化和存在量化的结合使我们能够表达$k$ -安全性之外的许多性质，包括例如广义不干涉或程序细化。我们的方法是基于一个基于策略的实例化的存在跟踪量化相结合的程序减少，无论是在一个固定的谓词抽象的上下文中。值得注意的是，我们的框架允许战略和减少的相互依赖。
2022-08-25 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
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
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
本文通过为{log}语言定义类型系统并实现类型检查器，将类型检查与集合约束求解结合，提高了软件验证的自动化程度，并通过两个工业案例验证了其有效性。
2024-03-21 cs.LO cs.PL
Efficient verification of imperative programs using auto2
Auto 2是最近为证明助手Isabelle引入的证明器。它被设计为既可以从Isabelle内部高度定制，又具有强大的证明搜索机制。本文将auto 2应用于命令式程序的验证。我们描述了两个阶段的证明过程中的自动2的设置：验证的功能版本的程序，并使用分离逻辑完善的命令式版本。作为例子，我们验证了几个数据结构，包括红黑树，区间树，优先级队列，和union-find。我们还验证了几个算法利用这些数据结构。这些例子表明，我们的框架是能够有效地验证复杂的算法，并在一个模块化的方式。
2018-02-24 cs.LO
