{"entities":{"Q40946":{"pageid":41002,"ns":120,"title":"Item:Q40946","lastrevid":105427376,"modified":"2026-10-09T10:07:28Z","type":"item","id":"Q40946","labels":{"en":{"language":"en","value":"AODV"}},"descriptions":{"en":{"language":"en","value":"AFP entry AODV"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"391f4d1bc839058d828cff42a4d47d17474e9048","datavalue":{"value":"29232","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40946$91FA94B0-95A1-40C8-88C3-87FB803C0FF8","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"f241d10a14bae0fd87391cabd84bb715c64aa126","datavalue":{"value":{"entity-type":"item","numeric-id":3457779,"id":"Q3457779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$909D42B2-7685-4C98-BD8C-A143630A10B2","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":"Q40946$E5A689B2-0415-4748-9EB4-0F7EF98A95C4","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"fc4463c58057eacd057cf525b88a2ee95d73ec41","datavalue":{"value":"https://www.isa-afp.org/entries/AODV.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40946$D397FD10-B5C6-4032-A388-4B9092073A2B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40946$DAD176B1-BBBF-4CC4-9821-4D736C0A2AD0","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"678b0b96157ea336e6c854b12f6f087351e83672","datavalue":{"value":{"entity-type":"item","numeric-id":15523,"id":"Q15523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$F02BDAF8-943F-4040-AE35-9CAEC4717866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1a13081736616da9f90fce82f89953fc6e18e56a","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$B8E33944-561F-45FC-8277-66334613501F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e6d2e04e15e4ff7c5352e03cfb60cfa3a47ea2e8","datavalue":{"value":{"entity-type":"item","numeric-id":16871,"id":"Q16871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$4C78192A-0C5E-4687-AC40-FA7EB3BD711F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0566ad334499237f2689386a24c3ff4452487d83","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$5E32C21E-50CE-4860-B618-C8C68E69FA77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ec1fbb0215e78def1ae9dec82cef015c02ce483","datavalue":{"value":{"entity-type":"item","numeric-id":27099,"id":"Q27099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$81E85198-4FEB-484E-9F60-C5634C25807F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$5C4A3547-1D40-4767-AC8F-FFE9FFDAA0C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$3E3251A5-E591-45B7-884E-5B6AB100FE7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7d415c0e796201decc94b5dc4e3ee671f2a4aa29","datavalue":{"value":{"entity-type":"item","numeric-id":21698,"id":"Q21698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$1D3B4309-BDC4-4E70-BD74-45E770A4FB34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9a2b11711042f0541d30a89aab2f1c4ade7b181a","datavalue":{"value":{"entity-type":"item","numeric-id":18650,"id":"Q18650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$714D6081-E284-4C3E-BDC3-086A30A3948C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$07C5290F-F2EF-44FF-BDCC-E71D590E1B91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ef831e16728dd07d011e57e6a7022c6842248dc4","datavalue":{"value":{"entity-type":"item","numeric-id":14250,"id":"Q14250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$A5FBABD5-4D6B-4799-9B61-59F8BF4FC4E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$E0793A5D-DBD8-4289-B531-4D4842AC7B84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"02b329e86bd44e002b407e5543cbe998c79c263a","datavalue":{"value":{"entity-type":"item","numeric-id":13928,"id":"Q13928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$FADD0EBC-1258-4AC1-B827-2DAC31DE369D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"446c33bf9b374ba0441e5f70667e3e0c13ccd355","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$B5800D27-E615-403B-BD72-51AA9D00CA17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f4fb518d3fd3a5c86906e09c5e1de9482d064570","datavalue":{"value":{"entity-type":"item","numeric-id":15706,"id":"Q15706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$EA81043D-217A-4BD2-A726-F3573A65744C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ea33959c08006f6073c1d1044d21ffca8f0fd427","datavalue":{"value":{"entity-type":"item","numeric-id":14230,"id":"Q14230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$99469C11-23BD-4CE0-B560-2F3C9E14FC39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6e300a4466d9ec0556ff7a6ef4303dc0b276d981","datavalue":{"value":{"entity-type":"item","numeric-id":21405,"id":"Q21405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$88248D0F-4792-4967-A2DD-F549C67F3601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fa753181d4b27073ff8b4b61a14be56eafd4f3d","datavalue":{"value":{"entity-type":"item","numeric-id":32844,"id":"Q32844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$3E7F4386-BA99-4511-8956-694DACC91B74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"040a5b024d9c3570d1d035cd3b25cd7dce399d47","datavalue":{"value":{"entity-type":"item","numeric-id":40983,"id":"Q40983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$7E56C66C-D91B-41EC-982F-18A80EFEA79C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0a5ed045faab8b0f5b4ecff6640a5cf3e0873180","datavalue":{"value":{"entity-type":"item","numeric-id":41340,"id":"Q41340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$CD53C24B-C78F-456C-9034-F8784DE6925E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fd5a09cf243b417fa044469da811392eb6162aca","datavalue":{"value":"https://isa-afp.org/entries/AODV.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40946$E365C7E1-D86D-4A94-863D-45FEBA1B3A28","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"036f489f1dc46b1f48c264ce34d5fc443dd97960","datavalue":{"value":"Timothy Bourke","type":"string"},"datatype":"string"},"type":"statement","id":"Q40946$634FEDCE-7480-49B3-9172-0EDAD3B3CBD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"764f505c166c35794d03c474c0f8d7e266076240","datavalue":{"value":"Peter H\u00f6fner","type":"string"},"datatype":"string"},"type":"statement","id":"Q40946$9BA7CD71-7F60-4F7D-9313-4750AFEA4809","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"071a0f25af1fa694316df86e004ab982f9574f81","datavalue":{"value":"The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is \u2018loop free\u2019 if it never leads to routing decisions that forward packets in circles. This development mechanises an existing pen-and-paper proof of loop freedom of AODV. The protocol is modelled in the Algebra of Wireless Networks (AWN), which is the subject of an earlier paper and AFP mechanization. The proof relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several variants of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40946$7A7EBCB9-2846-41E8-AF23-29CFE32B9267","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e9b4f197e093b9f3851e4da2207cbd9f355017e","datavalue":{"value":{"entity-type":"item","numeric-id":464749,"id":"Q464749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$903C2C88-CCE7-43B8-BBE8-1C224E9891DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"905f170f8e42e6203f058d3f7d4bc86d94d9f927","datavalue":{"value":{"entity-type":"item","numeric-id":2879249,"id":"Q2879249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$BF4B4C6E-C830-46EC-A383-D85E9FA090B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f69289dc607d39e20a8a6da6cccd525739105c8f","datavalue":{"value":{"entity-type":"item","numeric-id":3457779,"id":"Q3457779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$CEED16EE-56F0-4B99-9F81-6B9E78A96FE0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19223fa13371e3ce1b1dd08c8b63557fc81ef3f8","datavalue":{"value":{"time":"+2014-10-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":"Q40946$5CBE30C3-00E3-4385-8A27-BADF607AE84F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8d926f51546ce3b5210db061854e023a3a51fb5f","datavalue":{"value":{"text":"Loop freedom of the (untimed) AODV routing protocol","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40946$A9F227B6-64E0-41C8-A7D2-7691D80D7F44","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":"Q40946$681F7B03-C7D0-45FF-91C7-450E98087D94","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c6ccde7215f9cdd5e84de357037dbe28d2b5c586","datavalue":{"value":{"entity-type":"item","numeric-id":7361509,"id":"Q7361509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$70D298D2-A8F0-4F36-88FB-F493B573A1C3","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"147d947971425f6e481a02787827e4705017a40a","datavalue":{"value":{"entity-type":"item","numeric-id":7360786,"id":"Q7360786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40946$6A3B83C8-2478-4262-917B-F7613F4A594F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"AODV","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/AODV"}}}}}