Dataflow Analysis With Prophecy and History Variables

Martin Rinard, Austin Gadient

Leveraging concepts from state machine refinement proofs, we use prophecy variables, which predict information about the future program execution, to enable forward reasoning for b…