Deciding KAT and Hoare Logic with Derivatives

Ricardo Almeida, Sabine Broda, Nelma Moreira

Kleene algebra with tests (KAT) is an equational system for program verification, which is the combination of Boolean algebra (BA) and Kleene algebra (KA), the algebra of regular e…