{"entities":{"Q2177778":{"pageid":2188521,"ns":120,"title":"Item:Q2177778","lastrevid":53725685,"modified":"2026-01-25T15:09:19Z","type":"item","id":"Q2177778","labels":{"en":{"language":"en","value":"Leveraging Horn clause solving for compositional verification of PLC software"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7197643"}},"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":"Q2177778$24F04E4A-82F6-4BE9-A0B4-C429CDB171C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4d7a02fb36f88ed8be50aa51785f34cbe581b1e9","datavalue":{"value":{"text":"Leveraging Horn clause solving for compositional verification of PLC software","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2177778$5BA23D95-BF0C-41E1-9F07-7C2E50D49623","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dbb0094e57a1044e991987718b22401a7f229610","datavalue":{"value":"1435.68190","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$82F97BE8-D3C3-4C0F-BF32-314A9863A97E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e1464a18f9859535a618ef57a0a80621f6c0e108","datavalue":{"value":{"entity-type":"item","numeric-id":2177777,"id":"Q2177777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$FD152501-F1FD-4B86-AFDE-2066A2CD8BDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d00f922b699a93e6b4ff546635f394a57646991","datavalue":{"value":{"entity-type":"item","numeric-id":271718,"id":"Q271718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$A6F8B162-0D0B-4594-88EC-93D3AD509229","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0f7c04b6b94cf13c193d472c226068c28e7c8f04","datavalue":{"value":{"entity-type":"item","numeric-id":169421,"id":"Q169421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$C269C19C-9488-4393-A766-052E33B55A5C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63b133e2f3cdb47e2584c85d3d40bfb2c7f5272d","datavalue":{"value":{"time":"+2020-05-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2177778$E37F2A1B-BC42-4F07-90F9-5BE5548AC3AE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$77CD81AF-262B-4E3E-A38A-95F4FB4DDB3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$CDE5B116-6F7A-4CE9-AACB-446922687CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$2A5F3603-C179-4253-8B89-174AF5146DF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a94d5bf6eab7bddc9c7abbdf41796f52c9b87335","datavalue":{"value":"93C85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$7E9A1559-0165-4B1E-90DB-8E59AF992576","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e2ef9d831eec900be6b60ca0979738b8cd35d1b6","datavalue":{"value":"7197643","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$0373B50E-B70A-4865-B7FE-196062B79678","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$1D88C583-C96B-4344-B16B-C258F0DE8280","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f8a86a4bb6c29e581bd63f5d2a9ec1d11366dcec","datavalue":{"value":"programmable logic controllers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$5F33079C-23FC-49C1-AAEB-8B732E4F56CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$69DD731D-1B96-4579-AC80-2043C3183AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e47d18da5a3cc46f307e12b53d17a8f72c7da71","datavalue":{"value":"constrained Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$097C9249-9320-4C58-98C4-443E9DB84F05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36df8ec051c4d6f6e635b5236064a3c2629928b","datavalue":{"value":"software safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$67FC3466-30A9-49C2-9E33-7B303E42F028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e312494cfe8793918c835553c240d99d06d4bb6","datavalue":{"value":"industry automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2177778$6F2C60FB-8F0F-4570-BC9D-FEBFA57C0F88","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4e1fe9e7e19a9673e889bcce0afc1d800822389","datavalue":{"value":{"entity-type":"item","numeric-id":30365,"id":"Q30365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$C3B6E8B9-3A29-4AB5-B170-A207E2D4AE2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7edebecfea0d1be076050d73b49d0bc3b1453ace","datavalue":{"value":{"entity-type":"item","numeric-id":34655,"id":"Q34655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$974F02F8-35F5-4F83-B4BD-C67A9796F36A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$7D69169B-04D6-4D43-A542-F43042DDCCC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"550af4745ee61c125520a209383c6305679e155b","datavalue":{"value":{"entity-type":"item","numeric-id":35084,"id":"Q35084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$7EEE4142-94F7-46A2-8722-D6180A3E080C","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":"Q2177778$8A62BC27-273B-4077-8363-53278B643406","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b269ddd3fa7e250c621502a9d773b7df342b86f6","datavalue":{"value":"https://doi.org/10.1007/s10626-019-00296-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2177778$1440F7AC-2456-4618-B29F-5A7C906BA94D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b96721eddde6efb2960f24af636253a3c8556bb8","datavalue":{"value":"W2991058933","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$71740DE3-0BF6-4E6C-B45E-5B2F48528135","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"02525d66cda8cc43861270af05678eb88e9d5099","datavalue":{"value":{"entity-type":"item","numeric-id":5015366,"id":"Q5015366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$3EB55BA8-AC28-465F-8257-E11EBDD82E0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad7f4489d4c89d794424e5e3872c38fe58d4c967","datavalue":{"value":{"entity-type":"item","numeric-id":5429342,"id":"Q5429342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$C862654F-E8E3-4218-9F63-2D9123292836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2518ba6a38fa213a00f5ef7c14d9debc5928424c","datavalue":{"value":{"entity-type":"item","numeric-id":2947164,"id":"Q2947164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$D950FB0D-DE1B-4BBC-8044-BB8E40FE8E3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3e6ac22e6ae8e5c865a0d6a18fdb8b499da1672","datavalue":{"value":{"entity-type":"item","numeric-id":3791123,"id":"Q3791123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$253EFBD1-9F63-4AEF-96C6-D16CC4307E07","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":"Q2177778$9962F30C-F5C0-4831-B0FB-6E67CA0B7892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e29a9e63db651327a88d88e2cdc75e51e9cd4afb","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$A300B64F-26E3-4A6D-8F10-6CEAC56EFE43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"007b3bdccae716a59e9fcd68043221be3f0adcfc","datavalue":{"value":{"entity-type":"item","numeric-id":3587259,"id":"Q3587259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$52F4C94E-ACDE-4B3D-B72C-25CBEDEC22C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03f882972e0d4020177d8ec9773323d710a3e89a","datavalue":{"value":{"entity-type":"item","numeric-id":3141897,"id":"Q3141897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2177778$6580D1E6-D9EA-4558-83DA-6E30D434F4B0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c80bb4464903f8bd7f01ef65f0f92ae768323679","datavalue":{"value":"Q126672425","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$3E7354E8-1F98-4D44-8FC4-4511788DA4D3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b6dc3a92c3bfba13c73b14fb40ff5c585e814a86","datavalue":{"value":"10.1007/S10626-019-00296-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2177778$53036482-4975-4617-8AA4-A8F94F5C5DD6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9df7aa313318f9941f46314e3f46d32ff2bc02e","datavalue":{"value":{"entity-type":"item","numeric-id":4782047,"id":"Q4782047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a2801cda324a718e54b09c6a0301eefb1221066","datavalue":{"value":{"amount":"+0.7318843007087708","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":"Q2177778$C9841216-5198-4B5D-BB16-18239959B028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0602b9aefe8e8c4ad61373e1d91e4a6000ce1c84","datavalue":{"value":{"entity-type":"item","numeric-id":2375648,"id":"Q2375648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a11d1b41ba92e4cd0026d4a7d54baab7fc5b96d","datavalue":{"value":{"amount":"+0.7224023342132568","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":"Q2177778$3FF4C393-A68F-4C37-9A53-69047C1F9E2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"789804fee584fea5a77e6f1ed586c9f607bef10a","datavalue":{"value":{"entity-type":"item","numeric-id":3566623,"id":"Q3566623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c02079ab1b84c27976abc0301534f8f1965e851","datavalue":{"value":{"amount":"+0.7203978896141052","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":"Q2177778$5097A538-DE7A-4AC8-843A-A1B42C67CE0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3af34ba53e16c56333af05e0389a263d595eba8","datavalue":{"value":{"entity-type":"item","numeric-id":2827930,"id":"Q2827930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e7846018faa4e163708dff631ba6167cd35f879","datavalue":{"value":{"amount":"+0.7198629975318909","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":"Q2177778$25919683-2CDC-4C4E-AA9C-D04D0E2B149E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bf8a547a05669e0a88913b8edc63e64ac6ef627","datavalue":{"value":{"entity-type":"item","numeric-id":5060076,"id":"Q5060076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"389115fbbc3806c2217e607bc8bbafa24157fbe4","datavalue":{"value":{"amount":"+0.6890075206756592","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":"Q2177778$D8F108BC-CCFC-477A-BFAF-FCDAFAFDB981","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2177778","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2177778"}}}}}