{"entities":{"Q613139":{"pageid":614915,"ns":120,"title":"Item:Q613139","lastrevid":63170175,"modified":"2026-04-11T11:04:31Z","type":"item","id":"Q613139","labels":{"en":{"language":"en","value":"Inter-process buffers in separation logic with rely-guarantee"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5827628"}},"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":"Q613139$14A6DD1F-1720-41FA-BED4-B5BC1C632CF7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c54925b41e2053900a9803cf1a74d480b1f8a287","datavalue":{"value":{"text":"Inter-process buffers in separation logic with rely-guarantee","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q613139$C24DCA07-62D5-412A-84DC-6DD1C87C8104","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"91d5df2eccd9850974eda117511efa3681b8d6cc","datavalue":{"value":"1214.68131","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$4ABD9973-FA7E-452B-A4C9-D7CEE7DCEE52","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3396d8d6c2ec88284e647e78461450d99ea90ad","datavalue":{"value":{"entity-type":"item","numeric-id":469350,"id":"Q469350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$AD06D6C6-1253-4313-B752-AD81EA10477F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32584f5c482e29078ea6b6dcf1d1dfc11c06bcbd","datavalue":{"value":{"entity-type":"item","numeric-id":469351,"id":"Q469351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$5AA87021-BA59-4C51-9013-82B2C8BF2EEF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$CC60958D-0E23-4376-ACC6-D4183B8F11DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6ef5602477723905148f5f25f317bbf3837d9f5a","datavalue":{"value":{"time":"+2010-12-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q613139$2766AA85-AEF9-4B52-BA13-9AB530D0E39C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$F8B93E83-2E0E-4215-B3F7-9B1E0A2C8303","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$31DA4C17-D8A8-44D6-9FBE-EA9528A33ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$DFE62DF9-53E3-405F-AF85-7BFE7A83DAFC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"961aa9ec7a217f4983521b8a26db3f6481672041","datavalue":{"value":"5827628","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$DF06D110-46A0-4691-B478-22F69102684B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q613139$90321341-696E-4DCA-AF56-DEA8754B3503","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b7304181fde15f2ff08bea8b954e64f699bd5523","datavalue":{"value":"rely-guarantee","type":"string"},"datatype":"string"},"type":"statement","id":"Q613139$405E9889-286C-4FB1-99C2-5AAC35A6319E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q613139$14EA4F11-41F6-432F-8C33-43A63E7EC427","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9be3c881819601db6c208fd04cd17cc7030c18ec","datavalue":{"value":{"entity-type":"item","numeric-id":15656,"id":"Q15656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$7F2AAFBA-4C84-44D8-BE98-E706F5C2CB87","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":"Q613139$4238D149-D803-49DF-AFD4-D987207731C0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e5cbd50a8ce04b8306a1282356653c51b23ede5d","datavalue":{"value":"https://doi.org/10.1007/s00165-009-0141-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q613139$5EB287D5-9FC6-4891-BBBA-0976B67C2A36","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2de5bffea473c038a8960144d57bfb0e18ba5921","datavalue":{"value":"W2142118968","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$DCB3EF09-9876-46CA-9809-C59EA6A16CBD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b93a668eb9b37fb891a2cf6f0cf5bd4fa8900df","datavalue":{"value":{"entity-type":"item","numeric-id":3600463,"id":"Q3600463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$7E75E34E-1C23-444B-AAB5-9A81D3AEE1B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91b08ff1b0d4539c99f6902ec8427b7b8b6cea46","datavalue":{"value":{"entity-type":"item","numeric-id":5276151,"id":"Q5276151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$F21129D0-881B-4E47-86CB-E720E8D8EC4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c67625aaf8ba1a48060cec8621d1bfe60db9cb31","datavalue":{"value":{"entity-type":"item","numeric-id":2852352,"id":"Q2852352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$29169FDA-01A9-4767-A9E2-2B7A7963D2ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"288e9539ed7661e715c4eb9511317e6936f53231","datavalue":{"value":{"entity-type":"item","numeric-id":2721096,"id":"Q2721096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$09AC89C7-69DA-429C-935E-7135D35DB18F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c061d31b2ad1070c6417d39eb2aecfa3eccd84ae","datavalue":{"value":{"entity-type":"item","numeric-id":879367,"id":"Q879367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$DB1C5069-6E43-4B6A-A0C5-1A285796D9DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16df2553495bc38f714aaa2197b34e11b69c06ef","datavalue":{"value":{"entity-type":"item","numeric-id":5674963,"id":"Q5674963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$579C42DE-23F0-43DC-B5F3-0B2997C2A6D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a87a3173ec82197606f26c57e1aab02893571e70","datavalue":{"value":{"entity-type":"item","numeric-id":5621092,"id":"Q5621092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$AD7B1CE8-3700-496B-88CF-52A2DD6F004B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cad95b509958b84989ba393a95e7df3a53c21de6","datavalue":{"value":{"entity-type":"item","numeric-id":5255802,"id":"Q5255802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$20F86583-7A2A-4E41-9A70-25FF61C1C845","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":"Q613139$35156403-1489-4C3C-A780-FED04CFB8446","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c2bb38cd4937770f900508ed95421586cdd079e","datavalue":{"value":{"entity-type":"item","numeric-id":4808839,"id":"Q4808839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$D5B66165-8E72-4E97-933C-E6E596E1121F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bb301891097687d39d2b196bcb10dace2f46e9f","datavalue":{"value":{"entity-type":"item","numeric-id":4040791,"id":"Q4040791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$1C829EB9-BB09-481E-A782-59F1B46553D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f2100ba9c9ff3694b0619fc4e400acddec3af70","datavalue":{"value":{"entity-type":"item","numeric-id":3535380,"id":"Q3535380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$26109BDD-E988-42B8-B8CC-01D91BCE243F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3be8c8d124a78b7bc05b7543e4a39424af55fffb","datavalue":{"value":{"entity-type":"item","numeric-id":2486585,"id":"Q2486585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$0A52464D-1C66-4941-A8A6-8CA487A50A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4a9238fc49995a79f8c006683b1a9c42fafe2bd","datavalue":{"value":{"entity-type":"item","numeric-id":4085221,"id":"Q4085221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$23CC73F5-4976-4AB3-B00D-117FCBB60D95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec596191c58c0192912d43559518df53cc026d8f","datavalue":{"value":{"entity-type":"item","numeric-id":879368,"id":"Q879368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$AAB98238-FCB0-4E64-B034-8DCBD1BB8CF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"162bdd4df93f8ffd3483f8a1810ab35d50492908","datavalue":{"value":{"entity-type":"item","numeric-id":4262604,"id":"Q4262604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$98F67062-6302-4418-AFE8-E56CCA6F6928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb5c384f83cfe304bd792549ed6786939a461655","datavalue":{"value":{"entity-type":"item","numeric-id":4783297,"id":"Q4783297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$100C4884-FCA4-435C-B4A7-AC425F282100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc7b71d152d10b52f5614e1cbfe1243b395a5bb4","datavalue":{"value":{"entity-type":"item","numeric-id":3189809,"id":"Q3189809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$E0C21CFE-F633-4802-9980-CDE18BEADBC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa80d2afc7c3a96017ed74644e8193c5d7dedda8","datavalue":{"value":{"entity-type":"item","numeric-id":1764429,"id":"Q1764429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$A39FB334-7DB8-476D-BF6F-14D5C5FB3276","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d34476e0fc3213e918db7c48fd221cd690cd8a79","datavalue":{"value":{"entity-type":"item","numeric-id":3612005,"id":"Q3612005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$AE0C7AD0-15FF-4A1B-AE3B-1D5B26C7D5C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13221a28888c9beff2950e6426d16471a2f129f1","datavalue":{"value":{"entity-type":"item","numeric-id":3525642,"id":"Q3525642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q613139$FBC350E7-E245-4FF9-BB17-EE1FB89C7016","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a9e761e9199909af42f20ee900bdfd56625fc2ca","datavalue":{"value":"Q130880073","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$3CFC3573-71F5-4C42-BB70-CBA1339F5BC3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5b36dcdbdecc999855b08655662c110936c4ddba","datavalue":{"value":"10.1007/S00165-009-0141-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q613139$8C87B93C-F605-45E4-A3E7-F6EB8D9D2C78","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"510daf3b37e3128a58d2c11d92805ae8a9e2c038","datavalue":{"value":{"entity-type":"item","numeric-id":469352,"id":"Q469352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a32d93991e5dab282b64d76598df8d67e3675c38","datavalue":{"value":{"amount":"+0.7806364297866821","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":"Q613139$9E57502C-9546-4DD1-9771-1A3D9A50D2C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"229a3a0eba787aa84df1639600e3c6f3356421eb","datavalue":{"value":{"entity-type":"item","numeric-id":3557673,"id":"Q3557673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a84ec6e66af8ff88dbad68076e09d1ffa991bfb2","datavalue":{"value":{"amount":"+0.7779406905174255","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":"Q613139$14C7E71E-45E2-4EE7-B2CD-DD850BF68E58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71ef30a69ca665d03e843a21e0d767dd5d67a47c","datavalue":{"value":{"entity-type":"item","numeric-id":3525642,"id":"Q3525642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c51a1ad4f0708276e93bfed0065eb7ee86166fed","datavalue":{"value":{"amount":"+0.767869770526886","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":"Q613139$2F26468C-E2C0-4007-9EE8-7FD78F77DD7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ef0991b71712d7a5cc5aa1a32001ce0d64152b3","datavalue":{"value":{"entity-type":"item","numeric-id":3000585,"id":"Q3000585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccefb1734fedcb8e9a613f132a21b4ffab1e0f7b","datavalue":{"value":{"amount":"+0.749401867389679","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":"Q613139$12EFBD16-863B-4F2B-8456-B7D5530882F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"96f72112ae0de9c4ec7fdaff364082f56a8eeb23","datavalue":{"value":{"entity-type":"item","numeric-id":5311481,"id":"Q5311481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bf0cde0d6340e5783cca69e95c6688c3a13c34d","datavalue":{"value":{"amount":"+0.7392950654029846","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":"Q613139$CACC478F-2636-4FC9-979D-4028E17FF682","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Inter-process buffers in separation logic with rely-guarantee","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Inter-process_buffers_in_separation_logic_with_rely-guarantee"}}}}}