Key points are not available for this paper at this time.
摘要 基准测试是实验计算机科学中广泛使用的方法,特别是用于工具和算法的比较评估。因此,需要回答一些问题,以确保适当的基准测试、资源测量和结果呈现,这对研究人员、工具开发者和用户,以及工具比赛都是至关重要的。我们确定了一组对于自动求解器、验证器和类似工具的时间和内存使用的可靠基准测试和资源测量不可或缺的要求,并讨论了现有方法和基准工具的局限性。在基准测试框架中满足这些要求,当前(在Linux系统上)只能通过使用内核的cgroup和命名空间功能来实现。我们开发了BenchExec,这是一个即用型、工具独立的开源基准测试框架的实现,满足所有呈现的要求,使可靠的基准测试和资源测量变得简单。我们的框架能够与广泛的不同工具一起工作,在国际软件验证竞赛中证明了其可靠性和有效性,并被多国研究小组用于确保可靠的基准测试。最后,我们提供了关于如何以科学有效和易于理解的方式呈现测量结果的指南。
Beyer等人(周五)研究了这个问题。