Domain Reasoning in TopKAT: Reduction and Completeness

Explore a 19-minute conference talk from the Theory and Practice of Static Analysis workshop (TPSA'25) that investigates domain reasoning in TopKAT (Kleene algebra with tests extended with a top element). Learn how researchers Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi from UCL, Rochester Institute of Technology, and Boston University examine the completeness properties of TopKAT with respect to relational models. Discover their findings that TopKAT is complete for (co)domain comparison of KAT terms but incomplete when comparing (co)domain of arbitrary TopKAT terms. Understand the implications of these results for program logic applications, particularly for proving under-approximate specifications and reachability properties in imperative programs. This ACM SIGPLAN-sponsored presentation was delivered at POPL25 on January 21, 2025.