{"entities":{"Q1648035":{"pageid":1658776,"ns":120,"title":"Item:Q1648035","lastrevid":72946590,"modified":"2026-04-14T08:56:31Z","type":"item","id":"Q1648035","labels":{"en":{"language":"en","value":"A perspective on specifying and verifying concurrent modules"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6895011"}},"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":"Q1648035$0370D26D-B91F-4556-AB29-C88D35AFB425","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d0c550da3290baca9ec3541ed6462bf3bbd882c2","datavalue":{"value":{"text":"A perspective on specifying and verifying concurrent modules","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1648035$9AE5D39B-4917-4E88-8B3E-1C89D6B8B8D9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c562fefebcd068601500aa79c4f6681c0b8fcc87","datavalue":{"value":"1395.68187","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$5F16B719-71B3-4579-BD5F-911413E33460","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"478b1cc077659b300d5df2d6d7ad6015aac688d4","datavalue":{"value":{"entity-type":"item","numeric-id":964498,"id":"Q964498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$DCD9D37F-24D8-4F7B-8A9F-3257D315D8BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5aecfa24efe1d6531448974404886b2e3311e4c","datavalue":{"value":{"entity-type":"item","numeric-id":1648034,"id":"Q1648034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$48367DB6-016A-49E3-B951-8CD500667BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9a0eb51f415e5d6830c006f29bf0f051478fa880","datavalue":{"value":{"entity-type":"item","numeric-id":283752,"id":"Q283752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$340D6F2B-3F03-4771-AFD2-357DC48CE9A8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$01DD4E1C-0FCA-49E9-BCE3-B19DF056E182","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c8a780e74b0fc20f5c27aee56d09c8997e1b03d9","datavalue":{"value":{"time":"+2018-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1648035$E12275E9-EADD-4463-9513-CBBF23C6D6FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$AF1FE522-FBFC-4B4A-A528-0E3F57E71946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$C9C312D9-E4D5-4A44-9FF3-A3FA6A017534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$CCFEBAF5-2F5C-40A9-A9DB-E0AB45F43D30","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c0708ec034bc5b11afb3859a4dd2c77918b60fa3","datavalue":{"value":"6895011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$A5CDA118-5437-46A0-B048-2A5D60F809E5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1648035$EDC4960F-1E40-4BC5-A271-72354BC04AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1648035$8CD5FB23-94E8-43C9-B596-36559D1EE4BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1648035$8B83967F-ACBA-4CF2-9ADF-F0B63775F297","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb4ac1b3e6590933f07db2ef44e8e77f8844e4b4","datavalue":{"value":{"entity-type":"item","numeric-id":19271,"id":"Q19271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$C0F23696-EB68-46C7-916F-6D4795AABB78","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":"Q1648035$6E68A283-895F-41DD-8887-41D9CAF2B9EA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"512e10eaf9fbc14a906fc4f3c3e7ec91665eaf18","datavalue":{"value":"https://doi.org/10.1016/j.jlamp.2018.03.003","type":"string"},"datatype":"url"},"type":"statement","id":"Q1648035$6FF21587-00DE-4ACE-8499-AC205B842F06","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4d10d87349f5a96889b777b1c5240813453d17cf","datavalue":{"value":"W2796428443","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$92006A87-96FD-4C79-84E9-72E5101F3BE0","rank":"normal"}],"P223":[{"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":"Q1648035$D781DEE1-07BC-41B5-8456-3686E87F8D69","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":"Q1648035$59F3AFFD-ECD3-41B5-94B7-C21D66B26984","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e1620bc79adffbb9b0f00ce2b11a84d197fdf55","datavalue":{"value":{"entity-type":"item","numeric-id":2819854,"id":"Q2819854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$F7406EB9-F919-40F9-8FFA-48061D8137F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90600d640bf241ff0996bc9c4593429acd22ef8f","datavalue":{"value":{"entity-type":"item","numeric-id":5410705,"id":"Q5410705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$7F28B3E3-ED15-4FEC-AE9C-F51692F3212E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbae59cabb692e5aadee25ba2669315a1892bf3e","datavalue":{"value":{"entity-type":"item","numeric-id":2802440,"id":"Q2802440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$4ECE23C4-8441-487F-8C94-70B61DF8A1EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88107773061b55a684a37ff2030cb91e127bb568","datavalue":{"value":{"entity-type":"item","numeric-id":5408549,"id":"Q5408549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$F5D69BFE-E205-4470-9556-0A611797A6A1","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":"Q1648035$072D29AB-BB3C-4E39-8234-5F5F4926CF9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac23d65a9afeff852c7bda4556ad42907e525e44","datavalue":{"value":{"entity-type":"item","numeric-id":5178870,"id":"Q5178870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$A09036B4-D39F-4F17-9358-6E67321E2898","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":"Q1648035$E7CCDB73-40F9-4B2E-A409-C499B9688EA4","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":"Q1648035$793DEAE1-3EE4-4EDE-882E-97680B08390A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b2889d04761e06240c487cc63b75905e4a3cf42","datavalue":{"value":{"entity-type":"item","numeric-id":5261529,"id":"Q5261529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$C62F91F1-DD59-4B03-B2C4-C2CD5608742D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"408dd153356546cf4f54bb5174901182b587cfa6","datavalue":{"value":{"entity-type":"item","numeric-id":3617714,"id":"Q3617714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$0BA65BD1-C684-4658-A766-9322A960D88B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b6f86e69e4182fe9dee7c3758ceccac77217422","datavalue":{"value":{"entity-type":"item","numeric-id":4813391,"id":"Q4813391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$59B21B1B-35A4-4C20-B281-A1528E4E7849","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":"Q1648035$4C0732B0-ABF5-4185-8305-79956862CC83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2934261f50a1e0b490a2bf100b0d26006aa930a","datavalue":{"value":{"entity-type":"item","numeric-id":2931839,"id":"Q2931839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$6579388D-2C5D-42D9-B82E-CE5251050C44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"928940c82f5eab2df5a1704d32409a802ad3f2f0","datavalue":{"value":{"entity-type":"item","numeric-id":5244818,"id":"Q5244818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$B7FC9CB7-6D96-4603-9789-567FD672B573","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9dc6362ae6c42ca2e8e1880257b6d86ff0e45ca7","datavalue":{"value":{"entity-type":"item","numeric-id":5326285,"id":"Q5326285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$BD76DDDA-4FDB-4F8C-8F42-A771988E3FCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad9d568636dc034cf5bea0b01c0319383e3edc3a","datavalue":{"value":{"entity-type":"item","numeric-id":5410698,"id":"Q5410698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$20294E9C-04B9-4505-945E-7108C35A731A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4f3cf5cc8414064d2f13139103d36becc2b2b32","datavalue":{"value":{"entity-type":"item","numeric-id":3617704,"id":"Q3617704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$453A1990-6147-4050-A2BC-AB5CCBE6AB8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"127db5097e77e5b4edc8afc4e762efcd27117ed4","datavalue":{"value":{"entity-type":"item","numeric-id":2931804,"id":"Q2931804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$86857FCE-F33E-4385-856F-FFCBD987059D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1d89278057f829a68cd8215a1e83a3013e2243e","datavalue":{"value":{"entity-type":"item","numeric-id":5276150,"id":"Q5276150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$F909F6E9-3C11-4A34-B790-5105A9B12FB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fb33ef9ac4826d45084ea1d994a748baa58950f","datavalue":{"value":{"entity-type":"item","numeric-id":5891776,"id":"Q5891776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$1361203E-BE9A-4482-9A05-2BA454262196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d36cd773aabf189aeee9f5a8e88141bd0e8f83b","datavalue":{"value":{"entity-type":"item","numeric-id":2802477,"id":"Q2802477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$BB21149D-FAE9-443F-B56B-CE53921E37B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fa3e0baccd13a31decdefff78dab1089382403","datavalue":{"value":{"entity-type":"item","numeric-id":2988651,"id":"Q2988651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$A0953FFC-7AA9-4D05-A108-A399992A3E79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b4f5a22d9f04e362b8ec930a158e9412e528ccf3","datavalue":{"value":{"entity-type":"item","numeric-id":2802462,"id":"Q2802462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1648035$718EAAB5-602D-4897-9CC8-F44F6FE6AF27","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8ccc373b3a076c283d09fb1fdd9dbd64a56e41ed","datavalue":{"value":"10.1016/J.JLAMP.2018.03.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1648035$E39AA3DC-BDCC-49A5-B92C-E8420C6F123F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c3edb0e35abe551cd1ba974c3d36227362e9c22","datavalue":{"value":{"entity-type":"item","numeric-id":5971389,"id":"Q5971389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"908dad2ee2c32429ae1a74a1d0a06c85139a5877","datavalue":{"value":{"amount":"+0.902705192565918","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":"Q1648035$7EE36628-CCA5-4BD7-92A4-B945A135EA0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1ade388e4c29688b4c5548a6eb0a9dca301572a","datavalue":{"value":{"entity-type":"item","numeric-id":6162114,"id":"Q6162114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28333494a58cbbee94c3b28734356711a9b16f74","datavalue":{"value":{"amount":"+0.7728796601295471","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":"Q1648035$124F1D42-1A75-4F44-824A-DDB5FD928B57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dc9b0d04ab3450cb241ffa1da532485b511cc58","datavalue":{"value":{"entity-type":"item","numeric-id":5326285,"id":"Q5326285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56dd88f0d0b2995ad30ecea6a7e8b5d76ce65d97","datavalue":{"value":{"amount":"+0.763820469379425","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":"Q1648035$269862F1-9CF2-4D6D-992D-F14A08F0BBFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb906b7819af3215c442ea0a6017f05602f2584e","datavalue":{"value":{"entity-type":"item","numeric-id":2351261,"id":"Q2351261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60ea973ecca0826ee9537d0dc1abfa37b6edb202","datavalue":{"value":{"amount":"+0.758051335811615","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":"Q1648035$240D2C0C-F92C-448C-A35C-BCD13E0F2008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c928ffddde892e1817bc819ab21baaf4913e314f","datavalue":{"value":{"entity-type":"item","numeric-id":3189809,"id":"Q3189809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4dff97cedd219cb8a117a9c8ca11e6e1e7ac480a","datavalue":{"value":{"amount":"+0.7544037699699402","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":"Q1648035$5449A4D4-A5E7-466F-A7C3-47AF48C4D1B1","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":"Q1648035$48941CB1-E95E-4158-80F9-399AEE3E2812","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A perspective on specifying and verifying concurrent modules","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_perspective_on_specifying_and_verifying_concurrent_modules"}}}}}