Verifying Equivalence of Spark Programs
Verifying Equivalence of Spark Programs
复制标题
验证 Spark 程序的等效性
DOI：
10.1007/978-3-319-63390-9_15
复制
发表时间：
2017
影响因子：
2.5
通讯作者：
Shmuel Sagiv
中科院分区：
文献类型：
--
作者：
Shelly Grossman;Sara Cohen;Shachar Itzhaky;N. Rinetzky;Shmuel Sagiv
Apache Spark是编写大型数据处理应用程序的流行框架。我们的长期目标是开发自动工具，以推理有关火花程序的推理。这是具有挑战性的，因为Spark程序将类似数据库的关系代数操作和汇总操作结合在一起，与（嵌套）循环相对应，以及用户定义的函数（UDFS）。在本文中，我们提出了一种基于SMT的新技术，用于验证SPARK程序的等效性。
Apache Spark is a popular framework for writing large scale data processing applications. Our long term goal is to develop automatic tools for reasoning about Spark programs. This is challenging because Spark programs combine database-like relational algebraic operations and aggregate operations, corresponding to (nested) loops, with User Defined Functions (UDFs). In this paper, we present a novel SMT-based technique for verifying the equivalence of Spark programs.