{"entities":{"Q2147702":{"pageid":2158445,"ns":120,"title":"Item:Q2147702","lastrevid":54345224,"modified":"2026-01-26T16:28:38Z","type":"item","id":"Q2147702","labels":{"en":{"language":"en","value":"Abstraction and subsumption in modular verification of C programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7544948"}},"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":"Q2147702$BB742402-EB27-429B-A963-7E34871336DA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a9ca5cea01506a35028edcc39a85a97969d47d4e","datavalue":{"value":{"text":"Abstraction and subsumption in modular verification of C programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2147702$8BE14F8C-699C-43B9-9BBE-D4EA404AD1B9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7faf79303668ed9fa6d8434c426ea6e6661c949d","datavalue":{"value":"1505.68023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$669AF66A-73F2-42F5-950A-52BEC7992947","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbc276cb0285ab91fe37913260a1294cd4b610f4","datavalue":{"value":{"entity-type":"item","numeric-id":710671,"id":"Q710671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$4DF0210C-64A1-49DB-A966-BDB68517FCB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc26ae99955b17096664472ad434caf6f770734f","datavalue":{"value":{"entity-type":"item","numeric-id":1663237,"id":"Q1663237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$B3767469-8775-449E-8CA6-F6CEA1E1EF9C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$190014D0-199A-4BBC-A222-0478CCEC9FA6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"95e580f4051f5bb4afafd11f30b01e18c9a41ef8","datavalue":{"value":{"time":"+2022-06-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2147702$05AF4199-7C1A-4D17-8152-0677E60A6322","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$8AD871C5-02E5-4CB6-A2AA-5171B2ABF621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$4538B621-07B5-45A9-AF9D-F519A2BA6295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$FECBEA29-12AC-45F8-9206-94768FF7AD37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$C423C0BD-9C9F-4D46-9E56-9E9B16FB884F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a1bcbffa0bb713723ec3a847d8ac4410abf8a163","datavalue":{"value":"7544948","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$F5CDE7C0-E5C5-487A-892A-B8EC7DBE13CD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f63e28e1d4b6fc67ff50ec99e06aa3ad3ad82c7d","datavalue":{"value":"foundational program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2147702$9CBB7C67-853A-4B3F-B401-1737163714A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13ebea0abebf79df4c894ff86295ce8a634e5bad","datavalue":{"value":"separation logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2147702$0B452203-7ED9-47B9-80BD-E84B27333C53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5723ff2006ff6b387d55cb70866b952820aa308e","datavalue":{"value":"specification subsumption","type":"string"},"datatype":"string"},"type":"statement","id":"Q2147702$8F32CB41-1EA4-485F-93CF-FD4C439FB4B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fc1eb1b47753013f0fd6aa230af6a82d64e80200","datavalue":{"value":"intersection specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q2147702$5F0BA1D4-5B40-43A8-BB1E-645E1161F8B4","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$0A543C8A-A3D1-4D0A-91D0-8C00EB866F74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"174f08d95eb791d469e1c45d7c14093069896ee1","datavalue":{"value":{"entity-type":"item","numeric-id":16797,"id":"Q16797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$7690905C-1B54-44C2-8757-D38D9D30D796","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c9e521c77db45807815f297bb0abd1f031ff43b1","datavalue":{"value":{"entity-type":"item","numeric-id":39832,"id":"Q39832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$F6D86464-3302-4339-85E3-19E2A6F702C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a7de3809e549ab622397ccc7caf8aa4227aa8390","datavalue":{"value":{"entity-type":"item","numeric-id":40151,"id":"Q40151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$C4239529-1D0C-4029-A1B7-5ABEAA1DECDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"680e59220dfe1fcd219f2cf87836af5e1d29e43f","datavalue":{"value":{"entity-type":"item","numeric-id":5974505,"id":"Q5974505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$9FED8E86-FB6E-4DD8-B4B1-42EF197D0723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dee6d695234cdfbc4a272f03f51845f9fcd03368","datavalue":{"value":{"entity-type":"item","numeric-id":16399,"id":"Q16399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$3685EA63-B005-4583-9051-F193893876FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7ee2575b4b00dc5c48fe05a1a87740d06a1036d4","datavalue":{"value":{"entity-type":"item","numeric-id":21498,"id":"Q21498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$F26DF631-8131-4AE5-8BF1-A0B7FF16887D","rank":"normal"},{"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":"Q2147702$B5161EA6-6FAB-4DDE-BED0-041F3190934E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$01C35D6F-021E-47A9-B573-3CA259228F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1637c3ce3f61a15997b947ec05e883d55623946c","datavalue":{"value":{"entity-type":"item","numeric-id":19722,"id":"Q19722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$5AAFB143-764A-4AC0-8366-B7FEFAC8F740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$3FB81BE6-9D1F-426B-8427-6302D8B14A1E","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":"Q2147702$E16E4461-DC4E-4D18-8538-0052C752D05E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"573317c3cdfe2f1695c6242d9adce804b3be3187","datavalue":{"value":"https://doi.org/10.1007/s10703-020-00353-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q2147702$DDB1582C-830A-48C8-8389-AD92BDFE3DE3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"595ad9713fc4b0ab96339beb0758bfcdf4ab1c36","datavalue":{"value":"W3138908006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$B4F20B96-3941-44E2-B779-06C71EB6030C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7ab4ee3ee8ef05ab2de5721210c2223252774bf","datavalue":{"value":{"entity-type":"item","numeric-id":753944,"id":"Q753944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$EA8AF29B-3D7D-4C35-B15F-CCA6AE0A556B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c46319975d5f428b28cf95457785c347fec2d0df","datavalue":{"value":{"entity-type":"item","numeric-id":5494381,"id":"Q5494381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$EF7E8CFD-3EFD-4B1E-A115-E9C732E7472D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a8eda406b524bc7a8f585c46b182f9071cbe51a","datavalue":{"value":{"entity-type":"item","numeric-id":3087994,"id":"Q3087994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$F81AF8A7-E265-4738-877A-EC99DCC4CBCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"086fdbd21f473c213329b475c94f7dc23f61bf59","datavalue":{"value":{"entity-type":"item","numeric-id":1663238,"id":"Q1663238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$EFEABE2D-DCED-48AF-BA26-79B4467B6198","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2790188d3a2572a99d3b8280868598d27c040965","datavalue":{"value":{"entity-type":"item","numeric-id":4525781,"id":"Q4525781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$CF395793-77E1-46BC-8C05-14F8BDEFBC20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc39397aff1a518f386df54d5fcaaed065b005b2","datavalue":{"value":{"entity-type":"item","numeric-id":4625160,"id":"Q4625160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$778D244B-648A-4A6B-978F-3A7C079C5DD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a690a2cf3538761a016ee7f2e7f9e1e7cdbf71aa","datavalue":{"value":{"entity-type":"item","numeric-id":1977126,"id":"Q1977126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$852846D8-F435-40A9-80E4-DD304A13BFA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$A2565330-21E3-4F66-AE41-1B90CD2DD9EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"135af0129bd5600ceebf0463cd399deed754d959","datavalue":{"value":{"entity-type":"item","numeric-id":4411818,"id":"Q4411818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$E24F31A6-A7C8-401F-B45B-EE4B24769856","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":"Q2147702$26D50A19-5B30-4E07-894B-93DEEA5EAC4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e32e6c895a421389f04c5499d388fc13d53e99f","datavalue":{"value":{"entity-type":"item","numeric-id":2778806,"id":"Q2778806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$C4CEA817-591E-4018-909D-EDA0B80B16CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b32bffbad242579615a270378cbba850fe8dcb19","datavalue":{"value":{"entity-type":"item","numeric-id":2571207,"id":"Q2571207"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$75A1462B-80A7-4047-ACF0-D782BB5934F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1294a9f149b32a4428893a0339f4128fe743db7","datavalue":{"value":{"entity-type":"item","numeric-id":3067542,"id":"Q3067542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147702$9259E66C-61EC-4188-AB15-A6EEE4CFB86C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"55476acb6d0753e945831842570dcdf6772c043b","datavalue":{"value":"10.1007/S10703-020-00353-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147702$ED3452A8-C4A8-4FBB-A850-3BEA712A7846","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"351a90fd7374d7f2cebc9163de51f8831593258f","datavalue":{"value":{"entity-type":"item","numeric-id":2233451,"id":"Q2233451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77479454c85e319908d1c07e8c5456a4c4b1ab49","datavalue":{"value":{"amount":"+0.7804815769195557","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":"Q2147702$7134F0C6-3B28-47F1-87AC-0F38A5B60C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1e016c36edcd3a33eb45bd670c7736707a0de35","datavalue":{"value":{"entity-type":"item","numeric-id":1663238,"id":"Q1663238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a68c76fa0380718daec5bf69b6d4a25a8930cb0","datavalue":{"value":{"amount":"+0.766532838344574","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":"Q2147702$A19C2260-2866-4E72-B4FF-A2A59FFBFC99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e494b8ba3180a56bbba4cac54a6e75bdaf5b8f78","datavalue":{"value":{"entity-type":"item","numeric-id":5276150,"id":"Q5276150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1b066a324d63e50746294d1d85ac368e2a3daf8","datavalue":{"value":{"amount":"+0.7266131639480591","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":"Q2147702$9AF303D7-ACB8-4362-A049-2B2CE81D658F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66e125d08823e9eeeea82b37bc8cc9a6da32af54","datavalue":{"value":{"entity-type":"item","numeric-id":835768,"id":"Q835768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0d7185e19cfd705bd20b8201946b1a5cefac48f","datavalue":{"value":{"amount":"+0.7265284657478333","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":"Q2147702$4E32DA49-2913-435D-B350-996802FD348E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"211db3e7f011d05bb69203eff288ae10938d3e1c","datavalue":{"value":{"entity-type":"item","numeric-id":5385589,"id":"Q5385589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3784c108e1a90540864e943a024c44c978e2ec21","datavalue":{"value":{"amount":"+0.7167783379554749","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":"Q2147702$85DB525D-009C-4962-ACA3-8358F820C3A0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2147702","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2147702"}}}}}