Email Gateway (Dec 24 2025 at 15:36): Email Gateway (Dec 24 2025 at 15:36):From: Tobias Nipkow <nipkow@in.tum.de>
Dynamic Pushdown Networks
Peter Lammich
We present a formalization of Dynamic Pushdown Networks (DPNs) and the automata
based algorithm for computing backward reachability sets using Isabelle/HOL.
Dynamic pushdown networks are an abstract model for multithreaded,
interprocedural programs with dynamic thread creation that was presented by
Bouajjani, Müller-Olm and Touili in 2005. We formalize the notion of a DPN in
Isabelle and describe the algorithm for computing the
-set from a regular set of configurations, and prove its correctness. We first
give a nondeterministic description of the algorithm, from that we then infer a
deterministic one, from which we can generate executable code using Isabelle's
code-generation tool.
https://www.isa-afp.org/entries/Dynamic_Pushdown_Networks.html
Merry Christmas!
Last updated: Jan 11 2026 at 16:28 UTC