Verification of a Smart Contract for a Simple Casino
我们描述了一个简单的赌场应用程序的现有智能合约的验证，使用Whiley规范和程序设计语言，以及基于Boogie和Z3的全自动验证引擎。在发现并修复了智能合约中的几个规范和代码问题后，我们能够验证智能合约的所有操作。
2021-06-28 cs.LO
Proceedings 9th International Workshop on Automated Specification and Verification of Web Systems
本卷包含第9届Web系统自动化规范和验证国际研讨会（WWV'13）的接受论文，该研讨会于6月6日在意大利佛罗伦萨举行，作为第8届分布式计算技术国际联合会议（DisCoTec 2013）的卫星活动。
2013-07-31 cs.LO cs.SE
Towards Automated Verification of Web Services
本文提出了使用模型检测软件技术来验证基于Web服务的工作流和业务流程行为，即使用SPIN模型检测器。由于基于Web服务的业务流程行为的规范可以分解为模式，因此提出了一个众所周知的工作流模式的集合到PROMELA，SPIN的输入规约语言的翻译。这种翻译的使用说明了一个业务流程的例子，它演示了如何将其翻译为PROMELA模型可以是有用的Web服务规范和验证。
2011-11-11 cs.LO
Accelerated Runtime Verification of LTL Specifications with Counting Semantics
运行时验证是一种有效的自动化方法，用于基于规范的离线测试和分析以及复杂系统的在线监控。规约语言通常是正则表达式或流行的时态逻辑（如LTL）的变体。本文提出了一种新的和有效的并行算法验证LTL规范，结合计数语义，嵌套量词可以受到数值约束的更有表现力的版本。这样的约束在评估阈值（例如，Web服务器的预期带宽）。这种扩展的意义在于，它使我们能够推理的正确性的一大类系统，如Web服务器，操作系统内核，和网络行为，其中的属性需要被实例化的参数化请求，内核对象，网络节点等，我们的算法使用流行的{ \em MapReduce}体系结构分裂成基于变量的集群程序跟踪在运行时间。然后，每个集群都被映射到其各自的监视器实例，并在多核CPU或GPU上进行验证和简化。我们的算法是完全实现的，我们报告非常令人鼓舞的实验结果，在现实世界的数据集上的监控开销可以忽略不计。
2014-11-09 cs.LO
CTL* Verification and Synthesis using Existential Horn Clauses
Technion - Israel Institute of Technology（以色列理工学院）
本文提出基于存在性Horn子句（EHCs）的自动验证与合成方法，用于无限状态反应程序对CTL*规格的验证，展示了其在复杂系统中的应用。
2024-08-21 cs.LO
Specification and verification of a linear-time logic for graph transformation
提出一种基于对应物范式的一阶线性时间时序逻辑，用于推理有向图演化，并引入正规范形式简化验证，通过Agda形式化验证其语法与语义。
2023-05-05 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
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
Omega-regular Verification and Control for Distributional Specifications in MDPs
本文首次提出基于分布性证书的自动化方法，在 PSPACE 内实现对 MDP 分布性 omega-正则规范的可靠且相对完备的验证与控制。
2025-07-06 cs.LO
Automatic Verification of Parametric Specifications with Complex Topologies
本文的重点是降低验证的复杂性，利用模块化在各个层次上：在规范，验证，和结构。对于规范，我们使用的模块化语言CSP-OZ-DC，它允许我们解耦验证任务有关的数据从那些有关的持续时间。在验证级别，我们利用模块化的定理证明丰富的数据结构，并使用此不变检查。在结构层面上，我们分析了模块化验证的系统组成的各种组件的相互作用的可能性，我们说明了这些想法，通过自动验证安全性能的案例研究，从欧洲训练控制系统标准，它扩展了以前的例子，包括一个复杂的轨道拓扑结构与列表的轨道段和列车与不同的路线。
2010-10-08 cs.LO cs.SE
$\{log\}$: Applications to Software Specification, Prototyping and Verification
本文档将介绍如何将Z规范转换为$\{log\}$，以及如何使用$\{log\}$运行模拟和自动化证明。这可以帮助其他规约语言（如B和VDM）的用户按照相同的方式使用$\{log\}$。介绍相当非正式，面向用户。更多的技术和正式的介绍可以在作者发表的论文中找到。我们还假设读者至少对Z符号有基本的了解。
2021-03-27 cs.LO cs.SE
Lessons Learned From Microkernel Verification -- Specification is the New Bottleneck
软件验证工具近年来变得更加强大。甚至大型复杂系统的验证也是可行的，如L4.verified和Verisoft XT项目所示。尽管如此，大型软件系统的功能验证是罕见的-原因超出了大规模的验证工作所需的大小。在本文中，我们报告的经验教训，验证大型软件系统的基础上获得的经验，在Verisoft XT项目的微核验证。我们讨论了一些问题，阻碍广泛引入形式化验证在软件生命周期过程。
2012-11-27 cs.LO cs.SE
Weakest Precondition Rules for Programs with Linear Temporal Specifications
University of Augsburg（奥格斯堡大学）；LMU Munich（慕尼黑大学）
研究如何将软件模块集成中时态逻辑需求考虑进去，针对现有工具不足，提出一种简单通用能集成到现有验证条件生成器的解决方案来处理结构化程序与时态逻辑集成问题。
2026-07-10 cs.LO
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
A Hoare Logic for Domain Specification (Full Version)
针对现有程序规约与验证方法仅关注计算层面正确性的问题，研究提出整合实现与领域断言的双层霍尔逻辑，采用描述逻辑和语义提升方法，通过两类断言转换的演算实现关注点分离并支持验证中使用描述逻辑。
2024-02-01 cs.LO
A New Method of Verification of Functional Programs
本文研究了字符串上函数程序的验证问题，其中函数程序的性质规范由其它函数程序定义，一个函数程序S1满足另一个函数程序S2定义的规范当且仅当由函数程序S1和S2定义的函数的组合等于常数1.我们引入了一个FP的状态图的概念，并减少了验证问题的FP的状态图的分析问题。所提出的方法是说明了一个排序程序的验证的例子。
2016-04-14 cs.LO
Responsibility and verification: Importance value in temporal logics
我们的目标是测量系统的一部分，它的能力，以满足规格的不确定性的选择的影响。为此，我们应用Shapley值的概念来验证作为一种手段来评估系统的一部分是多么重要。组件的重要性是通过将其控制权单独或与其他组件一起交给对手，并测试系统是否仍然可以满足规范来衡量的。我们研究这个想法的框架中的模型检查与各种经典类型的线性时间规范，并提出了几种方法来转置分支。我们还提供了严格的复杂性界限，几乎在每一种情况下。
2021-04-20 cs.LO
Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications
研究随机系统在信号时序逻辑规范下的验证问题，提出STL侵蚀策略，将概率验证转化为更严格的确定性验证，可与现有算法无缝集成，数值实验验证了其有效性。
2025-02-11 cs.FL cs.LO cs.SY
A Verified Approach for Checking Real-Time Specification Patterns
我们提出了一个验证方法的形式化验证的时间属性使用模型检查技术。我们专注于使用实时的【形】规范模式，它可以被看作是一个子集的定时时序逻辑，包括反应系统的分析过程中常见的属性表示的属性。我们的模型检测方法是基于使用观察员，以转换到验证更简单的LTL公式的验证定时模式。虽然使用观察员的模型检查是很常见的，我们的贡献是原始的几个方面。首先，我们定义了一个正式的框架来验证我们的观察者是正确的和非侵入性的。其次，我们为每个模式定义不同的观察者类别，并使用务实的方法，以选择最有效的候选人在实践中。这种方法是实现在一个集成的验证工具链的Fiacre语言。
2013-01-31 cs.LO
Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements
本文提出定量假设-保证契约，实现多智能体系统在定量时间逻辑LTL[$\mathcal{F}$]规范下的组合式设计与验证，提高可扩展性和模块化。
2024-12-17 cs.LO
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
本文提出将非嵌套离散时间 STL 公式编码为 Lustre 同步观察器，提供三值在线语义以支持性质验证与反例搜索，并通过仪表化证明确保实现正确性，实验使用 Kind2 和 Z3 自动化完成。
2023-11-16 cs.LO
Refinement and Verification of Real-Time Systems
本文讨论了高度通用的机制，指定细化的实时的【形】系统作为一个集合的低级别的并行组件，保留的时间和功能要求的上层规格。这些机制的ASTRAL，这是一个正式的规约语言的实时的【形】系统的上下文中进行了讨论。细化是通过将上层规范的所有元素映射到可以在几个并行组件之间拆分的下层元素来完成的。此外，可以在较高级别中发生的动作被映射到在较低级别处操作的组件的动作。这允许以自然的方式指定几种类型的实现策略，而通用性（在复杂性方面）的代价仅在必要时支付。细化机制首先说明使用一个简单的数字电路，然后，通过一个高度复杂的电话系统，最后，从这些规格收集的设计准则。
2010-02-09 cs.LO
Weakening Goals in Logical Specifications
针对逻辑规范在系统退化或环境变化下属性不再成立的问题，提出反例引导的迭代弱化属性技术，应用于命题逻辑规范，并计划扩展至状态表示，以辅助理解不确定行为与组合验证。
2025-10-17 cs.LO
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
灯塔项目，如CompCert，seL 4，IronFleet和DeepSpec已经证明，通过在抽象系统规范和可执行实现之间建立细化关系，可以对整个系统进行全面验证。然而，现有的方法施加严重的限制，无论是抽象的系统规范，由于其有限的表现力或多功能性，或可执行代码，由于其依赖于次优的代码提取或无表现力的程序逻辑。我们提出了一种新的方法，结合了组成细化的抽象，基于事件的模型的分布式系统与验证的成熟的程序代码，使用表达分离逻辑，支持功能的现实程序设计语言，如可变堆数据结构和并发。我们的工作的主要技术贡献是一个正式的框架，健全的基于事件的系统模型，程序规范的分离逻辑，这样的成功验证建立了一个细化模型和代码之间的关系。我们在Isabelle/HOL中正式定义了我们的框架Igloo。我们的框架，使现有的程序验证器的协议开发工具的良好组合。我们报告的三个案例研究，领导人选举协议，复制协议，和安全协议，我们完善正式的要求到程序规范（在伊莎贝尔/HOL），我们在Java和Python中实现，并证明正确使用VeriFast和Nagini工具。
2020-10-09 cs.LO
OSVAuto: automatic proofs about functional specifications in OS verification
本研究提出OSVAuto工具，通过编码OS常见数据类型命题为SMT形式并扩展序列量词实例化方法，实现uC-OS/II内核验证中大量函数规范证明义务的自动求解，降低证明工作量。
2025-05-22 cs.LO cs.SC
Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
本文提出一种针对 OCaml 高阶迭代器的通用规约与演绎验证方法，利用 Gospel 语言描述迭代行为并通过 Cameleer 框架验证客户端正确性，经列表与图算法案例验证有效。
2025-06-25 cs.LO cs.PL
On the specification and verification of atomic swap smart contracts
区块链系统和智能合约提供了在不使用可信中介的情况下安全地实现多方交易的方法，而可信中介目前是许多商业交易的基础。但是，它们是通过将信任传递给计算机系统来实现这一点的，这就提出了代码是否可信的问题。错误代码导致的高价值损失的经验已经表明，智能合约的形式化验证可能是有益的。本文研究了一种简单形式的多方事务原子交换的规范和验证。有人认为，逻辑的能力来表达属性的球员在多智能体设置的策略在概念上是有用的，为此目的，虽然最终，对于我们的具体例子，时间逻辑的表达能力较低的设置足以验证具体的实现。通过使用模型检查器来验证链上和跨链设置中的原子交换智能合约的一些示例来说明这一点。
2018-11-14 cs.DC cs.LO
Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems
这些会议记录包含在2015年6月23日在挪威奥斯陆举行的第11届Web系统自动化规范和验证国际研讨会（WWV 2015）上提交的论文，作为第20届形式化方法国际研讨会（FM 2015）的卫星研讨会。WWV是一个年度跨学科论坛，研究人员来自以下领域：声明式，基于规则的编程，形式化方法，软件工程和基于Web的系统。该研讨会促进这些领域的混合方法的交叉和进步。
2015-08-14 cs.LO cs.PL cs.SE
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
Zhejiang University（浙江大学）；Peking University（北京大学）；The Chinese University of Hong Kong（香港中文大学）；Xidian University（西安电子科技大学）；Beijing Institute of Control Engineering（北京控制工程研究所）
Preguss通过结合静态分析与演绎验证，实现大规模程序的自动化形式化验证，显著提升验证效率。
2026-03-10 cs.LO cs.SE
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
我们提出RVHyper，一个运行时验证工具的hyperproperties。超性质，如非干涉性和观察决定论，将多个计算轨迹相互关联。规范在时态逻辑HyperLTL中以公式的形式给出，它扩展了线性时间时态逻辑（LTL）的跟踪量词和跟踪变量。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。作为一个示例应用程序，我们展示了如何RVHyper可以用来检测虚假的依赖关系，在硬件设计。
2019-05-31 cs.LO
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
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
2012-07-10 cs.LO cs.MS cs.PL
Proceedings 10th International Workshop on Automated Specification and Verification of Web Systems
这些会议记录包含在第10届Web系统自动规范和验证国际研讨会上提交的论文（WWV 2014），于2014年7月18日在奥地利维也纳举行，作为联邦逻辑会议的卫星研讨会（FLoC 2014），与第七届自动推理国际联合会议（IJCAR 2014）相关，作为维也纳逻辑之夏（VSL 2014）的一部分。WWV是一个年度研讨会，旨在提供一个跨学科的论坛，以促进交叉施肥和混合方法的发展，这些方法利用基于规则的编程，正式方法，软件工程和面向Web的研究的概念和工具。
2014-09-08 cs.LO cs.PL 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
A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification
本文讨论的问题，指定，模拟和验证反应系统重写逻辑。它提出了一个可执行的语义概率，时间和空间并发约束编程-这里称为随机和空间并发约束系统（SSCC）-在重写逻辑语义框架。该方法是基于一个增强和广义模型的并发约束规划（CCP）的计算层次空间可以分配给属于代理。可执行语义忠实地表示和操作捕捉高度并发的性质，不确定的行为，空间和认知特征的反应系统与信息流。在SSCC中，定时属性（由随机持续时间表示）可以与进程相关联，并且还支持排他性和独立的概率选择。利用Maude系统中的SMT求解技术，实现了SSCC的底层约束系统，包括整数和实数上的无量词公式。这导致了一个完全可执行的实时符号规范，可用于定量分析的统计模型检验的形式。SSCC的主要特点和能力说明了整个文件的例子。这一贡献是一个更大的研究工作的一部分，旨在提供正式的分析技术和工具，数学上建立在CCP的方法，研究界。
2022-11-03 cs.LO
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC cs.LO
Formal Specification and Verification of Solidity Contracts with Events
Solidity语言中的事件提供了去中心化应用程序的链上服务与这些服务的用户之间的通信方式。事件通常被用作从用户的角度来看相关的合约执行的抽象。因此，用户必须能够理解所发出事件的含义并信任其有效性。本文提出了一种源代码级的方法，用于Solidity合同的形式化规范和验证，主要关注事件。我们的方法允许根据事件跟踪的链上数据来指定事件，以及定义区块链状态与事件提供的抽象视图之间的对应关系的谓词。该方法是在solc验证，Solidity的模块化验证，我们证明了它的适用性与各种例子。
2020-05-20 cs.LO cs.PL cs.SE
Review of Recent Heap Specification and Verification Techniques
文章对现有的动态存储器验证方法进行了综述，并进行了比较分析，评价了其在解决动态存储器控制、监控和验证问题上的适用性。本文共分为八个部分。第一节介绍了形式化验证，随后的一节讨论了动态存储管理问题。第三部分讨论了Hoare的演算恢复堆变换的堆栈。第五节和第六节介绍了动态记忆形状分析和指针旋转的概念。第七是关于分离逻辑。最后一节讨论了进一步研究的可能领域，特别是在记录水平上识别对象的各种实例;证明的自动化;“热”代码，即程序运行时自动更新的软件代码;扩大直观性，例如，证明解释。
2022-03-24 cs.LO cs.SC
Advances of Proof Scores in CafeOBJ
本文介绍可执行代数规范语言系统 CafeOBJ 中证明评分的最新进展，说明其如何支持工程师开展规范验证并提升领域、需求与设计规范质量。
2023-12-06 cs.LO cs.SE
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
Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption
许多应用程序需要符合规范，约束资源的使用，如执行时间，能源，带宽等，我们已经提出了一个可配置的框架，静态资源使用验证规范可以包括下限和上限，数据大小相关的资源使用功能。为了静态地检查这些规范，我们的框架推断出相同类型的资源使用函数，这些函数安全地近似于程序的实际资源使用，并将它们与规范进行比较。我们回顾这个框架如何支持几种语言和编译输出格式，通过将它们翻译成基于Horn子句的中间表示，并使用该框架的可配置性来描述输入语言的资源语义。我们提供了一个更详细的形式化和扩展的框架，使资源使用规范和分析/验证输出可以包括前提条件表达区间的输入数据大小的断言是适用的，证明，或反驳。最重要的是，我们还扩展了可以检查的函数类。我们提供的Ciao/CiaoPP框架内的实施结果，并报告通过实例化这个框架的能源消耗规范的验证命令/嵌入式程序的工具。这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2018-03-12 cs.LO cs.PL
From Specifications to Behavior: Maneuver Verification in a Semantic State Space
fortiss GmbH（福蒂斯有限公司）；Technische Universität München（慕尼黑工业大学）
为了在可预见的未来实现自动驾驶汽车的市场进入，行为规划系统将需要遵守与人类相同的规则。如果不妥善解决审批陷阱，就无法强制执行产品责任。在本文中，我们定义了一个语义抽象的连续空间和形式化的交通规则的线性时序逻辑（LTL）。语义状态空间中的序列表示高级规划者可以选择执行的策略。我们检查这些演习对正式的交通规则，使用运行时验证。通过使用标准的模型检查器NuSMV，我们证明了我们的方法的有效性，并提供运行时属性的机动验证。我们表明，高层次的行为可以在语义状态空间中进行验证，以满足一组形式化的规则，这可以作为一个步骤，实现预期的功能安全。
2019-11-29 cs.LO cs.RO
Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems
本卷包含在第七届Web系统自动规范和验证国际研讨会（WWV 2011）上提交的论文的最终版本和修订版本。该研讨会于2011年6月9日在冰岛雷克雅未克举行，作为DisCoTec 2011的一部分。WWV研讨会系列的目的是提供一个跨学科的论坛，以促进交叉施肥和混合方法的发展，这些方法利用了基于规则的编程，软件工程，形式化方法和面向Web的研究的概念和工具。如今，许多公司和机构已经将其网站转向交互式、完全自动化的基于Web的应用程序，例如，电子商务、电子学习、电子政务和电子卫生。Web系统复杂性的增加和爆炸性的增长使其设计和实现成为一项具有挑战性的任务。系统的，正式的方法，他们的规格和验证可以允许通过自动化和有效的技术和工具来解决这个特定领域的问题。为了响应今年的论文征集，我们收到了9份论文。WWV 2011的计划委员会为每篇论文收集了三篇评论，并进行了电子讨论，最终选出7篇论文在研讨会上发表。除了选定的论文外，科学方案还包括邀请Elie Najm发表演讲。
2011-08-10 cs.LO cs.SE
Modeling and Verification of Agent based Adaptive Traffic Signal using Symbolic Model Verifier
本文讨论了多Agent系统（MAS）场景的建模与验证问题。我们已经考虑了基于代理的自适应交通信号系统。该系统监测两个路段交叉口的交通畅通。在描述了如何有效地使用自适应交通信号灯系统，并显示其优势，交通信号与预定的周期，我们已经展示了如何将这种情况下，我们可以转换为有限状态机（FSM）。一旦系统被转换成FSM，我们已经验证了规范中指定的计算树逻辑（CTL）使用NuSMV作为模型检验工具。从NuSMV获得的仿真结果表明，我们是否满足系统的规格或不。它还向我们展示了系统规范不成立的状态。使用它我们可以追溯到我们的系统，找到源，导致规范违反。最后，我们再次验证了修改后的系统与NuSMV的规格。
2012-08-16 cs.LO cs.SE
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
Towards Energy Consumption Verification via Static Analysis
在本文中，我们利用现有的一般框架资源使用验证和专门验证嵌入式程序的能耗规格。这样的规范可以包括能量使用的下限和上限，并且它们可以表示能量使用被证明在这样的界限内的间隔。区间的界限通常可以作为输入数据大小的函数给出。我们的验证系统可以证明是否符合此类能源使用规范。它还可以推断出这些规范所适用的特定条件。为此，这些条件也被表示为输入数据大小的函数的区间，使得给定的规范对于某些区间可以被证明，而对于其他区间可以被证伪。规范本身还可以包括表示输入数据大小的间隔的先决条件。我们报告的XC语言和XS 1-L架构的CiaoPP系统内的方法的原型实现，并举例说明嵌入式软件开发人员可以如何使用这个工具，特别是确定值的程序参数，确保满足给定的能源预算，同时最大限度地减少损失的服务质量。
2015-12-31 cs.DC cs.LO cs.PL
Formal Requirement Elicitation and Debugging for Testing and Verification of Cyber-Physical Systems
School of Computing, Informatics and Decision Systems Arizona State University（亚利桑那州立大学计算、信息与决策系统学院）
本文提出一个用于物理系统形式化规格的 elicitation 与调试框架，通过图形界面处理规格 elicitation，提供两种调试算法以解决规格错误，通过用户研究验证框架能有效解决常见规格错误。
2018-07-27 cs.LO cs.SE cs.SY
Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
本文提出用混合zonotope后向可达性分析构造时序逻辑树，以计算高效且能表示非凸、不相交几何形状的方式形式化验证自主系统的LTL规范。
2024-04-04 cs.LO cs.SY eess.SY
Preguss: It Analyzes, It Specifies, It Verifies
针对LLMs在形式化验证中因上下文限制和复杂规范推断难导致的可扩展性问题，本文提出模块化细粒度框架Preguss，协同静态分析与演绎验证，通过RTE引导验证单元构建及LLM辅助单元级过程间规范合成，助力大规模程序自动化验证。
2025-08-20 cs.LO cs.SE
Varanus: Runtime Verification for CSP
School of Computer Science, University of Nottingham（诺丁汉大学计算机学院）；University of Modena and Reggio Emilia（摩德纳和雷焦艾米利亚大学）
针对CSP缺乏运行时验证工具的问题，提出Varanus工具，可复用CSP规约构建预言机监控系统，在核废料巡检模拟场景中验证了其违规检测能力，且监控器生成与事件检查效率较高。
2025-06-17 cs.LO cs.SE
Specification and Automatic Verification of Computational Reductions
本文提出 cookbook reductions 这一图形化归约规范机制，证明其表达力足以覆盖经典图归约并保持 SAT 的 NP 完全性，同时验证问题在自然子类上是可判定的。
2024-07-04 cs.CC cs.LO
Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling
本文倡导在气候建模中采用形式化方法，识别适合形式化规格说明的ESM关键方面，提出抽象方法，并通过CIVL模型检查器验证海洋混合参数化方案修复的案例，旨在开发领域特定工具以提升模式可靠性与开发效率。
2025-10-15 cs.LO cs.MS
Verifying Verified Code
Chong等人最近在AWS的一个案例研究中提出了一种有效的工业界有界模型检验方法。在本文中，我们报告了一个后续的案例研究，从三个研究问题的角度探讨了方法：（a）证明工件可以跨验证工具使用;（b）验证代码中是否存在错误;（c）规范是否可以改进。为了研究这些问题，我们将$\texttt{aws-c-common}$库的验证任务移植到SEAHORN和KLEE。我们展示了使用编译器语义和交叉检查规范与不同的验证技术的好处，并呼吁标准化证明库扩展，以增加规范的重用。讨论的核查任务可在网上公开查阅。
2021-07-01 cs.LO cs.SE
KindHML: formal verification of smart contracts based on Hennessy-Milner logic
Università degli Studi di Cagliari（卡利亚里大学）；Università degli Studi di Modena e Reggio Emilia（摩德纳与雷焦艾米利亚大学）；Télécom Paris, Institut Polytechnique de Paris（巴黎电信学院，巴黎理工学院）
本文提出一种自动化方法，用于验证智能合约的复杂时间属性，通过将Solidity合约和Hennessy-Milner逻辑的时间规范编码到Lustre中，利用Kind 2模型检查器进行验证，有效检测现有工具无法发现的攻击漏洞。
2026-04-15 cs.CR cs.LO
