一句话：提出 BenchCloud，一个与 BenchExec 集成的弹性可扩展基准测试平台，支持跨数百节点的大规模工具性能评测。
自动化推理工具的性能评测需要严格测量时间与内存等资源消耗，而广泛使用的基准测试框架 BenchExec 只能可靠地测量在单节点本地执行的工具。本文提出 BenchCloud，一个面向数百节点的弹性、可扩展作业分发平台，支持在分布式异构计算环境中进行大规模实验。BenchCloud 与 BenchExec 无缝集成，允许 BenchExec 将实际执行委托给 BenchCloud。该系统已用于 SMT-COMP、SV-COMP 和 Test-Comp 等多个知名国际自动推理竞赛，保障了实验结果的内外部有效性。论文概述了 BenchCloud 的架构，并重点介绍了其在可扩展基准测试中的主要用例。
Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and highlights its primary use cases in facilitating scalable benchmarking.