Unpublished Isabelle/HOL Related Projects

Formalization of pre* for DPNs

Peter Lammich

(Preliminary version, not yet published)

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 $pre^*$-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.

Proof Document
Proof Outline
Isabelle Sources (Not stripped, contains some unrelated/obsolete stuff)

TODO-List until final version:

Kill/Gen Analysis for Programs with Procedures and Thread Creation

Peter Lammich
May 2006

Formalization of kill/gen forward analysis for programs with Procedures and Thread Creation
The formalization was done related to my diploma thesis, and later extended, but never put into a consistent shape suitable for publication.

Our paper Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures describes (a generalization of) the analysis.