找到27个数据集

标签: 形式化验证

过滤结果

  • GitHub_Copilot_Based代码可验证性探索数据集

    2026年2月8日 30 97 36

    数据集概述 本数据集为“Exploring the Verifiability of Code Generated by GitHub Copilot”研究项目的配套数据，包含GitHub Copilot生成的Python代码实现，以及将其转换为Dafny语言并尝试验证的相关内容，用于研究代码生成工具的输出可验证性。 文件详解...
    packageimg

  • Separation_Logic_无限制效果处理程序实现与测试基准数据

    2026年2月6日 30 146 13

    数据集概述 本数据集为论文《Separation Logic for Unrestricted Effect Handlers》的支撑数据，包含分离逻辑无限制效果处理程序的最新实现代码与测试基准，以压缩包形式提供，用于支持相关研究的复现与验证。 文件详解 文件名称：speration_logic_for_effects.zip 文件格式：ZIP...
    packageimg

  • mCRL2_Based_符号奇偶游戏动态求解技术对比数据

    2026年1月30日 30 93 92

    数据集概述 本数据集包含一组mCRL2规格和公式，用于比较符号奇偶游戏的多种动态求解技术。这些技术对应论文《On-The-Fly Solving for Symbolic Parity Games》中的研究内容，数据集以压缩包形式提供，可用于验证不同求解方法的性能与效果。 文件详解 symbolic-artifact.zip 文件格式：ZIP...
    packageimg

  • Storm_Based_数据密集型应用瓶颈节点分析模型数据

    2026年1月29日 30 204 140

    数据集概述 本数据集包含一组表示Storm拓扑的模型描述文件，旨在支撑论文中提出的基于度量时序逻辑的数据分析方法，聚焦于Storm实现的数据密集型应用瓶颈节点分析。数据集仅含一个压缩文件，无目录层级结构。 文件详解 文件名称：ICFEM.zip 文件格式：ZIP...
    packageimg

  • D_VerT_Source_Storm拓扑形式化验证研究完整数据2017

    2026年1月21日 30 52 33

    数据集概述 本数据集为论文《Formal Verification of Storm Topologies through D-VerT》的配套研究数据，包含论文中展示的UML模型、D-VerT自动生成的时序逻辑模型实例及实验输出文件，用于支持Storm流处理拓扑的形式化验证研究，总计一个压缩文件。 文件详解 文件名称：SAC2017.zip...
    packageimg

  • Kaki_Concurrent_Update_Synthesis_制品包

    2026年1月21日 30 162 74

    数据集概述 本数据集是论文"Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games"的配套制品包，包含运行Kaki工具、生成实验问题及复现论文结果所需的文件，帮助使用者验证Kaki工具的功能与实验结论。 文件详解...
    packageimg

  • ICBC_Cross_chain_workshop_Event_B形式化区块链互操作性方案验证数据

    2026年1月7日 30 83 8

    数据集概述 本数据集为论文"Formalising a Gateway-based Blockchain Interoperability Solution with Event-B"的复现包，包含Event-B形式化规范、规范动画及用例场景规范三类核心成果，用于验证网关跨链互操作性方案的安全性、功能性与实用性，涉及以太坊与Hyperledger...
    packageimg

  • ORM控制器摘要推理验证数据集

    2025年12月20日 30 58 48

    数据集概述 本数据集包含基于摘要推理的ORM控制器验证相关的实验结果与代码文件，对应研究论文不同章节的内容，涵盖控制器验证、多页数据检查、突变分析、JPF验证等模块，为ORM控制器的形式化验证研究提供支持。 文件详解 压缩文件： icse2022-subm-data-1008-orm-...
    packageimg

  • 量子模拟验证编译器工件

    2025年12月23日 30 140 65

    数据集概述 该数据集是论文《A Verified Compiler for Quantum Simulation》的配套工件，包含名为QBlue的首个基于二次量子化的哈密顿量模拟验证编译框架相关内容，为量子模拟编译研究提供支持。 文件详解 该数据集包含一个压缩文件，具体说明如下： - 文件名称: qblue.zip - 文件格式: ZIP (.zip)...
    packageimg

  • FMICS2021出版物_系统需求形式化分析案例研究_补充数据集

    2025年12月23日 30 203 121

    数据集概述 本数据集为FMICS2021出版物《系统需求形式化分析案例研究》的补充数据，含UMC、ProB、LNT模型、SECURail交付物及翻译工具源码，以PDF文档和压缩包形式存储，支撑相关研究的细节验证与扩展分析。 文件详解 文档类文件（.pdf格式）：共4个 TIN15-v5.pdf：具体内容未详细说明的PDF文档...
    packageimg

  • JavaSMT框架扩展与Bitwuzla求解器评估基准数据集

    2025年12月22日 30 195 165

    数据集概述 该数据集是论文《Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker》的基准文件，包含评估JavaSMT框架扩展及Bitwuzla求解器性能的相关数据文件。 文件详解...
    packageimg

  • 自主机器人形式化模型保障案例演进补充材料

    2025年12月22日 30 144 83

    数据集概述 本数据集为论文《自主机器人形式化模型保障案例演进》的补充材料，包含保障案例模式的详细说明、Isabelle/SACM实现、实例化内容及相关Isabelle脚本，为理解论文核心内容提供补充支持。 文件详解 文件名称: main-suppl.pdf 文件格式: PDF (.pdf) 文件内容: 包含论文相关的补充材料，具体涵盖：...
    packageimg

  • Intel_TDX_Module_Based_安全验证基准测试完整数据集

    2025年12月22日 30 142 78

    数据集概述 该数据集包含Intel TDX模块（版本1.5.05）的源代码、验证工具集、衍生验证任务及任务生成脚本与工具，支持基于不同初始化策略生成验证任务，适用于Intel TDX模块的安全性与可达性验证研究。 文件详解 核心目录结构： intel-tdx/src/: Intel TDX模块源代码（版本1.5.05） intel-...
    packageimg

  • MCComp_2025_攻击者控制与漏洞优先级排序基准数据集

    2025年12月21日 30 104 90

    数据集概述 该数据集是面向投影模型计数的CNF公式基准，基于《攻击者控制与漏洞优先级排序》（USENIX Security 2025）的研究工件构建，包含一百六十二组对应真实程序定量控制问题的公式（其中一百三十七组源自CVE），用于MCComp 2025竞赛。 文件详解 文档类文件：...
    packageimg

  • 何塞_安东尼奥定理的形式化与证明数据集

    2025年12月20日 30 181 20

    数据集概述 本数据集包含何塞·安东尼奥定理的形式化表述与证明文档，聚焦等腰直角三角形（TRI）内的几何关系，探讨其与黄金比例的关联，并通过AHXIOM格式呈现定理的逻辑结构与直观解释。 文件详解 文件名称: 1∅∅∅ SCod Teorema de José Antonio- Formalización y Demostración TRI.pdf...
    packageimg

  • TACAS_25论文实验材料_性能启发式GR_1_可实现性检查与相关分析

    2025年12月20日 30 202 50

    数据集概述 本数据集是TACAS'25论文《性能启发式GR(1)可实现性检查与相关分析》的配套实验材料，包含实验测试文件、结果数据、分析文档及环境配置文件，为复现论文实验及验证方法性能提供支持。 文件详解 文档类文件： LICENSE.txt：TXT格式，包含BSD 3-Clause开源许可协议内容，涉及版权归属与使用条款...
    packageimg

  • 一阶线性时态逻辑规范验证的位向量逻辑编码实验评估数据集

    2025年12月20日 30 181 118

    数据集概述 本数据集是论文《How Bit-Vector Logic Can Help Improve the Verification of First-Order LTL Specifications》中提出的位向量逻辑编码方法的实验评估数据，包含模型描述、实验文件及相关插件压缩包。 文件详解...
    packageimg

  • 分支LSCs挖掘数据集

    2025年12月18日 30 80 25

    数据集概述 该数据集包含两个面向对象应用程序（CrossFTP和Columba）的执行轨迹数据，以及使用不同参数挖掘线性时间和分支时间场景（以Live Sequence Charts形式）的实验结果，还包含一个描述数据与实验的索引文件。 文件详解 index.html: HTML格式文件，描述数据集内容与实验信息。 crossftp.xes.gz:...
    packageimg

  • Linux内核任务调度器函数select_idle_core形式化验证案例研究数据集

    2025年12月15日 30 11 4

    数据集概述 该数据集包含针对Linux内核任务调度器函数select_idle_core进行形式化验证的实验代码与规范文件，支撑"Understanding Linux-Kernel Code Through Formal Verification..."论文研究，为内核代码验证提供实践数据。 文件详解 文件名称: artifact.zip 文件格式:...
    packageimg

  • C程序形式化验证高效技术_SV_COMP2022数据集

    2025年12月15日 30 59 19

    数据集概述 本数据集包含工具Theta在SV-COMP 2022的最后一轮预运行基准测试结果，由SV-COMP 2022组织者执行，相关评估见于学士论文，旨在为论文读者提供可访问的基准结果存档。 文件详解 该数据集包含十八个文件，具体说明如下： - 核心基准结果文件（.bz2格式，共十三个）： -...
    packageimg