GKAT with Hoare Hypotheses

<div class="elementToProof"><em>By Dr. Jana Wagemaker</em><br> <br> <strong><u>Abstract</u></strong></div> <div class="elementToProof">Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra and it is an algebraic framework that allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the talk we start with context on Kleene algebra and GKAT, and then we address the challenge of reasoning under assumptions about these GKAT programs. In particular, we develop a form of Hoare hypotheses,