Personal tools

Verified Data-structures and Algorithms

From PUMA Graduiertenkolleg

Jump to: navigation, search

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.

see "Aleksandr Karbyshev"