Unpublished Isabelle/HOL Related Projects
Formalization of pre* for DPNs
Peter Lammich
2007
(Preliminary version, not yet published)
Abstract
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:
- Make efficient implementation, using collection's framework. The current implementatioon is executable, but really slow.
- Perhaps extend to witness computation: The saturation algorithm can compute a tree-regular representation of all executions that lead from a start to an end configuration.
- Perhaps extend to weighted DPN (WDPN), a DPN model where transitions are assigned weights, and one computes the join of the weights of all executions.
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.