Saturation Meets SMT: Locality-Aware Reachability over Logical Predicates (Accompanying Artifact)

The artifact accompanies the paper “Saturation Meets SMT: Locality-Aware Reachability over Logical Predicates” submitted to FMCAD 2026. It contains everything needed to reproduce the paper’s figures from pre-recorded benchmark results and to re-run the benchmarks from scratch. The artifact is organized into three main directories:- benchmarking/: benchmark definitions, tool binaries, execution scripts, and benchmark results- plots/: scripts and data for regenerating all figures and tables from the paper- third-party-licenses/: license files for bundled third-party tools The artifact bundles Theta 6.28.0, ITS-reach 0.2.20250911075655, LTSmin 3.0.2, Z3 4.5.0, and BenchExec 3.30-dev. Requirements:- Docker- sudo access for temporarily adjusting an AppArmor kernel setting required by BenchExec on Ubuntu 24.04+ The artifact was tested on Ubuntu 24.04.3 LTS (x86_64). The plots directory already contains the raw BenchExec result files used in the paper, so reviewers can regenerate all figures immediately without re-running benchmarks. The generated output is a self-contained PDF containing all plots and tables from the paper. The benchmarks cover three domains:- DVE models from the BEEM suite- Petri net models from the 2025 Model Checking Contest- Software concurrency benchmarks from the SV-COMP concurrency category A smoke test is included and runs 5 models from each domain across most tool configurations in roughly 30 seconds. The full benchmark set contains 300 DVE models, 1617 Petri net models, and 726 software concurrency benchmarks across 20 tool configurations. Each task runs with a 15-minute timeout, 15 GB memory limit, and 2 CPU cores. Full execution may take weeks on a single machine and is primarily intended for compute clusters. Scripts for VerifierCloud / BenchCloud execution are included. For detailed instructions, command-line options, and output locations, please refer to the included README files:- main README: overall artifact structure and quick start- benchmarking/README.md: benchmark execution and cluster usage- plots/README.md: figure regeneration and plotting pipeline本实验附属材料对应投稿至FMCAD 2026的论文《Saturation Meets SMT: Locality-Aware Reachability over Logical Predicates》（饱和算法结合SMT：基于逻辑谓词的局域性感知可达性分析），其中包含了从预录制的基准测试结果复现论文图表所需的全部资源，以及从零开始重新运行基准测试的完整流程。 本附属材料分为三个核心目录： - benchmarking/：基准测试定义、工具二进制文件、执行脚本与基准测试结果 - plots/：用于重新生成论文中全部图表与表格的脚本与数据 - third-party-licenses/：捆绑的第三方工具的许可文件 本附属材料集成了Theta 6.28.0、ITS-reach 0.2.20250911075655、LTSmin 3.0.2、Z3 4.5.0以及BenchExec 3.30-dev。 ### 依赖要求 - Docker - 针对Ubuntu 24.04及以上版本，需具备sudo权限以临时调整BenchExec所需的AppArmor内核设置 本附属材料已在Ubuntu 24.04.3 LTS (x86_64) 环境下完成测试。 plots目录已包含论文中使用的原始BenchExec结果文件，因此评审人员可直接重新生成全部图表，无需重新运行基准测试。最终生成的输出为包含论文所有图表与表格的独立PDF文件。 本次基准测试覆盖三大领域： 1. BEEM套件中的DVE模型 2. 2025年模型检查竞赛（Model Checking Contest）中的Petri网模型 3. SV-COMP并发类别下的软件并发基准测试 本附属材料内置冒烟测试，可在约30秒内针对多数工具配置运行每个领域中的5个模型。 完整基准测试集包含300个DVE模型、1617个Petri网模型以及726个软件并发基准测试，覆盖20种工具配置。每项任务的运行超时时间为15分钟，内存限制为15GB，使用2个CPU核心。单台机器运行完整测试集可能需要数周时间，主要适用于计算集群，附带了适用于VerifierCloud / BenchCloud执行的脚本。 如需获取详细操作指南、命令行选项与输出位置，请参阅附带的README文件： - 主README：整体附属材料结构与快速入门指南 - benchmarking/README.md：基准测试执行与集群使用说明 - plots/README.md：图表重新生成与绘图流程说明