{"entities":{"Q6847672":{"pageid":20582704,"ns":120,"title":"Item:Q6847672","lastrevid":84275906,"modified":"2026-05-14T13:05:30Z","type":"item","id":"Q6847672","labels":{"en":{"language":"en","value":"DM-check: verifying invariants of concurrent systems by deductive model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8169619"}},"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":"Q6847672$98BD48AB-5329-411C-B529-A7CF0795F872","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd901de2869e186bb6182f90cc7d5dc05e25b88b","datavalue":{"value":{"text":"DM-check: verifying invariants of concurrent systems by deductive model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6847672$819F9D90-A992-43EC-87C5-6816BB12D2C2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c712a26488a1f755facfe3ae874535257d57b38a","datavalue":{"value":"10.1016/J.JLAMP.2025.101107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6847672$760F4279-7C00-488E-BBEC-9C52B75FE863","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7abae01514d1760eb4f9d93836437ad171626b69","datavalue":{"value":{"entity-type":"item","numeric-id":1951604,"id":"Q1951604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$37534BDB-B69F-45C0-857E-185D38BE08F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5805f02852c8c5214c4739c3a07407316889a81f","datavalue":{"value":{"entity-type":"item","numeric-id":462490,"id":"Q462490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$7DAD31FD-DA9B-47F6-921E-C30903DF136F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b07a4e61b62ce54995b2f0e708397c1238b9d5e2","datavalue":{"value":{"entity-type":"item","numeric-id":6052947,"id":"Q6052947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$9FB92FD8-650C-474F-A671-FF42DE0A0B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"db32c21cc482660e99c90b1907d7d5760cbfacfe","datavalue":{"value":{"entity-type":"item","numeric-id":347381,"id":"Q347381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$1C7237C2-0A6D-4271-83AB-1DD81781D38B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6d326dde040720157c585183b6d2e8a202bb550f","datavalue":{"value":{"entity-type":"item","numeric-id":739629,"id":"Q739629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$2AEEADF7-F7CA-43C3-BC79-0FF5540881C0","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":"Q6847672$93FF77DA-A463-431C-ABF6-E8EAE86F7873","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"665884feed858a78717dfed3ddfae506708060db","datavalue":{"value":{"time":"+2026-03-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6847672$EFBF2F9B-549E-4469-890D-54601346BA91","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6847672$FF8D6935-B9BB-4D09-98A8-D291852A4602","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cc238e5436334db9245c245b98410db2e60d047c","datavalue":{"value":"8169619","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6847672$F7815087-95BF-4DE4-A18E-F846345624CD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"302e7bd67d2646d1e0615c1195ca61ad56775360","datavalue":{"value":"rewriting logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6847672$16150367-9D97-4EA8-8863-7E89A699400E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q6847672$43E7301E-0F83-45BE-AF7B-B7479E7E5CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa6792ab787021778f5f20cba1d78917f3fc46dd","datavalue":{"value":"inductive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6847672$A95C9E97-25DC-421F-A2F8-9A932FD93200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e4de46a0d3893db2cc6abcfda48dd51644993b19","datavalue":{"value":"constrained patterns","type":"string"},"datatype":"string"},"type":"statement","id":"Q6847672$AA254744-B520-4788-939A-0420B61930F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09ca32413f1d623ef3eb8d4a14ac759e926ea85f","datavalue":{"value":"invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6847672$DE3E9A82-C9B4-40C2-A740-9982C912422D","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":"Q6847672$7FE560FB-F681-4091-9D99-2B55281FF820","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"031d93ba0f0d59696b935bd9707e0c0dc3b5aa4f","datavalue":{"value":{"entity-type":"item","numeric-id":4050191,"id":"Q4050191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$39BBD837-4E0A-4A30-A96F-3CCE36059F6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14a1a742e214d8245c75cee91c994ccfb70891f3","datavalue":{"value":{"entity-type":"item","numeric-id":880981,"id":"Q880981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$7A571F10-FBEF-4FE3-B56C-1D1E5F72BEE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c264d0378a5f30df399a3e5c6ab315df59ddacaa","datavalue":{"value":{"entity-type":"item","numeric-id":1190488,"id":"Q1190488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$D7F41898-669A-46E4-9494-E9A4EF701B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c884171bba72c2b3f8a55330fd6748a3e548c6f","datavalue":{"value":{"entity-type":"item","numeric-id":5432339,"id":"Q5432339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$030C776D-CF3B-4B3E-B2C7-BC202411DA64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00e7fb512c3c2088a0e31db09a35588d6ca50ae7","datavalue":{"value":{"entity-type":"item","numeric-id":2958376,"id":"Q2958376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$B53518A6-7A82-4B25-8D09-9E779567DB20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2613520dd94bccb06517a96e46dc00cc2cb71a4d","datavalue":{"value":{"entity-type":"item","numeric-id":3184784,"id":"Q3184784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$9C12F163-00C1-42D6-AD4D-99B0DE99D687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9347765136650ae068c681dd50837d0a09bc96f4","datavalue":{"value":{"entity-type":"item","numeric-id":2291818,"id":"Q2291818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$DE399123-2E71-4A62-A902-38AD9D426368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cde07a5af9c9126c9edeee597823bae300bf25b6","datavalue":{"value":{"entity-type":"item","numeric-id":1931909,"id":"Q1931909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$048EC915-4933-4706-9FF8-C7A7A4C6602A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89ce0f860d09058e603a5b1cbf016972766fc0ef","datavalue":{"value":{"entity-type":"item","numeric-id":2291817,"id":"Q2291817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$0BA13CC9-6E24-43E7-9CB7-823AAADAE8A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35de7df0c420175ccefc3da8012590103dbdf602","datavalue":{"value":{"entity-type":"item","numeric-id":3839051,"id":"Q3839051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$23B22F55-958E-439A-9D33-CBBE676E901C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3239d3bc022112b37f4da6991a3c7bf09667ee35","datavalue":{"value":{"entity-type":"item","numeric-id":1196302,"id":"Q1196302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$996CFB40-DB7B-48E1-8517-260F8064F66D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e0c1063d2d24fe1956813fa9bc95f21d14d9d1e","datavalue":{"value":{"entity-type":"item","numeric-id":730473,"id":"Q730473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$F11DB1CA-2A77-49A9-B0AB-E586F39FF953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01d4a91dcf05e247efe3d36d8b1cf5c4792f88","datavalue":{"value":{"entity-type":"item","numeric-id":4385532,"id":"Q4385532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$73558829-0B3A-4C54-815F-0888199504E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4503ba4114e24ed9a5c364813a9872b5b85bf46d","datavalue":{"value":{"entity-type":"item","numeric-id":347382,"id":"Q347382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$5B32E71E-51F9-4CFF-9B37-9305266D9CB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69bd394a77de6a66e7c3ead14354e268bd49cc00","datavalue":{"value":{"entity-type":"item","numeric-id":997833,"id":"Q997833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$B7DBFAB7-8F4C-48E9-BE31-76F9A67A5C17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4eb176e33191c1bdb10e72d085b171a598ebbffc","datavalue":{"value":{"entity-type":"item","numeric-id":7009392,"id":"Q7009392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$EF911632-1588-4CD2-A33A-2B095F182012","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7585a3414ed5d460ebd13d62b6e4dd63859751d","datavalue":{"value":{"entity-type":"item","numeric-id":2811360,"id":"Q2811360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$569CC231-3946-4F71-A96B-54E98F66CB0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0575fb0f9e8dcd74b50e1e98d2b39b91e52d8a90","datavalue":{"value":{"entity-type":"item","numeric-id":5403085,"id":"Q5403085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$2800D888-0E2D-4A1B-A3BD-BA97953D2091","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59cb51f6693b3dc79e9cbaae1f269d0e937851b5","datavalue":{"value":{"entity-type":"item","numeric-id":5170808,"id":"Q5170808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$0EB666E1-4AE7-4652-BA62-2151F2DDDFD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55474ef7b09a7d9ac924269c7b98f7c00174578b","datavalue":{"value":{"entity-type":"item","numeric-id":3090877,"id":"Q3090877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$27D8A73B-314E-45DD-AFA0-42A5771963BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad8ae5b8a023162693faa8fd065c4838972a71dd","datavalue":{"value":{"entity-type":"item","numeric-id":5403086,"id":"Q5403086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$C3C5C51A-C21E-4EF2-A76D-18E383AA4B61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ee29e8a506c504ab9034445431f767c21cf2916","datavalue":{"value":{"entity-type":"item","numeric-id":5902548,"id":"Q5902548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$750546A9-8089-4405-BA92-FB88FEC601CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86415c654a903509b73bb5d92c7a2bf96bc67567","datavalue":{"value":{"entity-type":"item","numeric-id":2104541,"id":"Q2104541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$A16BA99C-70C7-4AC4-B0BA-21763572CC6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b2a325f2821aad8753d3ce236c86a4b2aaffc82","datavalue":{"value":{"entity-type":"item","numeric-id":2945133,"id":"Q2945133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$D4831BE3-6726-47C1-8B58-FE7B98920D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"674b20c3236b9fe5338c929f7f2bef21f80418e6","datavalue":{"value":{"entity-type":"item","numeric-id":6643468,"id":"Q6643468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$4B9891A1-1E0B-4E41-AB9E-3C6EDD7619FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64955960b6b306cddce35bef2716491e75c84c49","datavalue":{"value":{"entity-type":"item","numeric-id":6914455,"id":"Q6914455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6847672$E690AA91-E686-4446-8B40-3E2158A9AD9A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"DM-check: verifying invariants of concurrent systems by deductive model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/DM-check:_verifying_invariants_of_concurrent_systems_by_deductive_model_checking"}}}}}