{"entities":{"Q832723":{"pageid":834571,"ns":120,"title":"Item:Q832723","lastrevid":77681756,"modified":"2026-05-06T09:49:39Z","type":"item","id":"Q832723","labels":{"en":{"language":"en","value":"Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7498610"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$59FFAFD7-E367-4E19-A9CF-A7E8CC4D1BF2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"77f0a65f62aee73e577e820e7ee6230adc38928f","datavalue":{"value":{"text":"Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q832723$D62ADE3B-8543-4CA5-AF89-98316D5D4B51","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"628ca06949720b4fe3c151916560ebce65d741fc","datavalue":{"value":{"entity-type":"item","numeric-id":832722,"id":"Q832722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$8106B743-A0EE-496F-9D9C-8CC2F6ADA845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07c694df1fbeaa11f2d143be3a0f488131a3d130","datavalue":{"value":{"entity-type":"item","numeric-id":736792,"id":"Q736792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$3C5598E4-6E1C-472A-B4BF-2F8644EF7B52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32e53015970cac840f13624d12043d566c18d3f2","datavalue":{"value":{"entity-type":"item","numeric-id":470036,"id":"Q470036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$EFAEF223-544C-429C-8853-4DE3AFB2354C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ec377ce736b6c6e493e8394b5df9bdb00d5fb01","datavalue":{"value":{"entity-type":"item","numeric-id":436355,"id":"Q436355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$78C723B6-ECCB-4BEA-8552-454B97AA05D6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$E19CA9B5-2F82-449E-B62D-11724DC11C82","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"26426ab4d5a6ecfa201abc41ba9257e3996155a5","datavalue":{"value":{"time":"+2022-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q832723$B7E31C1F-F0FD-464E-8427-DDF2B7AAFB66","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"44afc62a67e851b1b948936e6a3f4dc05a296eb9","datavalue":{"value":"https://arxiv.org/abs/2004.02983","type":"string"},"datatype":"url"},"type":"statement","id":"Q832723$6C13BB33-EA21-43DC-84F5-9D9BA6038418","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832723$79796073-AE1B-4F1E-836C-86B5FF19A8A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832723$3F56E8B7-D86B-4D63-9440-D80AA1F7616F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"86241d19718ba6c910e8a3829b8d4dd6cfaf1035","datavalue":{"value":"7498610","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832723$5EB577B4-4061-40DB-854E-D388396DF78B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8f0aa4f7918f95edae5d22bab2d2bca19acc0faf","datavalue":{"value":"C11","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$CF5ED243-3C5D-446E-A72A-262AA40A701A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$839656DA-1B48-4BF3-BB33-334EC8FD2D0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7aaaf7bd659464062f402485e03b48584e585d65","datavalue":{"value":"Owicki-Gries","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$079C2C5C-0799-48CB-9089-57A2FF8B1E16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$9E30DEED-C8D2-404F-BB0D-4C904472DB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d49a0a3cfdf1415249a7c3e075d149a96b70434b","datavalue":{"value":"weak memory","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$14316ECF-1B77-45E7-8633-62748C0AA1C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q832723$9C771E9C-0E44-4147-A56E-A89635279A03","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$B998D799-1EDE-42EB-AB8D-876CC504737C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53a4a9b6c38d395d5b2eb80cedc3eefcbf3e9947","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$672C6D11-97C8-45FB-AEB9-194F085D61F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b9afd1e8fc349d198c89a22f85926ff81edbd463","datavalue":{"value":{"entity-type":"item","numeric-id":26932,"id":"Q26932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$4AEF263A-497C-460B-8AAA-5D6C1E60CC40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$6D9991F8-C4B8-4CCD-B10C-FE3ECFCC4A94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$E17FA0C6-C2A3-4E7B-9DC6-AC09040EA9E2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$F5B00EDA-4153-4EDE-929A-DDD4FF1F4AE6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"740eed487a75b16e0afda41021ec5c22a18c4386","datavalue":{"value":"W3214317778","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832723$0916A003-1F95-4E6A-905E-9477BB847FA1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bfcdc3f39b30ddbcf72bddf86d2beca129b3fdf0","datavalue":{"value":{"entity-type":"item","numeric-id":1683934,"id":"Q1683934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$8438939F-6CD3-4965-B2CA-10335763010F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54b2024aa8d54e27f7fccd5324cb75636425f072","datavalue":{"value":{"entity-type":"item","numeric-id":5370841,"id":"Q5370841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$DC78E398-28E9-415C-B61A-4B1E433CC3DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1278f450e92c60aefd3ce7b062893c4212f063b7","datavalue":{"value":{"entity-type":"item","numeric-id":5326305,"id":"Q5326305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$65D649EC-D894-4426-9236-9D1DB192DDAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"989ffcc992d1ac31e39a63758614d7ce6f35323e","datavalue":{"value":{"entity-type":"item","numeric-id":837527,"id":"Q837527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$AF9451B8-5747-4A3C-A6DC-95C0189B6479","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3b91bb151cd8a64e803b2a1e144870181c46cb5","datavalue":{"value":{"entity-type":"item","numeric-id":5408531,"id":"Q5408531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$3ADCA0AC-C65D-40C0-ABC2-904BCA857100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$D3E7753E-7984-4208-9BD5-52DA0185C751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de928295b18ffce2a5aa2ac27ac1d6497faa848b","datavalue":{"value":{"entity-type":"item","numeric-id":681346,"id":"Q681346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$050A5059-B935-4852-92DD-5D23FE682B29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e4059e3e3788a873388fc3b6237dcbc3b49d09","datavalue":{"value":{"entity-type":"item","numeric-id":2768503,"id":"Q2768503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$20A7019E-86CA-4546-811D-2F89E273C238","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e55fbaa7b570af31cfa5d8e16c655c1bc869851e","datavalue":{"value":{"entity-type":"item","numeric-id":2796064,"id":"Q2796064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$029D9F79-46E0-476C-85A2-BB7D8E5A5E1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1182097fb44d1361e09ae16f758d339b08a5ce4","datavalue":{"value":{"entity-type":"item","numeric-id":2988652,"id":"Q2988652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$E8E1F113-82AB-439E-A827-1C9BA07A46B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$1A5EE3F8-2DC8-468E-91E8-3B8B314C1602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06e24dfcf208ad7ddc97aa163494313cd9959a87","datavalue":{"value":{"entity-type":"item","numeric-id":5370854,"id":"Q5370854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$1CE095C7-8140-462F-9B32-D77D7B2A602D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2da1cc5a574b49803eb1701499baba77e3e9ea7f","datavalue":{"value":{"entity-type":"item","numeric-id":3449485,"id":"Q3449485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$002A0B39-E63C-4A81-8644-671644A66A88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"066eb8cdc8433f36244b58d272d4a6e6c9cc7f21","datavalue":{"value":{"entity-type":"item","numeric-id":3853114,"id":"Q3853114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$6F5108E5-268E-45EA-BBF3-91E264EA82C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3422aaa623eb5f87aeca9f244e6f007c7eb8ce2c","datavalue":{"value":{"entity-type":"item","numeric-id":2796035,"id":"Q2796035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$8AE7E9A7-5B1B-47DE-A26B-8ECAD686A88E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"796364eeefb9789a01eab3a144d0337d6c23ee01","datavalue":{"value":{"entity-type":"item","numeric-id":1219675,"id":"Q1219675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$2A036009-7681-482D-AE2B-50480D90B303","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$0C736475-30FD-4ED5-B34C-8CA0A42F34C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"758f34ad23e2758a87a12540215d5aa42e2ea7cd","datavalue":{"value":{"entity-type":"item","numeric-id":5041113,"id":"Q5041113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$C5E5E68A-8F57-4717-9A6F-164CDD9B6ADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adbe506beada9bb0831e3665fa451027cf6697b0","datavalue":{"value":{"entity-type":"item","numeric-id":2324213,"id":"Q2324213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$F0E47AD4-6CF8-4495-9DF6-B513F1648868","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aded3f9c41f40827cb7b1b61c5c29bdb1bd7f42","datavalue":{"value":{"entity-type":"item","numeric-id":2323985,"id":"Q2323985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$A05EF770-6026-4DF0-A794-D678E36061AA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a6a0e67824f22d7546420a050ec4bf3df0ccb74b","datavalue":{"value":"10.1007/S10817-021-09610-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832723$BD3EAFDB-CA2A-43DF-89D5-49FC78BC9B0D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a9dbad85b24d9a28aa30ad6051b001874f74ff","datavalue":{"value":{"entity-type":"item","numeric-id":2324213,"id":"Q2324213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6f2e6119b19b71a3fb566ce6192f7b8e8bc7a92","datavalue":{"value":{"amount":"+0.8499100804328918","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q832723$3E570D26-671B-4A21-A545-E80A79528D08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67303c82678628ecfc3c2251f31c6a2e5a9b0753","datavalue":{"value":{"entity-type":"item","numeric-id":3449485,"id":"Q3449485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56cec2ed4d88235d975e728c45746f41623cae7b","datavalue":{"value":{"amount":"+0.8221163153648376","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q832723$8FAED8A2-8012-4EFF-A80D-2A428C47DA1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47d35681e391fdf56041687e513bd455b5a835f5","datavalue":{"value":{"entity-type":"item","numeric-id":5056374,"id":"Q5056374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1713581fb6e8578397da3fa44bb23b0e0be642ac","datavalue":{"value":{"amount":"+0.8192722797393799","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q832723$A66F173A-50AE-42FA-985A-F564D027DC5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51aaa25ebb07ee12b83c51af98b12f5d8616b46f","datavalue":{"value":{"entity-type":"item","numeric-id":2151230,"id":"Q2151230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f020c3763321fd1fa6f62d45c2c063c33edefa30","datavalue":{"value":{"amount":"+0.81337571144104","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q832723$7C435718-8DAA-4D48-A707-E4DB5EED8B4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2329ac48b709f66aa4e2a0cfdaaaf3d4cea285dd","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89167d034b6bfa09b4ac0cb07d6ed1d2fce06560","datavalue":{"value":{"amount":"+0.7534975409507751","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q832723$5BE0AAC5-F1CA-4C38-8215-A72F6E608104","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832723$104BE5EE-C73F-4D07-8386-6088C7197073","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Integrating_Owicki-Gries_for_C11-style_memory_models_into_Isabelle/HOL"}}}}}