Proving correctness of the query containment solver SpeCS using SPARQL set semantics

Abstract

Solving the SPARQL query containment problem is of fundamental importance for the verification and optimization of SPARQL queries. With the increasing popularity of the Semantic Web and its applications, SPARQL query containment solvers face significant challenges: covering a wide range of language constructs, achieving high efficiency, and guaranteeing correctness. While language coverage and efficiency can be reliably evaluated by testing with relevant benchmarks, we need formal proof of correctness to ensure the trustworthiness of a tool. In this paper, we prove the correctness of SPECS a highly efficient state-of-the-art query containment solver that supports reasoning about queries containing all commonly used SPARQL language constructs. We outline set semantics that cover the most common subset of the SPARQL language and give precise definitions of all fundamental SPARQL concepts. We briefly discuss the procedure used by SPECS for reducing the query containment problem into a formal logical framework. We prove that this procedure is both sound and complete for conjunctive queries as well as for some important classes of non-conjunctive queries (queries containing the union operator, the optional operator, and subqueries). We consider soundness and completeness in both containment and subsumption forms. We also discuss the advantages of solver development driven by correctness proofs.