Download PDFOpen PDF in browser

Syntactic and Semantic Soundness of Structural Dataflow Analysis

EasyChair Preprint 1645

31 pagesDate: October 12, 2019

Abstract

We show that the classical approach to the soundness of dataflow analysis is with respect to a syntactic path abstraction that may be problematic with respect to a semantics trace-based specification. The fix is a rigorous abstract interpretation based approach to formally construct dataflow analysis algorithms by calculational design.

Keyphrases: Semantic Definition, Semantic Soundness, Trace semantic, abstract interpretation, calculational design, dataflow analysis, deadness abstraction, definite deadness, definite liveness, flow analysis, liveness analysis, liveness analysis algorithm, maximal trace semantic, potential live variable algorithm, potential liveness, prefix trace, soundness, structural dataflow analysis, structural induction

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:1645,
  author    = {Patrick Cousot},
  title     = {Syntactic and Semantic Soundness of Structural Dataflow Analysis},
  howpublished = {EasyChair Preprint 1645},
  year      = {EasyChair, 2019}}
Download PDFOpen PDF in browser