Description

Title Formal verification of data provenance records
Abstract Data provenance is the history of derivation of a data artifact from its original sources. Tracking and recording such histories is crucial for facilitating reuse and management of data produced by computation intensive applications, such as used in the e-science domain. Formally, a provenance record can be seen as a directed graph with certain nodes associated with data artifacts, and as such, it bears some resemblance to the standard notion of a transition system. This suggests a possibility of adopting some common formal verification techniques based on different dynamic logics (program verification logics) to the problem of checking formal properties of provenance records. In this presentation I will outline our first steps towards designing such a logic-based verification formalism. (This is a joint work with L. Serafini, FBK Trento)