Verified Data-structures and Algorithms
From PUMA Graduiertenkolleg
Program analyses in compilers must satisfy certain performance demands. In order to keep the verification simple, modelling and verification of dataflow analyses in Isabelle or Coq so far have been on the purely functional level only. Also, the employed algorithms for fixpoint iteration have been very simple such as Kildall's algorithm. In contrast, it should now be tried to model and verify dataflow analyzers with imperative data-structures.