Conference paperHorn clauses and the fixpoint query hierarchyAshok K. Chandra, David HarelSIGMOD/PODS 1982
PaperProving the correctness of regular deterministic programs: A unifying survey using dynamic logicDavid HarelTheoretical Computer Science