{"entities":{"Q7361875":{"pageid":31521164,"ns":120,"title":"Item:Q7361875","lastrevid":105369974,"modified":"2026-10-07T13:38:44Z","type":"item","id":"Q7361875","labels":{"en":{"language":"en","value":"Dynamic Pushdown Networks"}},"descriptions":{"en":{"language":"en","value":"AFP entry Dynamic_Pushdown_Networks"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"352a4b212afedc9161e16e25dc27ca8e06b00563","datavalue":{"value":"https://isa-afp.org/entries/Dynamic_Pushdown_Networks.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361875$A5AC3BA5-3115-4A0A-9941-59DA38D699C6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ced0407c121e1fe8f98dc4fd0d9d692157131171","datavalue":{"value":{"time":"+2025-12-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361875$3666881E-7AAF-4F76-B3DF-4F11F8C63590","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361875$80B704B7-8B25-4554-ABCC-19736AFD8C88","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5ffffcbd5561159e585873238f6ad1eda0b42e66","datavalue":{"value":{"text":"Dynamic Pushdown Networks","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361875$BC389245-2BDF-475E-8B7E-09B3C6E5C807","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a97d87ccefed5b20afa4ca52166dba63af9bae8c","datavalue":{"value":"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\u00fcller-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.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361875$CB6FF309-3072-4DB1-833C-F89CDA3DA415","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b614d2d330f36bdd9ecd3e94fb292809877a0f54","datavalue":{"value":{"entity-type":"item","numeric-id":5307073,"id":"Q5307073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$52D912AC-D7B7-460C-A949-0172338D17AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34c82e9f6dc46a17a1531710a1314df285e95f1c","datavalue":{"value":{"entity-type":"item","numeric-id":5897502,"id":"Q5897502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$81DA1A52-98C8-45B7-AA0F-DDAA10A9BAAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"763d845caa57489776d3b781ab08fe29f3b63057","datavalue":{"value":{"entity-type":"item","numeric-id":4274278,"id":"Q4274278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$FE82C7C4-486B-45F5-A3B9-9B2D320FE2E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$C4A15B35-0353-42C2-A231-FC971A9501FF","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$451A22CA-EF41-45BD-AEC3-3720A3C93ED4","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"27e971e25f48a406ca09caf18a9e463d40cb63ef","datavalue":{"value":{"entity-type":"item","numeric-id":7361166,"id":"Q7361166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$051742BF-D50B-41B5-8FFB-AAE68B9B2F94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"42f5e878637080193430cb67c74dd886376e6e01","datavalue":{"value":{"entity-type":"item","numeric-id":7361823,"id":"Q7361823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$67B20D66-BD93-4BED-A1BD-9325EC7340FB","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ec084f2f33463e96367d261c341919d2f3128032","datavalue":{"value":{"entity-type":"item","numeric-id":7360771,"id":"Q7360771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$F7BBB07A-2A4A-419F-9F23-DA7809FE738D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$0F3AC613-67E0-4BDC-B4E8-A59894D0203B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"b721b89857a714d14089f2631e7d6953fb3d481c","datavalue":{"value":{"entity-type":"item","numeric-id":7360799,"id":"Q7360799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$C46D3B58-3F18-437F-B4A5-761D9555A255","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361875$951C61D1-65AB-4A03-9F9A-37575A879DCC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Dynamic Pushdown Networks","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Dynamic_Pushdown_Networks"}}}}}