{"entities":{"Q40950":{"pageid":41006,"ns":120,"title":"Item:Q40950","lastrevid":105427418,"modified":"2026-10-09T10:07:34Z","type":"item","id":"Q40950","labels":{"en":{"language":"en","value":"DiskPaxos"}},"descriptions":{"en":{"language":"en","value":"AFP entry DiskPaxos"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"9430cc8278bcd312d86dff28127ea911a57efea2","datavalue":{"value":"29236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40950$BF8D0F45-E015-44E4-AA88-B571890D4D9D","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":"Q40950$461F13BE-7E51-4FD7-B438-9BEC0FFCAD80","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"1c8ae2c30b1dfa92e5c608e54a803f7616ed1349","datavalue":{"value":"https://www.isa-afp.org/entries/DiskPaxos.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40950$8BD6E4A3-A367-4663-8291-463A679C52CB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40950$739588D7-08E2-4ADA-AC86-5E72D5C48BCB","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$86217764-FEBA-4E77-BACF-B6EA2135EC67","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":"Q40950$8C283862-DCC5-4882-AD4B-F042C92415B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc571a8be4640388232f236c429044db5abc7030","datavalue":{"value":{"entity-type":"item","numeric-id":5972521,"id":"Q5972521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$D3A2855B-7DEC-4583-AAA7-BD70B8503109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"48c65ba4e4d38103c6617ad144591b105bb6b2b6","datavalue":{"value":{"entity-type":"item","numeric-id":21509,"id":"Q21509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$18AF5726-E7EE-424C-8D71-2C4F5B00D425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$2DDC5E64-9E84-43D0-BE1D-929204203157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0e25be57e1296470c78e495e58e23e70a4054e25","datavalue":{"value":{"entity-type":"item","numeric-id":40549,"id":"Q40549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$880FB393-97F1-4A07-8F2F-CEEB98C9EE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a5226fd137c2167e439294ca4cdc09da6fe13411","datavalue":{"value":{"entity-type":"item","numeric-id":40324,"id":"Q40324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$CC89F2C7-6811-4080-95F8-18E07EE52FA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e8320d126b57d987a786415a6e889261cd197254","datavalue":{"value":{"entity-type":"item","numeric-id":22297,"id":"Q22297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$90D2D35B-C391-43BA-AA23-562867EAB57E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dcac59b9e5787f06515f6e4d79db27ac6f3ba71c","datavalue":{"value":{"entity-type":"item","numeric-id":22296,"id":"Q22296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$6E0B2460-2EB6-4A26-A02B-237D616D8E8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bc63b18f29e81036c5e8291dd57d82490deaa954","datavalue":{"value":{"entity-type":"item","numeric-id":19233,"id":"Q19233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$AB44DA03-7492-4021-B673-5883A1316A80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c45d553bb9f3e000daa693712f4a182ffdf86459","datavalue":{"value":{"entity-type":"item","numeric-id":13712,"id":"Q13712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$D1147CBF-AB04-4F25-9208-768EBE0AAE87","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1ad44ced1d18419ac00259b4c207dc1fb6655419","datavalue":{"value":"https://isa-afp.org/entries/DiskPaxos.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40950$AF408FB9-EED3-4C86-A9C7-B18EE6D6130D","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a9e6f77602afb01a81648bc91cc5b50fb14095c4","datavalue":{"value":"Mauro Jaskelioff","type":"string"},"datatype":"string"},"type":"statement","id":"Q40950$DB3812CE-993E-4021-AB2F-7E84BBF018CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"cc9e79466e658b1f2029f03a95cc9639795afc16","datavalue":{"value":"Stephan Merz","type":"string"},"datatype":"string"},"type":"statement","id":"Q40950$DA0C8730-11DB-44D7-9FA5-61CFD0ECA91C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1cbcb65cd1bf86868a77fc25a2a41e90b3e436a6","datavalue":{"value":"Disk Paxos is an algorithm for building arbitrary fault-tolerant distributed systems. The specification of Disk Paxos has been proved correct informally and tested using the TLC model checker, but up to now, it has never been fully formally verified. In this work we have formally verified its correctness using the Isabelle theorem prover and the HOL logic system, showing that Isabelle is a practical tool for verifying properties of TLA+ specifications.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40950$78892BBE-F553-4EA3-A4C1-C75AFF4AF3F8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f590cec5fd53fd781b95878fac781f9f8f8fe75","datavalue":{"value":{"entity-type":"item","numeric-id":2766889,"id":"Q2766889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$69C919D2-2478-48E7-8855-78C66F79B322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d37b23b7db99d33ba41b8c893bcac4aca2de8fdd","datavalue":{"value":{"entity-type":"item","numeric-id":4870018,"id":"Q4870018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$A52BCA86-BDE0-4F8E-8F05-BC4E5BC255E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6245a6f9978f36104aee1883c6017c17dc7a8be","datavalue":{"value":{"entity-type":"item","numeric-id":4680191,"id":"Q4680191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$1BA20123-E3DD-4288-B009-EFB046A6DF7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$91780B57-4734-4BC0-BD03-BA071BD970D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8219577a178b5e6bc0cc5aede73996c94784449","datavalue":{"value":{"entity-type":"item","numeric-id":4435474,"id":"Q4435474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$A3D1AD59-6B13-4412-9B62-C2D1A19E1842","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a415faf8a5f610a3108e7fd472916d58928f6763","datavalue":{"value":{"time":"+2005-06-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40950$1355523D-71FA-4C0B-895C-49DDDA3E3695","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"67b60e65eee61d537f5364748ed44dc2d0e05c38","datavalue":{"value":{"text":"Proving the Correctness of Disk Paxos","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40950$42DE111E-F154-40C2-B6F5-52FAF6B86B0C","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":"Q40950$46AD6866-0370-48E5-BB8E-AD0117015970","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"c619aaf4eae47fe7f56126dec3ae88d7d608eebc","datavalue":{"value":{"entity-type":"item","numeric-id":7360775,"id":"Q7360775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40950$10BCB7FB-0CD1-4888-B0A3-CC73FA669E57","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"DiskPaxos","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/DiskPaxos"}}}}}