Tags:data flow, program verification and tree automata
Abstract:
Data flow proofs, which are classically based on data flow graphs, bear a promising practical potential for automatic verification. We base a fundamental investigation of data flow proofs on the notion of a data flow tree, which allows us to capture data flow at a finer level of granularity than data flow graphs. In particular, we characterize the exact relation between the data flow in actual executions and the data flow represented by the data flow graph.