Proving correctness for SQL implementations of OCL constraints

ficantly less efficient -- from the point of view of execution-time performance -- than the implementations manually written by database experts. In this paper, we propose a different approach to bridge the gap between models with OCL constraints and their corresponding database implementations. In particular, we introduce a model-based methodology for proving the correctness of manually written SQL implementations of OCL constraints. This methodology is based on a novel mapping from a significant subset of the SQL language into many-sorted first-order logic. Moreover, by leveraging on an already existing mapping from the OCL language into many-sorted first-order logic, we can use SMT solvers to automatically prove the correctness of SQL implementations of OCL constraints. To illustrate and show the applicability of our approach, we include in the paper a number of non-trivial examples. Finally, we report on the status of a suite of tools supporting our approach.