This project focuses on verifying correctness of Spark’s SQL operations and optimizations via Coq, a formal proof-management system. The first part of this project was done in my previous UROP experiences, which involved formalizing translation of SQL operations to builders, a core feature behind Spark for back-end optimization. After successfully developing the basic formalization, the goal of this SuperUROP project is to prove some optimizations for the formalized Spark’s SQL operations so that we can translate SQL queries to our formalized and optimized builders for fast querying while preserving the correctness of the output.

I’m participating in SuperUROP because I want to research and explore program verification that is, how to ensure that a program is semantically correct and runs as intended. I also want to learn more about tools and techniques for formalizing correctness of a program.