Formalizing Weighted Pushdown Systems in Isabelle/HOL

Pushdown systems are a fundamental formalism in computer science with applications in model checking and program analysis. As a generalization, weighted pushdown systems associate transitions in pushdown systems with weights, thus allowing one to calculate the cost of reaching configurations, where the cost is measured over an algebraic structure. Several model checkers and program analysis tools apply libraries for weighted pushdown system reachability. In this paper, we formalize weighted pushdown systems in Isabelle/HOL. Specifically, we formally prove the correctness of an algorithm for reachability in such systems and extract a verified implementation of the algorithm as a functional program. This requires us to formalize bounded idempotent semirings and sums over countably infinite sets of their elements, as well as saturation procedures that compute these sums. We use differential testing to compare our implementation with a state-of-the-art implementation called PDAAAL. Our testing revealed an error in PDAAAL which we have remedied.