{"entities":{"Q816201":{"pageid":818049,"ns":120,"title":"Item:Q816201","lastrevid":49789507,"modified":"2026-01-10T18:40:53Z","type":"item","id":"Q816201","labels":{"en":{"language":"en","value":"Formal verification of the VAMP floating point unit"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5007754"}},"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":"Q816201$09539AA0-CEA1-4636-A72A-579AF738E237","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b88bf8e72c0ffd659100db6247ef42788e870f81","datavalue":{"value":{"text":"Formal verification of the VAMP floating point unit","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q816201$12E6F111-E532-4E67-B566-33830BC59C63","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"35befe20fd540c069fa51fb6a4711680754174f4","datavalue":{"value":"1086.68518","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816201$8E0A4A4F-BA8A-422E-94D3-8150634EAE0B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e2127eec4ba281abb8966ef52832ebc2ecbc5c1","datavalue":{"value":{"entity-type":"item","numeric-id":816199,"id":"Q816199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$EAF26C48-0CD2-4F96-A748-8837AED03AA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"26782b83bc5c887a3a53c8779f05ad2e63070ab2","datavalue":{"value":{"entity-type":"item","numeric-id":816200,"id":"Q816200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$23F88CA5-5261-4226-9938-9885BD2B5976","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":"Q816201$47EE4641-0DE5-4747-A69F-84F67DBBD93F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d5a46ca8715888f9181d63a117c8c9aa412098d3","datavalue":{"value":{"time":"+2006-02-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":"Q816201$BE20B92A-6D30-4E50-BE67-E79C5C36818D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"06aaf19f4bbdd9676f0ed308701e830d30be51c5","datavalue":{"value":"68M99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816201$004ECF53-8CC6-4D78-A079-60F27E0C2BF5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb013b98638b783e1548a0d2af9f967315656f52","datavalue":{"value":"5007754","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816201$93E807DF-404A-4394-933B-507101EFCE90","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6dffbe17987cdad05ed09fd93c8757783375e50d","datavalue":{"value":"floating point unit","type":"string"},"datatype":"string"},"type":"statement","id":"Q816201$F625FA01-9D6A-45A0-9778-6DEB96066A26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q816201$1F2FEB6D-C84F-4F75-A92F-0C38631E2D00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9ddd6390e74391578ea62dab4051aac9888aa7d","datavalue":{"value":"IEEE standard 754","type":"string"},"datatype":"string"},"type":"statement","id":"Q816201$B0AEBC4E-1BF4-4ADE-8DA3-EEEBC5C582A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q816201$7AFE26BF-37A7-4740-A93E-8FF3AB9E06F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q816201$55CA1F58-AB85-4C4F-A2DA-83234926B9D3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$3A8CA37B-5940-4308-B786-7E04F9182AFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$2327F077-BFDE-4A85-A658-B3A43E972542","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":"Q816201$743CCF24-35F0-4A5A-968E-6B0267BA1B79","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":"Q816201$D193AB4B-F933-473F-BF82-1FACD1CC6301","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e1a5b1c14ab21a56a4d6c6e8c349c6e899e13c94","datavalue":{"value":"https://doi.org/10.1007/s10703-005-1613-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q816201$398A0C6B-F69D-43BE-94EE-3A5CD3ADA7AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7f03be9994baaa1e1c335fc946d8629771023d11","datavalue":{"value":"W2157753532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816201$B6D026E6-06AA-43E9-ACB1-3609ACE47B0C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6230eb5099e27c7ab57f995d507233f844638ee","datavalue":{"value":{"entity-type":"item","numeric-id":2754053,"id":"Q2754053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$47187589-782B-4FE0-8A13-CFA3FB50DE15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73be90735838b7922cc6ea358a4a7056c4765ec3","datavalue":{"value":{"entity-type":"item","numeric-id":4787242,"id":"Q4787242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$3B44E267-3055-4716-98B9-33812FA2B7F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91d83abec22f28b19800352199911df73da724ab","datavalue":{"value":{"entity-type":"item","numeric-id":5897057,"id":"Q5897057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$52645BFF-E53F-4FE5-98BC-AA41BDFF97CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2940d495eb2b669794d95ca8ddbb03437430e8b","datavalue":{"value":{"entity-type":"item","numeric-id":4790659,"id":"Q4790659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$E09E96C3-7D00-4D84-8AC2-1458AFC57838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"313795597e095eb856bc35d86675fdb69ac186ec","datavalue":{"value":{"entity-type":"item","numeric-id":4571360,"id":"Q4571360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$2D19E702-76F1-470B-B21D-F6322E2EDF6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0f7b9ad80057c9ca5c9b18a33cafda29b9317b1","datavalue":{"value":{"entity-type":"item","numeric-id":4860810,"id":"Q4860810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$AA11C7A9-9148-481E-AAE1-864BD8DC1D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a639d6ce02b12e61efb79efe22756885c781f9ba","datavalue":{"value":{"entity-type":"item","numeric-id":4804904,"id":"Q4804904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$62AC1B9F-5A23-4B29-A628-C0E7283ED8C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b4057c89110ed5546a59ac677c1664783555b43","datavalue":{"value":{"entity-type":"item","numeric-id":4787230,"id":"Q4787230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$D7A1BD22-586C-4D08-8E71-8A24E76E486A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c97813355f8a3ed047649f2193bf1bd050bdd9f","datavalue":{"value":{"entity-type":"item","numeric-id":4494691,"id":"Q4494691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$F8FA8B2A-C834-4A35-BE55-52C8F6B82D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afefbaf137f83b64b00e4ef48cc98682850f21d5","datavalue":{"value":{"entity-type":"item","numeric-id":4230664,"id":"Q4230664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$90C55FAE-1AA3-44E7-B423-4A51832FA45E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d106093459e030e9ab8e70edf35d232c482a92ce","datavalue":{"value":{"entity-type":"item","numeric-id":1314510,"id":"Q1314510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816201$BDA0AECF-4B98-4EE9-AE4A-1AE4E089AC53","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eb012699855cd0b2e386b61160db3c7deb911ba8","datavalue":{"value":"10.1007/S10703-005-1613-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816201$8177B72A-C216-4B94-96F1-25E0D870A57E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c7e7fb217c914e638e4f5584326c05b02f37a783","datavalue":{"value":{"entity-type":"item","numeric-id":4787242,"id":"Q4787242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a4ad93a4f81c32f00c2718a29c9f537010c1c70","datavalue":{"value":{"amount":"+0.9628811478614808","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":"Q816201$A50CCCA5-DFF8-4E87-9016-8B7621A4B785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0adab14be603a93bde827af0da3bc9888b83cc92","datavalue":{"value":{"entity-type":"item","numeric-id":4230664,"id":"Q4230664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9accb39ecc58bea910fc1330798bc60dc940087b","datavalue":{"value":{"amount":"+0.8347865343093872","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":"Q816201$5FC26DAE-B22E-402B-A2C8-DDA03DB20D03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4042647b40b7232d9e5d270d53453de771416c9","datavalue":{"value":{"entity-type":"item","numeric-id":5159259,"id":"Q5159259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c436caf6b4ed1981cc4941dbdb73dfdec2bb669","datavalue":{"value":{"amount":"+0.8203017711639404","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":"Q816201$6AAD38A9-CE73-4329-8A7F-D9FF8B7BA189","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f91743ae3c8568d1b04bd42aa171ffdda9d6e4b9","datavalue":{"value":{"entity-type":"item","numeric-id":4412533,"id":"Q4412533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d097933fff468f431c1ed799846b0b205deb3f1","datavalue":{"value":{"amount":"+0.8060190081596375","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":"Q816201$E8E91A2B-08CC-4A3D-9297-E563BD598F02","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":"e175af36eeadcc29f88c8a150af35213d7dbefc9","datavalue":{"value":{"amount":"+0.7837120294570923","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":"Q816201$DE6F5BC5-1B8B-418A-B384-FBC4353B4B4C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:816201","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:816201"}}}}}