Applications range from formal language theory to program

analysis and verification, concurrency control and the design of

algorithms. This talk surveys recent extensions of Kleene algebras by

modal operators. It sketches the axiomatisation and calculus of modal

Kleene algebras, some interesting models, such as traces, graphs,

relations and predicate transformers, and their connection with

Boolean algebras with operators, propositional dynamic logics and

temporal logics. A particular benefit of the algebraic approach is

that some complex analysis tasks that previously required higher-order

reasoning can, for the first time, be fully automated through

equational reasoning with off-the-shelf theorem provers. This is

illustrated through several examples: program analysis in Hoare logic,

Bachmair and Dershowitz's termination theorem for rewrite systems,

Back's atomicity refinement theorem and a correspondence proof

of Loeb's formula in modal/provability logic.

Robert Recorde Room

Department of Computer Science