Formal Semantics and Verification of Procedural SQL Programs Implementing Materialized Data Integration

The increasing heterogeneity of data models and schemas of numerous data sources makes data integration more and more urgent. Data integration programs can be very complicated, and therefore, formal verification of their correctness becomes important. The paper proposes a method for verification of programs for materialized data integration expressed in a procedural SQL dialect. The method is based on the definition of SQL program semantics in a formal specification language supported by automated provers. The method is illustrated by the verification of a program for materialized data integration in land use management.