{"entities":{"Q7361011":{"pageid":31518572,"ns":120,"title":"Item:Q7361011","lastrevid":105362396,"modified":"2026-10-07T13:34:12Z","type":"item","id":"Q7361011","labels":{"en":{"language":"en","value":"A Framework for Verifying Depth-First Search Algorithms"}},"descriptions":{"en":{"language":"en","value":"AFP entry DFS_Framework"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"38d4a9634808f6329225f659d3783be328109753","datavalue":{"value":"https://isa-afp.org/entries/DFS_Framework.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361011$2D45C5AE-B5B5-4156-9251-7B9A1DD0F02F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96ffc2d0a9b6e5a88899520001cb0fe4528f891f","datavalue":{"value":{"time":"+2016-07-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361011$3BBA4B09-B838-49EC-8365-5E6DD5B9E13A","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361011$B5FA92A2-485F-4AB0-854D-B7FB95B96EB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0ecc22d00a75bcea18b023112e4b2e17fe97020a","datavalue":{"value":"Ren\u00e9 Neumann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361011$8C152D86-01F9-4B04-ABB1-5AE1875B2E88","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c4d327d9c02d771f97959b692d9a0f3f1d87383","datavalue":{"value":{"text":"A Framework for Verifying Depth-First Search Algorithms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361011$BEB8784F-C8A8-4D6C-A6B3-0D1235C11CC1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4727f7ad01eeeb80022d050634d549cd02b2afd3","datavalue":{"value":"This entry presents a framework for the modular verification of DFS-based algorithms, which is described in our [CPP-2015] paper. It provides a generic DFS algorithm framework, that can be parameterized with user-defined actions on certain events (e.g. discovery of new node). It comes with an extensible library of invariants, which can be used to derive invariants of a specific parameterization. Using refinement techniques, efficient implementations of the algorithms can easily be derived. Here, the framework comes with templates for a recursive and a tail-recursive implementation, and also with several templates for implementing the data structures required by the DFS algorithm. Finally, this entry contains a set of re-usable DFS-based algorithms, which illustrate the application of the framework. [CPP-2015] Peter Lammich, Ren\u00e9 Neumann: A Framework for Verifying Depth-First Search Algorithms. CPP 2015: 137-146","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361011$3155AB31-DE22-48DD-8A76-942677C913C1","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":"Q7361011$1376D3C1-DF2F-4844-8128-C7EC5BE7F83A","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"57153f9096aa0dddca483f863db49f1a20c72ecc","datavalue":{"value":{"entity-type":"item","numeric-id":7361530,"id":"Q7361530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361011$4DCF4769-A190-43C6-9F90-55356C04DF55","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0cb214ba14504ce52502380598f813a3d010fff5","datavalue":{"value":{"entity-type":"item","numeric-id":7360777,"id":"Q7360777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361011$E3C7F5A1-06C1-48B6-9EE4-530469324761","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":"Q7361011$3B295699-AC10-48DA-91E8-B4DC786011D6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Framework for Verifying Depth-First Search Algorithms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Framework_for_Verifying_Depth-First_Search_Algorithms"}}}}}