{"entities":{"Q4988925":{"pageid":7018502,"ns":120,"title":"Item:Q4988925","lastrevid":55966033,"modified":"2026-02-21T14:22:04Z","type":"item","id":"Q4988925","labels":{"en":{"language":"en","value":"Abstract contract synthesis and verification in the symbolic \\(\\mathbb{K}\\) framework"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7350033"}},"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":"Q4988925$EAC618E4-1A95-4BAB-8562-9606A5894AC6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"26b9569d977bbb2d0c79b7c19355a6c9364ae107","datavalue":{"value":{"text":"Abstract Contract Synthesis and Verification in the Symbolic \ud835\udd42 Framework","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4988925$D31D9CE0-6CEA-4CDF-8BD5-773B6AC135CC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1d3c57487c9dd46fd3ad8b8b68866a39f79e1e4f","datavalue":{"value":"1497.68106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$3C43E40B-964D-4E26-ABE9-260191EF0103","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"99210c8a2b64909516b22a32d58bf0d9340eb522","datavalue":{"value":"10.3233/FI-2020-1989","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$F1C617C1-DA96-4204-BB2C-619916D7B22C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"65d58dce9335ad8803534573ec5bd4ff4bf4b330","datavalue":{"value":{"entity-type":"item","numeric-id":2321073,"id":"Q2321073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$1C717079-DEB9-45F2-9538-380EBD7EFA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"36308e32b5a03059e4bfa8be66993d163941fc86","datavalue":{"value":{"entity-type":"item","numeric-id":2409735,"id":"Q2409735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$728C7ECE-79EE-4BD0-8042-722EDEA1A934","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b9ad0f43ee1ceda3dd968cb3b2fb5c858da6895a","datavalue":{"value":{"entity-type":"item","numeric-id":671507,"id":"Q671507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$AD0BE4A8-ACF2-4FF4-8893-169A1C476292","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1529db038bde6a8aed76ac5e8432917aee1a9200","datavalue":{"value":{"entity-type":"item","numeric-id":2803574,"id":"Q2803574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$5F014039-3385-45C9-90CE-71375B92ABC6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"211031a52806337129a1eef00df007a6622a5387","datavalue":{"value":{"time":"+2021-05-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":"Q4988925$01ABE760-89E2-40C9-9FCC-5A3E340723F4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$490AE446-208A-442E-9B80-90D059076DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$DE5BAFEF-B0BF-40FA-AFC7-63F49729C7A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$321085DC-FA28-402D-8333-5113DDFBB716","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"61ae87e430ad2a664f5c9b2b50a05bc758cd8cd3","datavalue":{"value":"7350033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$E4303186-FA06-4329-A458-E2CBF527E90B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eea8ca7075190f2c2c06c4ea617a9eeb5bbefef1","datavalue":{"value":"contract inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q4988925$D0D75AB8-CDD9-46FF-99FC-7EFB03F322B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69dd490da9b67dc4fe4c624a05791d0c4fa27f2e","datavalue":{"value":"symbolic execution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4988925$B4710EB5-0165-4AB6-B50C-690743D0246C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0546c90fcd67296b136e3cba1186af2aab81422f","datavalue":{"value":"abstract subsumption","type":"string"},"datatype":"string"},"type":"statement","id":"Q4988925$F18695BB-CE31-4BAA-A89C-EE975AD759F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4988925$C0ED289D-247C-49C0-8C6F-5C171FDD6A92","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc61f5d85676d96d8740575ab7a32a3d10e30835","datavalue":{"value":{"entity-type":"item","numeric-id":33414,"id":"Q33414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$6387AE37-C35B-4CB8-AD04-98B628C800C5","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":"Q4988925$CFBBBFDA-8919-4724-8BF2-4793792EFD6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$6B8B862A-DD3B-45DF-88F2-BCDCA8DFEA01","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":"Q4988925$C3300EF1-B356-4E2D-87D2-AAE6FB7584AF","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":"Q4988925$7EA9E2CD-6DC9-4CE0-84D1-FA39F0FD58FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"600d8a1514e6fed4e4c66ebeb9b62bee4bc86b61","datavalue":{"value":{"entity-type":"item","numeric-id":4417936,"id":"Q4417936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$03234F23-25CE-4672-8A8C-09418E749EFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8135d2b21803eba4e4837602065847af8c31a6fd","datavalue":{"value":{"entity-type":"item","numeric-id":3787422,"id":"Q3787422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$F0F55256-0BF5-4FB0-8CBB-32F3F79183EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83fa1aea41b23b77e49c2e6c48c1b67f2ce6b255","datavalue":{"value":{"entity-type":"item","numeric-id":4095837,"id":"Q4095837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$5F9643DB-A257-4C95-B02D-FBF51DB9EB7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23623728af77877c2c658b5f16ea2ac66fec79f9","datavalue":{"value":{"entity-type":"item","numeric-id":987974,"id":"Q987974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$BABF8573-8405-4272-AB78-AE51C49BCD73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"626fabf8b26cfe6bb444d73ba24ee22259902ffa","datavalue":{"value":{"entity-type":"item","numeric-id":1749128,"id":"Q1749128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$4C57B6B0-9940-4FC5-846E-0788BC499D00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37f11d087fb352d8b17c817d210efa2f25331977","datavalue":{"value":{"entity-type":"item","numeric-id":4417955,"id":"Q4417955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$AB75018D-F454-4B5F-85F5-9006E1F4D346","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f47472a8d03d2f478529f1d7346717f059c86f4a","datavalue":{"value":{"entity-type":"item","numeric-id":2409736,"id":"Q2409736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$CDFB6CC7-7BB4-4925-BF98-A3CFC133C2B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"391e966cda7841966699f9d7a3bf9750dda40e97","datavalue":{"value":{"entity-type":"item","numeric-id":3992568,"id":"Q3992568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$AA161319-E521-48D4-8EFC-23BF4A2B0E1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1175367724993f3e0249db2e141c79883c1c01f4","datavalue":{"value":{"entity-type":"item","numeric-id":5711490,"id":"Q5711490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$A45F4192-9F10-4E54-BA83-967060AD6FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2308082f9a80f9a7eb4caa9bee27706d8306e6f1","datavalue":{"value":{"entity-type":"item","numeric-id":2945730,"id":"Q2945730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$0176E5CF-A88C-445D-9866-3790AD3AED1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bbfbc9d107d10f469b35a5fc043708881c82d23","datavalue":{"value":{"entity-type":"item","numeric-id":4856658,"id":"Q4856658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$8453FA66-A2F3-4603-8699-A020CBFD49DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88d1b205201f13d82c065e97ff01a6bc59a545ee","datavalue":{"value":{"entity-type":"item","numeric-id":5271073,"id":"Q5271073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$2C40A94F-D4CB-47CD-9AD1-D4C86034D57A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1832a8f9f3048a5dffcc1f9a0d084d432f65a88c","datavalue":{"value":{"entity-type":"item","numeric-id":3392926,"id":"Q3392926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$4F91BCF4-CB4E-4FBE-8B0B-56ADDEC90932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2023b97550e2a7e9dc61b29f602d69fb831f0b7","datavalue":{"value":{"entity-type":"item","numeric-id":604392,"id":"Q604392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$AFEE0F59-7190-49EB-AAD3-D48D7C2A5DB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"458dfa6fd44072143815c860d3690f1687a12132","datavalue":{"value":{"entity-type":"item","numeric-id":2463543,"id":"Q2463543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$ADF9F4AB-F285-4594-9E96-79EB3B590F1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f927eef2ff97bc2ae67635a63548bc51b9896f2b","datavalue":{"value":{"entity-type":"item","numeric-id":5371995,"id":"Q5371995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$1037A240-BB4D-4104-AE69-F269FF62475E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4a322e28578b4a1afe501621a0109e6461fb8d9","datavalue":{"value":{"entity-type":"item","numeric-id":5398052,"id":"Q5398052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$2AD2AB90-2ED0-48FB-8273-678D0BE68D75","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":"Q4988925$00A9648D-9E6E-4F6B-9E09-286F19967263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd073d5f1b45c21954c5cfcc1b9243be226d02ac","datavalue":{"value":{"entity-type":"item","numeric-id":5429321,"id":"Q5429321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988925$516193BF-7BF3-43BE-89AE-93C9CD1027E6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"486d8c8331e93da7b709e6f6c4f57c1990017776","datavalue":{"value":"https://doi.org/10.3233/fi-2020-1989","type":"string"},"datatype":"url"},"type":"statement","id":"Q4988925$D3CC9915-C2C2-44ED-A53C-4C03491D346A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"07a9478b19dd5dd3419d84dc144c037f4d56fea0","datavalue":{"value":"W3111118845","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988925$C46FF5A2-A24E-4035-947A-442F9B2B1A04","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92839d41dedbd0185b71170cf641b8ae7af57f80","datavalue":{"value":{"entity-type":"item","numeric-id":2409736,"id":"Q2409736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5424a007a3aacee85531265ed360f9cbda10dde3","datavalue":{"value":{"amount":"+0.9356695413589478","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":"Q4988925$C2F30C52-3D1D-4089-B442-7D1B6035EF2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a840a40cc352fcfa7b956c03a07ea490f36f99c4","datavalue":{"value":{"entity-type":"item","numeric-id":5371996,"id":"Q5371996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1ccbff6a47707d98d034f4cabfdd951e5b6c984","datavalue":{"value":{"amount":"+0.7229343056678772","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":"Q4988925$D21AE29F-2498-4B98-A334-F5C31098DA78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4a4841cbd91fad18a3443c16cb27b975d599133","datavalue":{"value":{"entity-type":"item","numeric-id":5902410,"id":"Q5902410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0f930c1eded066556eb4215a3180aded0b7b6c3","datavalue":{"value":{"amount":"+0.7067056894302368","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":"Q4988925$EF2332F9-5898-47B8-9514-4EA2837F6211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d19e005a0abe117167f38c3b5f5143e8643419a6","datavalue":{"value":{"entity-type":"item","numeric-id":604392,"id":"Q604392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"857f2423d9804be3fd54285e7b13b4b1a1263eb4","datavalue":{"value":{"amount":"+0.7059221267700195","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":"Q4988925$6DCFD9EA-9B7C-4E24-8EAA-DB5F48E6EEE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"149dbc9ca3addc70c8e9bb7aa3f9b8fe64c83ad8","datavalue":{"value":{"entity-type":"item","numeric-id":2828322,"id":"Q2828322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e19608a9d689b49a8087be22ea7dcc6fbab3ef7","datavalue":{"value":{"amount":"+0.7025529742240906","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":"Q4988925$1FD35A7F-DAC1-4EC7-959E-FA7F1B7C4343","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4988925","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4988925"}}}}}