article · 2009

Formalization of Dynamic Pushdown Networks in Isabelle/HOL

Cited by 1Abstract and details only

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, Mller-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

Cite this paper

APA 7

Lammich, P. (2009). Formalization of Dynamic Pushdown Networks in Isabelle/HOL.

MLA 9

Lammich, Peter. “Formalization of Dynamic Pushdown Networks in Isabelle/HOL.” 2009.

Chicago

Lammich, Peter. 2009. “Formalization of Dynamic Pushdown Networks in Isabelle/HOL.”

Harvard

Lammich, P. (2009) ‘Formalization of Dynamic Pushdown Networks in Isabelle/HOL’.

BibTeX

@article{lammich2009formalization,
  title = {{Formalization of Dynamic Pushdown Networks in Isabelle/HOL}},
  author = {Lammich, Peter},
  year = {2009}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.