Smart Contracts Formal Verification: A Systematic Literature Review
本文系统综述智能合约形式化验证相关文献，梳理规格说明、验证工具与实验，并提出基于描述逻辑的替代验证方法。
2025-10-15 cs.LO cs.SE
Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification
形式方法是用于软件设计和工程的基于数学的技术，它能够对系统的行为进行明确的描述和推理。自主系统使用软件在没有人类控制的情况下做出决策，通常嵌入在机器人系统中，通常是安全关键的，并且越来越多地被引入日常环境中。自治系统需要健壮的开发和验证方法，但形式化方法的实践者经常被问到：为什么要使用自治系统的形式化方法？为了回答这个问题，这份立场文件描述了从文献中收集的五个配方，用于正式验证自治系统的各个方面。配方的例子是如何形式化方法可以成为一个有效的工具，自主系统的开发和验证。在设计过程中，它们可以明确地描述需求;在开发过程中，可以根据需求验证正式规范;可以从验证的规范合成软件组件;可以在运行时监控行为并与原始规范进行比较。现代形式化方法通常包括高度自动化的工具支持，这使得能够对系统的状态空间进行详尽的检查。本文认为，形式化方法是一个强大的工具，与其他强大的软件工程技术的发展技术的剧目安全自治系统。
2021-07-28 cs.LO cs.SE
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
本文提出一种符合功能安全标准的 PLC 程序形式化验证即服务，通过外部专家降低组织内部培训成本，并扩展至时间相关及专有技术保护组件建模，在 CERN 与 GSI 粒子加速器安全关键装置中验证了其有效性。
2025-02-26 cs.LO cs.SE
Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
在基于工业模型的开发（MBD）框架中，通常使用文本描述非正式地指定需求。为了使正式方法的应用，这些规格需要正式的输入语言的所有正式工具，应适用于分析模型在不同的发展水平。在本文中，我们提出了一个统一的方法，计算机辅助的正式规格说明的要求和他们的完全自动化翻译成规约语言的不同的验证工具。我们考虑一个两阶段的MBD方案，第一个Simulink模型的开发，自动生成可执行代码。我们（i）提出了一种规约语言和一个原型工具，用于正式但仍然是文本的需求规范，（ii）展示了如何将这些需求自动转换为Simulink Design Verifier的输入语言，用于验证Simulink模型和BTC EmbeddedValidator的源代码验证，以及（iii）展示了我们的统一框架如何在自动化形式化验证之外还实现测试用例的自动化生成。
2019-06-17 cs.LO cs.SE
Self-Driving Vehicle Verification Towards a Benchmark
University of Pennsylvania（宾夕法尼亚大学）
本文提出一个简单的形式化模型用于自动驾驶车辆，尽管经过简化后其安全性已手动证明，但目前尚无自动形式化验证工具支持其动态特性，旨在为形式化验证工具提供挑战。
2018-06-20 cs.LO cs.RO cs.SY
Introducing H, an institution-based formal specification and verification language
这是一个简短的调查的发展，形式规格说明和验证语言H的科学部分的重点。H是一种现代的高度表达性的语言，它牢固地建立在先进的数学理论基础上，例如机构理论中Kripke语义学的内化。
2019-08-26 cs.LO math.LO
A Formal Verification Methodology for Checking Data Integrity
形式化验证技术在预硅验证过程中发挥着重要作用。在进行形式化验证时考虑的最重要的一点是定义好的验证范围，我们应该明确定义在测试中的设计要正式验证什么。在定义形式化验证的范围时，我们考虑了以下三个实际需求。它们（a）难以核实（b）小到难以处理（c）容易理解。我们的新方法是将系统的通用属性分解为块级的原型属性，并定义可验证RTL的需求。因此，每个设计者而不是验证专家可以很容易地描述设计的属性，形式化的模型检验可以系统地和彻底地应用到所有的叶子模块。在服务器平台组件芯片的开发过程中，我们专注于RAS（可靠性，可用性和可服务性）功能，并在PSL中描述了2000多个属性。通过形式化验证，我们在有限的时间内发现了几个关键的逻辑错误，并成功地验证了所有这些错误。本文提出了一种功能验证方法的研究。
2007-10-25 cs.LO
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
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
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
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第13届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2022）的会议记录。Gandalf 2022研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2022-09-19 cs.FL cs.GT cs.LO
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
A case study in formal verification of a Java program
我们描述了一个成功的尝试，正式验证一个简单的遗传算法编写的Java。为此，我们比较了几个为Java设计的形式化验证工具，并选择Krakatoa作为最适合的任务。根据我们的经验，我们提出了几个建议，使工具更加用户友好，我们希望这将导致更广泛地采用正式的方法。特别是，我们将详细讨论证明者进行某种形式的溯因推理是多么有用，也就是说，让他们猜测他们需要哪些额外的假设来证明一个陈述。我们认为，这一领域的进展将极大地改善形式化验证工具的可用性。
2018-09-10 cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Formal Verification of Probing Security via Conditional Independence
Faculty of Education and Integrated Arts and Sciences Waseda University（早稻田大学教育综合科学部）
提出基于概率分离逻辑的方法，通过连接非干扰性与条件独立性，利用Lilac分离逻辑验证掩码算法的探测安全性，并提供证明规则。
2026-05-25 cs.CR cs.LO
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第七届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2016）的会议记录。研讨会于2016年9月14日至16日在意大利卡塔尼亚举行。研讨会的会议记录包括3个特邀演讲的摘要和21篇论文全文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题涵盖算法博弈论，自动机理论，综合，形式化验证，动态，模态和时态逻辑。
2016-09-13 cs.FL cs.GT cs.LO
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
2012-07-10 cs.LO cs.MS cs.PL
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification
该论文集汇集GandALF 2023关于博弈、自动机、逻辑与形式验证的研究，旨在连接学界与业界并推动理论及应用的交叉融合。
2023-09-29 cs.CC cs.FL cs.LO
A Formal Framework for Noisy Runtime Verification
Rensselaer Polytechnic Institute（伦斯勒理工学院）；Kansas State University（堪萨斯州立大学）；Tohoku University（东北大学）
本文提出认识动态逻辑EDMon，用于形式化建模噪声运行时验证中的可监控性，并证明其能捕捉文献中众多结果，梳理了与邻近逻辑的关系及定理类。
2026-09-10 cs.LO
Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第五届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2014）的会议记录。研讨会于2014年9月10日至12日在意大利维罗纳举行。专题讨论会的会议记录载有三次应邀演讲的摘要和19篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2014-08-24 cs.FL cs.GT cs.LO
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
本文是关于GandALF 2026研讨会论文集的介绍，该会议于2026年在丹麦奥尔堡举行，旨在汇集博弈、自动机、逻辑与形式化验证领域的研究者，促进理论与应用的交叉融合。
2026-10-08 cs.FL cs.LO
Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第四届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2013）的会议记录。研讨会于2013年8月29日至31日在意大利Borca di Cadore举行。专题讨论会的会议记录载有三次应邀演讲的摘要和17篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2013-07-16 cs.FL cs.GT 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
Proceedings Fifteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷是2024年6月在冰岛雷克雅未克举办的第十五届GandALF研讨会论文集，该会汇聚游戏、自动机等领域产学研研究者，覆盖理论到应用主题以促进跨领域融合。
2024-10-29 cs.CC cs.FL cs.LO
Proceedings of the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷为 GandALF 2025（第十六届国际游戏、自动机、逻辑与形式化验证研讨会）论文集，旨在汇聚相关领域产学研人员，推动从理论到应用的广泛主题交流与交叉融合。
2025-09-16 cs.LO
Formal Verification of Parameterized Systems based on Induction
针对参数化协议形式化验证的难题，提出基于归纳的验证框架wiseParaverifier，通过反例引导、启发式不变式查找等方法，在多类协议上实现了高效自动验证。
2025-03-23 cs.LO cs.SC
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
UCLID 5是一个多模态形式化建模、验证和系统综合的工具。它使人们能够解决异构系统的验证问题，如硬件和软件的组合，或那些有多个，不同的规格，或系统，需要混合模式的建模。\uclid的一个新方面是强调使用语法引导和归纳综合来自动化建模和验证步骤。本文介绍了\uclid工具的新发展，包括新的语言功能，集成与新技术的语法指导合成和可满足性解决，支持hyperproperties和组合的公理和操作建模，演示新的问题类，和一个强大的实现。
2022-08-07 cs.LO
Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda
随着软件变得越来越复杂，并在我们的生活中扮演着越来越重要的角色，形式化验证将成为未来保护软件系统的黄金标准，因为它可以保证没有错误和整个攻击类别。形式化验证的最新进展正被用于保护从无人驾驶飞机到互联网的一切。与此同时，可用性安全研究社区在提高安全产品的可用性和最终用户对安全问题的理解方面取得了巨大进展。然而，目前还没有以人为中心的研究关注形式化验证对使用和采用经正式验证的软件产品的影响。我们提出了一个研究议程，以填补这一空白，并有助于与第一次收集的研究对人们的心理模型的形式化验证和相关的安全和隐私的保证和威胁。拟议的研究有可能增加采用更安全的产品，它可以直接用于安全和正式的方法社区，以创建更有效和安全的软件工具。
2021-11-16 cs.CR cs.HC cs.LO
Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification
本卷包含了第二届游戏、自动机、语言和形式化验证国际研讨会（GandALF 2011）的论文集。会议于2011年6月15日至17日在意大利阿马尔菲海岸的米诺里举行。Gandalf研讨会的目的是为来自不同领域和不同背景的研究人员提供一个论坛，这些研究人员在博弈论，数理逻辑，自动机理论及其在复杂系统的规范，设计和验证中的应用方面有着共同的兴趣。本论文集包含三个特邀演讲和十九篇定期论文的摘要，这些论文是根据原创性、质量和与研讨会主题的相关性通过严格的审查过程选出的。
2011-06-04 cs.LO
Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification
本卷包含了2012年9月6日至8日在那不勒斯（意大利）举行的第三届游戏、自动机、逻辑和形式化验证国际研讨会（GandALF）的会议记录。Gandalf是由一些意大利计算机科学家创立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。尽管专题讨论会的想法是在意大利研究界提出的，但正如会议委员会的组成和方案所证明的那样，这次活动具有真正的国际性质。
2012-10-07 cs.GT cs.LO
Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python
National Institute of Advanced Industrial Science and Technology（国家工业科学与技术研究院）
针对科研可重复性危机，提出Python统计程序形式验证框架。介绍Why3-py，将Python程序转为WhyML表示，还扩展StatWhy工具，可助用户识别假设及分析误用，验证程序正确性。
2026-09-22 cs.AI cs.LO cs.PL
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第九届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2018）的会议记录。研讨会于2018年9月26日至28日在德国萨尔布吕肯举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2018-09-07 cs.FL cs.LO
A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks
本文综述了无线传感器网络的基础设施--adhoc路由协议的正确性证明的形式化验证方法。现有的技术分为两类：小规模网络上的验证和无界网络上的验证。由于验证过程中产生的状态空间有限，前者始终是全自动的，易于使用。然而，它不能证明所有情况下的正确性。后者可以提供一个基于无界网络抽象的完整证明。然而，它通常需要用户干预和验证方面的专业知识。对这两种方法的稳定性、无环性和无死锁性等关键性能进行了验证。总之，它们可以分别用于查找错误和证明正确性。我们相信，他们可以一起帮助正确的ad hoc路由协议的发展和可靠的实现。
2014-08-26 cs.LO cs.NI
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
TU Dortmund University（多特蒙德工业大学）；University of Oxford（牛津大学）
本综述针对形式化验证中手动制定规约困难且易错的瓶颈，系统梳理并比较了从系统行为示例中自动挖掘线性时序逻辑（LTL）规约的最新技术与方法。
2025-01-27 cs.AI cs.FL cs.LO
Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第11届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2020）的会议记录。研讨会于2020年9月21日至22日以完全在线的方式举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2020-09-20 cs.FL cs.GT cs.LO
Pseudo-Formalization for Automatic Proof Verification
本文提出了一种名为伪形式化的证明格式，该格式在保持自然语言灵活性的同时，保留了形式证明的模块性和精确性，通过块验证算法实现了对自然语言证明的高效验证，其在错误发现的精度和召回率上优于现有基线方法。
2026-10-02 cs.LG cs.LO
Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第十届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2019）的会议记录。研讨会于2010年9月2日至3日在法国波尔多举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2019-09-12 cs.FL cs.GT cs.LO
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第八届游戏、自动机、逻辑和形式化验证国际研讨会（GandALF 2017）的会议记录。研讨会于2017年9月20日至22日在意大利罗马举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2017-09-06 cs.FL cs.GT cs.LO
Abstraction-Based Proof Production in Formal Verification of Neural Networks
The Hebrew University of Jerusalem, Israel（耶路撒冷希伯来大学）；Technical University of Munich, Germany（慕尼黑技术大学）；Amherst College, USA（阿默斯特学院）
本文提出支持证明生成的基于抽象的 DNN 验证框架，将任务拆分为抽象网络正确性与抽象可靠性证明，填补可扩展性和形式化保证之间的缺口。
2025-06-11 cs.AI cs.LO
Proceedings First Symposium on Games, Automata, Logic, and Formal Verification
本卷包含了第一次研讨会上的“游戏，自动机，逻辑，和形式化验证（GandALF）"，在米诺里（阿马尔菲海岸），意大利，2010年6月17日至18日举行的会议记录。研讨会由一些对博弈论、数理逻辑、自动机理论及其在复杂系统的规范、设计和验证中的应用感兴趣的意大利计算机科学家推动。它涵盖了大量的研究课题，从理论方面到具体应用。它的目的是提供一个论坛，让来自不同地区的人，可能有不同的背景，可以成功地互动。该活动的高水平国际形象由节目委员会的组成和最终节目见证。
2010-06-09 cs.FL cs.GT cs.LO
Formal verification of a deadlock detection algorithm
死锁检测是片上网络分析和设计中的一个具有挑战性的问题。我们设计了一个算法，自动检测芯片上的网络中的虫洞交换的死锁。该算法已在ACL 2中指定并证明是正确的。为了实现自顶向下的证明方法，算法的某些部分尚未实现。对于这些部分，ACL 2规范包含了defun-sk引入的约束函数。我们使用单线程对象来表示算法使用的数据结构。在本文中，我们提出的算法的正确性证明的细节。形式化验证是保证算法无缺陷的关键。我们的最终目标是有一个有效的可执行文件，并正式证明正确的算法在ACL 2中运行的实现。
2011-10-21 cs.LO
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2
我们提出了一种算法RTL设计的形式化验证方法，它结合了时序逻辑等价性检查和交互式定理证明。一个Verilog模块的中间模型是用Restricted Systemic C（RAC）手工编码的，RAC是一个C的原始子集，由Systemic C的整数和定点寄存器类模板扩充。该模型被设计为尽可能的抽象和紧凑，但足够忠实的RTL允许有效的等价性检查与商业工具。然后，它会自动转换为ACL 2的逻辑，从而能够根据正式的体系结构规范对正确性进行机械检查。在本文中，我们描述了RAC语言，翻译过程，以及一些技术，方便正式分析所产生的ACL2代码。
2020-09-29 cs.LO cs.SC
Experience Report: Teaching Code Analysis and Verification Using Frama-C
形式化方法为软件开发提供了系统的、严格的技术。我们坚信，必须在计算机科学课程中教授这些知识。在本文中，我们提出的教学理论基础和具体实施的两门课程的使用形式化的方法，分享一些材料。这些课程促进了形式化验证的使用，以确保软件的安全性，例如物联网领域。
2021-11-16 cs.LO
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
这个扩展的抽象是关于努力建立一个正式的描述的三角剖分算法，从一个天真的描述的算法，三角形，边缘和三角剖分简单地给出了作为集和最复杂的概念是那些边界和分离的边缘。当执行有关该算法的证明，对称性的问题出现，本博览会试图给这些对称性如何处理的帐户。所有这些工作都依赖于Coq和数学组件库的正式开发。
2018-09-03 cs.CG cs.LO
Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
本文提出了两种形式化模型的数据加密标准（DES），第一个使用国际标准LOTOS，第二个使用最近的过程演算LNT。两种模型都以异步电路的方式对DES进行编码，即，DES算法的数据流块由经由会合通信的进程表示。为了确保模型的正确性，已经应用了几种技术，包括模型检验，等价性检验，并将从正式模型自动生成的原型产生的结果与DES的现有实现进行比较。模型的完整代码作为附录提供，也可以在CADP验证工具箱的网站上获得。
2015-11-13 cs.CR cs.LO
Formal Design and Verification of N-M Switching Control System
稳定电压至关重要的生产工厂，例如，电镀厂需要持续稳定的电压，以便通过实时的调整输入电压来最大限度地减少损耗，即使从外部提供低质量的电力。针对供电不稳定地区的工厂经常提出的这一问题，设计了N-M切换控制系统，并利用LTL模型检验技术验证了其正确性。
2012-12-12 cs.LO
Simplifying Neural Networks using Formal Verification
The Hebrew University of Jerusalem（耶路撒冷希伯来大学）；Stanford University（斯坦福大学）
深度神经网络（DNN）验证是一个新兴的领域，各种验证引擎迅速变得可用。在真实世界的DNN上展示这些引擎的有效性是迈向更广泛采用的重要一步。我们提出了一种工具，可以利用现有的验证引擎执行一个新的应用程序：神经网络简化，通过减少DNN的大小，而不损害其准确性。我们报告了简化过程的工作流程，并展示了其在一系列真实世界的DNN上的潜在意义和适用性，这些DNN用于飞机防撞，我们能够将其大小减少多达10%。
2020-08-10 cs.LG cs.LO cs.NE
FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping
Hong Kong University of Science and Technology(Guangzhou)（香港科技大学（广州））；Hong Kong University of Science and Technology（香港科技大学）
FORWORD是一种专为数据路径验证设计的字级扫描引擎，通过自适应优化和约束驱动模拟提升验证效率和适应性。
2025-12-12 cs.LO
Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+
使用控制模型提供访问控制、数字权限和信任管理的集成。为了实现这种集成，使用控制模型支持额外的概念，如属性可变性和决策的连续性。然而，这些概念可能会给底层模型带来额外的复杂性，使其定义成为一个繁琐且容易出错的过程。应用形式化验证技术允许对组件之间的交互进行严格分析，从而允许对模型的正确性进行形式化保证。在本文中，我们详细介绍了一个案例研究，在那里我们表示的高级功能模型的TLA+正式规约语言的使用控制模型的EQUIPCON，并验证其正确性<=12使用其支持的授权模型。
2018-06-26 cs.CR cs.LO
Formal verification of Zagier's one-sentence proof
我们评论两个正式证明费马的两个平方和定理，书面使用的数学组件库的Coq证明助手。第一个遵循Zagier著名的一句话证明;第二个遵循David Christopher最近的证明依赖于分割理论的论点。这两种形式的证明依赖于一个一般性质的对合的有限集，独立的利益。证明技术主要包括通过特殊策略自动化经常性任务（例如自然数的大小写区分和计算）。用同样的方法，我们还给出了关于素数的另一个经典结果$a^2 + 2 b^2$的形式证明。
2021-04-24 cs.LO math.NT
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest
通信是使多智能体系统能够合作的关键部分。这意味着将形式化方法应用于多智能体系统内的通信协议，可以为其可靠性提供有用的信心。在本文中，我们描述了形式化验证的一个复杂的通信协议，协调代理合并他们的环境的地图。LFC团队在2019年的多智能体编程竞赛（MAPC）中使用了该协议。我们的协议规范是写在通信顺序进程（CSP），这是一个非常适合的方法来指定智能体通信协议，由于其重点是并发通信系统。我们使用已知正确行为的场景来验证规范的行为，并验证最终所有映射都已合并。
2021-06-22 cs.LO cs.MA
Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification
本文提出以事务级层次结构替代模块层次结构，通过增强 PDVL 并结合 Coq 的 DFV 流程，将功能覆盖率转化为证明义务，实现 100% 覆盖与证明复用。
2025-01-02 cs.AR cs.LO
