### Abstract

This entry formalises the fast iterative algorithm for computing dominators due to Cooper, Harvey and Kennedy. It gives a specification of computing dominators on a control flow graph where each node refers to its reverse post order number. A semilattice of reversed-ordered list which represents dominators is built and a Kildall-style algorithm on the semilattice is defined for computing dominators. Finally the soundness and completeness of the algorithm are proved w.r.t. the specification.

### License

BSD License

### Topics

- Computer science/Programming languages/Static analysis

### Session Dominance_CHK

- Cfg
- Sorted_Less2
- Sorted_List_Operations2
- Dom_Semi_List
- Dom_Kildall
- Dom_Kildall_Property
- Dom_Kildall_Correct

### Depends on

- Jinja is not Java
- List Index

### Auto-related entries

- Shivers' Control Flow Analysis

## Cite

×

Dominance_CHK-AFP

    @article{Dominance_CHK-AFP,
      author  = {Nan Jiang},
      title   = {A data flow analysis algorithm for computing dominators},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Dominance_CHK.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Sep 7, 2021 : Isabelle2021