{"entities":{"Q2576572":{"pageid":2587315,"ns":120,"title":"Item:Q2576572","lastrevid":48611974,"modified":"2026-01-05T09:29:59Z","type":"item","id":"Q2576572","labels":{"en":{"language":"en","value":"Mechanizing compositional reasoning for concurrent systems: some lessons"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2238116"}},"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":"Q2576572$73D3BB52-97ED-43FF-9F9E-56DC560CF7B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"376d53ff679b6665fdaadc168242f2f60e5ab3c9","datavalue":{"value":{"text":"Mechanizing compositional reasoning for concurrent systems: some lessons","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2576572$28133FE3-2EEB-4179-8F48-EB8FF837562A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c13592cc37b5b383f67c9d2ee1380c1dc3fb1eb5","datavalue":{"value":"1101.68619","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$EC74641F-9B68-4FA5-BA8A-73481EFC2651","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"702a48ef0c3ae4721f33ede803ee875dfb45ba50","datavalue":{"value":{"entity-type":"item","numeric-id":2576571,"id":"Q2576571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2576572$8C777125-5987-4152-8308-913E80C8BFE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2576572$3B5EB30B-22F4-4368-94BB-FF9685F73951","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":"Q2576572$71ACDED5-B67E-402D-99B4-5A7DD8883F6A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"872b3ec3e8824551f65a9a9d299f4b9d6894a9ac","datavalue":{"value":{"time":"+2005-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2576572$6805DF70-D1E0-4959-AB27-9732F2E01CB5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c189c45b466f89dd188bd061df8c45f23f05da60","datavalue":{"value":"68Q32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$D3C52B17-A15A-4A80-A8FE-5DE57DB8FE7B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cd75fa96fe539b0a6a0882cb8205cfae7f48ef20","datavalue":{"value":"2238116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$82783626-F44F-4805-A40C-6284387CF4DA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f89702f81bb443a3353ee5f0794cae6733ae9b5","datavalue":{"value":"UNITY","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$4FBD54F5-9B25-449C-A381-E28872EDB328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$2C8111FB-241D-43A3-AF32-5C3FE31F48F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e783c4686d63dee029aba369ed89a8f33a7e9c21","datavalue":{"value":"Compositional reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$15927604-4E8F-402B-BA06-628537A69A4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab92fc65c908b61a8484a2727180a329a859156f","datavalue":{"value":"Existential properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$B0AE39EB-31F8-46E6-85A2-DF4AB132B762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6da534ad5126cc360ef4afba95eb9ed01867a263","datavalue":{"value":"Universal properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$F2D732E7-A6A1-418F-99BE-972FA2E279FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f458287fd5b7df7236bf25ed0d5c51663a73471","datavalue":{"value":"Guarantees assertions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2576572$F4B8241B-F6A9-4892-A5A4-D097DE1B8049","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"43d68f4a5817b4dbfbf178319d035ad1addabb61","datavalue":{"value":"Q57382658","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$93FAC651-0637-47E3-B2B1-C2A732CF5245","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":"Q2576572$224130C2-48FC-4B7E-B343-C3BAF17B0E59","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5ce5e189ef64622bff10a2dafce2daa88a261cf7","datavalue":{"value":"https://doi.org/10.1007/s00165-004-0053-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q2576572$9F9F3C7A-FC00-4800-A026-F9DBCECD99A0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d2bf2f9d0e8c5b062372cdb55769a7a854a4214f","datavalue":{"value":"W1971790863","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$837577D7-2626-41A3-AFA5-C2FFB4FC7C04","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"98d906bdc1952a408f609cc0abe25491fcffc86b","datavalue":{"value":"journals/fac/EhmetyP05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$7EE95B83-F646-4DF4-B8F0-AE13CBF06378","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e87d4f8606e702516f5621b1e271ddd10d974332","datavalue":{"value":"10.1007/S00165-004-0053-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2576572$41F1F9D0-53C9-4E5C-817B-0CBF803FD018","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"123c98468e5cf1b64592ce854598c12cc291f51d","datavalue":{"value":{"entity-type":"item","numeric-id":5738896,"id":"Q5738896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e6043ea73248b7d3505ed1cc78366cee62dc43e","datavalue":{"value":{"amount":"+0.8009761571884155","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":"Q2576572$6969EB4B-2834-46DD-A406-611F35F57D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f83df204fba48b96d25944b421a5b581e31a5c93","datavalue":{"value":{"entity-type":"item","numeric-id":1391101,"id":"Q1391101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10d5548510a14d807f956e47a420959038f9bf62","datavalue":{"value":{"amount":"+0.7618184685707092","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":"Q2576572$B799512E-F478-441E-8719-37FB3E70AAE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"135f7a0031c0002118754e31fdf0b810129803c3","datavalue":{"value":{"entity-type":"item","numeric-id":5096396,"id":"Q5096396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b3514c04428640b1422c591eee2021f63afdea1","datavalue":{"value":{"amount":"+0.7459145188331604","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":"Q2576572$C210DF93-26B9-49E9-ABE2-D80AB2817681","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3709436caebdb389c9afab90636fadf4b733f94","datavalue":{"value":{"entity-type":"item","numeric-id":3725529,"id":"Q3725529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a1f55f4596356e7b10272e05d6352c33a77d1aa","datavalue":{"value":{"amount":"+0.7395961284637451","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":"Q2576572$D3F109F8-8D2E-4509-931F-B3091B636356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4b0f8fd32fb3675f59dc6402b153e97c16eaee5","datavalue":{"value":{"entity-type":"item","numeric-id":1961924,"id":"Q1961924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04e95609334a5a55196c1edd4f7f88284b21a580","datavalue":{"value":{"amount":"+0.7291965484619141","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":"Q2576572$32BB5D9A-4568-4444-B048-5A598A9100CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2576572","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2576572"}}}}}