{"entities":{"Q2233510":{"pageid":2244253,"ns":120,"title":"Item:Q2233510","lastrevid":73842465,"modified":"2026-04-14T17:27:34Z","type":"item","id":"Q2233510","labels":{"en":{"language":"en","value":"Deductive verification of floating-point Java programs in KeY"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7410489"}},"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":"Q2233510$C423F7AE-A5EA-4266-8DDC-D0FE2C067C4A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"213f9bea426a4c96233130ba18cc1f485c2db413","datavalue":{"value":{"text":"Deductive verification of floating-point Java programs in KeY","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2233510$E4C29AFC-019E-4C06-ADCF-BC5D7F7A07D9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4cf2eae9b9a5763115695aa66c0c92659842936c","datavalue":{"value":"1474.68186","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$8C75A9E9-8E19-45EB-851E-77CDD4AE05BB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ccd8c6dad0419d699f84be4cfc39fa32f9fef100","datavalue":{"value":"10.1007/978-3-030-72013-1_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$B176D076-A8B7-45AB-B3A1-0597AC04AAE1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a858c491fcf2ce62d8e3f3bb447f496f6d21769","datavalue":{"value":{"entity-type":"item","numeric-id":1731829,"id":"Q1731829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$7EFB81D2-3C96-4A78-81C1-78B08959BEEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dd054cb7728b2a0bf2d3ed984a328fdecda1e2f1","datavalue":{"value":{"entity-type":"item","numeric-id":1630023,"id":"Q1630023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$84A63C4A-0526-4C78-AE92-6D2F42398531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc64b0431d237d2cb162de6a38437bcb6b852e6d","datavalue":{"value":{"entity-type":"item","numeric-id":2024355,"id":"Q2024355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$7AD58F5A-42C9-4EE1-A61B-DE610B638EED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"54b40af6acb3456c1b6977fa01e79eec0014485a","datavalue":{"value":{"entity-type":"item","numeric-id":1630024,"id":"Q1630024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$F8005E66-7028-48D3-A66A-FB88B3DCF5C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"38294c3226d3792efd0f0a6334adfdf20cdb195e","datavalue":{"value":{"entity-type":"item","numeric-id":1951608,"id":"Q1951608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$6AB651A5-84BE-417E-9D35-D170318E04C2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"899d672926fe97cd87f3708d91dc74172e4f3b51","datavalue":{"value":{"time":"+2021-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2233510$DDCFCAE6-3F94-470D-B8EF-C99F66591057","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e0320b91e204cc403c36cbddb16db6fa2fe4f997","datavalue":{"value":"https://arxiv.org/abs/2101.08733","type":"string"},"datatype":"url"},"type":"statement","id":"Q2233510$569BD39A-A035-40E0-BEB2-A576AEE84C2C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$4E2C2768-D698-473C-B578-EE35ADCB8905","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"224133dd68a4f3b66ddf7d50fd627018c06684e4","datavalue":{"value":"65G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$A2178F96-B49C-4064-80F9-2DAD28C33CC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$3A4325C8-CED6-44B3-B12C-DD77CD233E60","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2df3f351095d65e360782cb6e7911dca33567d80","datavalue":{"value":"7410489","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$508413D6-69B6-4222-BFCD-D26841D6DD58","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233510$0795D608-23E2-4DA6-A8F0-C5AEEEF95EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233510$31D416B5-102E-4EB7-A7C6-A0AF677E707A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"819f137f9ec626acba1c8947981be8a93c7821b2","datavalue":{"value":"transcendental functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233510$E0F0779F-D154-415A-9093-66C4C690752B","rank":"normal"}],"P1463":[{"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":"Q2233510$C614A61B-FE74-4296-978B-62D9C47AB2C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fe5077d712c4f7a91829b6a22ef0e0039cd600ea","datavalue":{"value":{"entity-type":"item","numeric-id":15691,"id":"Q15691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$70FD3183-912B-4213-BA6E-B12CDC418F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$0B01D6E0-D0DE-4159-AAAF-D364644F6BFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"15df3347da4f77fd05a06551feb8504f4b1bfb98","datavalue":{"value":{"entity-type":"item","numeric-id":31665,"id":"Q31665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$197DA28C-784C-4950-8CD8-B2473BA8EC54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b9afd1e8fc349d198c89a22f85926ff81edbd463","datavalue":{"value":{"entity-type":"item","numeric-id":26932,"id":"Q26932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$77805800-C83C-444F-BDB7-7B3D20253DB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ba44c00a1dca3a3675ca0a9e2d9e7fbaf25b9e12","datavalue":{"value":{"entity-type":"item","numeric-id":37641,"id":"Q37641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$8493510F-D044-44C4-9C10-7F80CBA1BC8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$B54B4965-F629-4A4C-AD65-B4CDD224B008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aa786b5c8269f6cf517ad0f032932817c0bb268f","datavalue":{"value":{"entity-type":"item","numeric-id":18875,"id":"Q18875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$A75B9BAC-9E24-4181-8782-64D1462A6032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$0B8C7803-1D5F-4390-8B9F-B1E42A8A5862","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d2f61eeddf1828d82b7393c95d22003b9c58afa3","datavalue":{"value":{"entity-type":"item","numeric-id":19210,"id":"Q19210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$D6F4B81D-22D0-492E-B98E-5CED29AFC19A","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":"Q2233510$610712BA-7329-4A63-BFE8-CC55DBB04384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$82570062-1DB5-48A5-9C2E-02A1F4FF14D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12b8fef36068e5bdaa4e8c4c10a706c6f98b9349","datavalue":{"value":{"entity-type":"item","numeric-id":21946,"id":"Q21946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$6AFBE5FC-1057-49F9-B9B2-CA2BE351D2D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a87571fce9d57d6b7264f57af4011b2fd5ef1520","datavalue":{"value":{"entity-type":"item","numeric-id":56293,"id":"Q56293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$17E2F809-577A-420E-82A8-E80DC6630016","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fcdbfa32784c23b7fe08f942b96ddd3d82a0a653","datavalue":{"value":{"entity-type":"item","numeric-id":56295,"id":"Q56295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$8933C12E-1DFD-4939-8F64-9CE5FE35DF07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"734e42efcc5acc9a70e5f97b719e8699f2d9a314","datavalue":{"value":{"entity-type":"item","numeric-id":56294,"id":"Q56294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$B3BCC116-7D65-4156-92C5-D89191A8163A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$1CB51EAA-325E-49D7-B076-27F176BBA727","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$9A8E36BD-1661-4940-8080-B9FA97873045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"38bea4297d9f2f2e9764919709eca5e372065699","datavalue":{"value":{"entity-type":"item","numeric-id":12818,"id":"Q12818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$FB341996-2CA0-4565-B3D1-4F7C73F804D7","rank":"normal"},{"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":"Q2233510$1FE5B08F-02FA-4D7F-BD13-4AD51E686FD1","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":"Q2233510$7FEAA132-B960-4E57-9FE0-BB4CA03C2D64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$83CD2BED-3D5F-46A4-8B46-84BC501D6DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"42950e8602f0bf155e8f0e40e68f674e5831f7bb","datavalue":{"value":{"entity-type":"item","numeric-id":21550,"id":"Q21550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$98F5BCCA-8BF2-4A0D-AC5D-07F1F4042D84","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":"Q2233510$CC34B821-B12E-4962-8BFA-5290A829E68F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3162e659f28e117def5ad1c288eb199ec8a0d901","datavalue":{"value":"W3146695734","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233510$18FC7444-4987-4396-B962-12EF6F5E4D15","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a602a31ec5858953936704adacfb1f5bdcaed350","datavalue":{"value":{"entity-type":"item","numeric-id":972422,"id":"Q972422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$EB302DFD-26A4-4DAC-BDA8-364F683EBC25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52a1a1a1392ded61e6c64da43feaf22a7950d952","datavalue":{"value":{"entity-type":"item","numeric-id":2931838,"id":"Q2931838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$477FF08F-5839-4ACE-82DC-18B919822793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6826931c7fbd099e876410cceeef903bc184e57","datavalue":{"value":{"entity-type":"item","numeric-id":4414726,"id":"Q4414726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$16C1166F-A182-4454-A207-F84FA7F8DC7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6ecc4a9847b1757b816a66a2c8d99f5449bc756","datavalue":{"value":{"entity-type":"item","numeric-id":352952,"id":"Q352952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$DEE2C6E9-4934-49F4-8ECE-DF6B4A29A9A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbb7fdabd5a856f8e1d09080b76afc7309a50a3e","datavalue":{"value":{"entity-type":"item","numeric-id":3637269,"id":"Q3637269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$AE681984-8FFC-41C2-BDD1-E9D10EB864E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21640ae8e3aa02debe92970cf2184aca918b76e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326318,"id":"Q5326318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$D2DD3930-42A6-4AF9-B780-783148000851","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b020a91ffd3c81f18a1e5e555d90c0a605e24a18","datavalue":{"value":{"entity-type":"item","numeric-id":5408419,"id":"Q5408419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$1629FA7C-D286-4262-A85C-41F7F635966D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc81427ce87e6cbaee7bf3723fe7564840540ed5","datavalue":{"value":{"entity-type":"item","numeric-id":1630033,"id":"Q1630033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$B37D70CA-3017-4D8E-BE19-22A1C374A1D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe33bf4e1ec51f59c09f65752ea810761eb09a2a","datavalue":{"value":{"entity-type":"item","numeric-id":4928439,"id":"Q4928439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$15E991F8-01BF-47A3-9872-CDC8059DCC8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$09AF475A-CF21-4549-8DC6-2D4412A69287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7842cc7997d2d8faf03cd74c496ae509956b9581","datavalue":{"value":{"entity-type":"item","numeric-id":3075485,"id":"Q3075485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$2BF3C254-5B59-4068-8FEB-FBF740209AA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aaf66c6b46b567a5cdc53e98afdb0efcafa5e37d","datavalue":{"value":{"entity-type":"item","numeric-id":4789445,"id":"Q4789445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$E46DFCE9-19E8-4748-B5D3-5835711BF939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e271733ec76e1b5dc30187cdb76a992b525bf482","datavalue":{"value":{"entity-type":"item","numeric-id":2233532,"id":"Q2233532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$4D46F027-9B7D-4D7E-B6E2-C49CBE183B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e7d5ae19ceb74486133d17c8479ae773e6fd29f","datavalue":{"value":{"entity-type":"item","numeric-id":2520685,"id":"Q2520685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$4E97975C-6A39-4421-83E7-2A04200F2312","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e0215749ba1a507181a8a777bfd7878a71e7ff9","datavalue":{"value":{"entity-type":"item","numeric-id":3133585,"id":"Q3133585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$E8E8A94F-DBA4-4C41-982C-0562D781F5D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eddd8cbb64d539857cacbe7cdb050d3d43884a13","datavalue":{"value":{"entity-type":"item","numeric-id":1881670,"id":"Q1881670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$016B0449-DD5C-42CB-A001-119F9236DD43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9da274f8b55281fb4f3f25740da1cf036b4e73f7","datavalue":{"value":{"entity-type":"item","numeric-id":2947225,"id":"Q2947225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$FCF8CDCE-0D8A-4D42-840E-AC56817075FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0410914bfe194e14ab162760d09e45b8722d5b6d","datavalue":{"value":{"entity-type":"item","numeric-id":1630022,"id":"Q1630022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$2A389F42-B73E-42C4-BC41-23DAFD52015F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d077f7417b2812e541ae3d63f2b9abb351153146","datavalue":{"value":{"entity-type":"item","numeric-id":3629031,"id":"Q3629031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$9AAB069E-A977-40E9-B434-5DC4EDA81E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3422aaa623eb5f87aeca9f244e6f007c7eb8ce2c","datavalue":{"value":{"entity-type":"item","numeric-id":2796035,"id":"Q2796035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$AB77ADF1-8860-448C-8F62-DB0CEF3F7448","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83c978ed0eb834f46527acd6a93f4b47491cfbfd","datavalue":{"value":{"entity-type":"item","numeric-id":5206960,"id":"Q5206960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233510$4A0D8FAB-2273-4A69-BC35-7636D0C593B3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab31d5912cadbbfefc841f45e39fc28cb02cf95c","datavalue":{"value":{"entity-type":"item","numeric-id":5747756,"id":"Q5747756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1793937b983d920545bac5d573cf413ed318d812","datavalue":{"value":{"amount":"+0.8404642343521118","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":"Q2233510$EA8FEA4D-3741-4F1A-BE54-0368D95051E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2456a4221f4f4afd5cdaf689ddf8012c09f5d13","datavalue":{"value":{"entity-type":"item","numeric-id":1630033,"id":"Q1630033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0d8caaecfedb511c4bef144b72e9b53e390a06a","datavalue":{"value":{"amount":"+0.798076868057251","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":"Q2233510$6EC04573-4E20-4349-BF75-7B0A33036101","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"634865f6354839c52530abb008d3913b47aec7f9","datavalue":{"value":{"entity-type":"item","numeric-id":2152274,"id":"Q2152274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34bb0cbee1f6a6334f41d32e979ec0ce6e55cd4c","datavalue":{"value":{"amount":"+0.7464579343795776","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":"Q2233510$FB07A06D-4B7A-4EAC-B01C-E568E7A79447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"688dc3a554669b3a1e0ced4ab92a8787af0109bc","datavalue":{"value":{"entity-type":"item","numeric-id":2233493,"id":"Q2233493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64d9a7391c6880be36de6dd6af1a08d6e6cda704","datavalue":{"value":{"amount":"+0.733921468257904","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":"Q2233510$EFA52013-BFDB-4B9A-9589-930CD8C41587","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39543e823be30e37369ab04509198db83e3988ed","datavalue":{"value":{"entity-type":"item","numeric-id":2352505,"id":"Q2352505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ad5d5a364517337b54cdcc200571cb2dddd0b69","datavalue":{"value":{"amount":"+0.7178428173065186","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":"Q2233510$CEF73FBC-E492-4105-BD03-BFC184111C0E","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":"Q2233510$020DB0D9-2799-4BBC-92FD-9D794A722599","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Deductive verification of floating-point Java programs in KeY","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Deductive_verification_of_floating-point_Java_programs_in_KeY"}}}}}