{"entities":{"Q7361472":{"pageid":31519955,"ns":120,"title":"Item:Q7361472","lastrevid":105366785,"modified":"2026-10-07T13:36:42Z","type":"item","id":"Q7361472","labels":{"en":{"language":"en","value":"Rely-Guarantee Extensions and Locks"}},"descriptions":{"en":{"language":"en","value":"AFP entry RG_Locks"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2602d7b56900339a6ac6dbd531bc566092643a1b","datavalue":{"value":"https://isa-afp.org/entries/RG_Locks.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361472$F1668715-E362-4ECF-8540-8A64E312D982","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f974a567496d997696a7f7f0ff44cd54be3aa7c","datavalue":{"value":{"time":"+2025-11-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361472$331C7FA7-490C-444D-8E71-196324A0C3D8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"b319d18a35bbe3197e764f80bbd36b571a96722b","datavalue":{"value":"Robert J. Colvin","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361472$AB1CB195-9FE2-41F0-B0B9-504EEE3F31A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"cdd4977e2a46b945f25281ad840831b5b51605ff","datavalue":{"value":"Scott Heiner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361472$0EE28C51-6F52-4BB9-AF42-5DE140C0E2BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"764f505c166c35794d03c474c0f8d7e266076240","datavalue":{"value":"Peter H\u00f6fner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361472$2D7F8626-A087-4D89-A90F-AAAEEEA01907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c6df8eef86868568e1b8a62b62ce767d5c00230e","datavalue":{"value":"Roger C. Su","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361472$4D3149FB-DEC1-45E7-881D-91C5E01D97A2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ea1051d321cfccc270815f6258b0751a4001c5d4","datavalue":{"value":{"text":"Rely-Guarantee Extensions and Locks","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361472$D6E6781A-8E5B-4670-A0A4-8738C837FA61","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a525dc7e948e7bfca5366a1231265be954858cf9","datavalue":{"value":"We enhance rely-guarantee verification in Isabelle/HOL by extending the 2003 built-in library with flexible syntax, data-invariant support, and new tactics. We demonstrate our enhanced library by applying it to the examples attached to the original library. We also apply our library to three queue locks: the Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361472$4E3710B9-C7BE-4EB1-995C-8194D17EBFA4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e7f7a002bf1488e9eda8c9de5c95b2763f569ef","datavalue":{"value":{"entity-type":"item","numeric-id":4417904,"id":"Q4417904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361472$8E9DE33D-E734-4C0C-A538-74FD86DD0CC5","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":"Q7361472$87E38E1F-5993-4205-B914-391933E5BEA4","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"d4e45a44d8cb21e0bc3c4e18fb1edc38a1545452","datavalue":{"value":{"entity-type":"item","numeric-id":7360785,"id":"Q7360785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361472$4BA1D097-DFAF-4311-BF47-B3ECDFADD453","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"67f9152ae39999cbb9c1eb53eaa258495b5f6fca","datavalue":{"value":{"entity-type":"item","numeric-id":7360774,"id":"Q7360774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361472$6D0F5241-92B0-4C6D-BDD8-57824D7CE594","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":"Q7361472$5E56DEE1-841F-47B7-A947-6BB5D04484FE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Rely-Guarantee Extensions and Locks","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Rely-Guarantee_Extensions_and_Locks"}}}}}