{"entities":{"Q2336214":{"pageid":2346957,"ns":120,"title":"Item:Q2336214","lastrevid":57312876,"modified":"2026-03-30T09:29:54Z","type":"item","id":"Q2336214","labels":{"en":{"language":"en","value":"Functional verification of high performance adders in \\textsc{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7131397"}},"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":"Q2336214$C66D19BB-0C82-4EEB-9118-D0363E17629B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c1767158ba5fb78fede49a70035716b27a29e7e1","datavalue":{"value":{"text":"Functional verification of high performance adders in \\textsc{Coq}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2336214$97849DE9-4E08-4A48-83A2-1A65F30066E5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f9427690aedad354598d927154548f64173fc8c3","datavalue":{"value":"1437.68191","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$FD65EF40-AA28-4B0C-8299-CF703BC53548","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6e1460dec1e2838af3bb4672b5c4dcaa95a96a1b","datavalue":{"value":"10.1155/2014/197252","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$63429D82-71C3-484A-B012-46A3AD1ECB3C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$CCB689C1-9575-47B7-BFBE-E993DA130EFD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$CAD502DD-8185-45E4-AE5C-044CFDCC0AD2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"10393ba55f1a886ba53e75eccd4b56403eff1eb9","datavalue":{"value":{"time":"+2019-11-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2336214$B0CC7A22-0FC1-4C70-A0AE-8A44FD2B6860","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6bee14e194a7ac707faab6e6369ab0f59097507d","datavalue":{"value":"Summary: Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant \\textsc{Coq}. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2336214$AD0B5EE2-D4CB-425C-88BF-D1545D2B27CE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$39838296-8A13-48C8-BDC2-F67A4024F23F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$0C7F1A50-E761-4A87-A9F2-8946DEBCA36F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2bf534479b9242e973ca011ffc03f5c515318eab","datavalue":{"value":"94D10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$450E9442-6D13-4752-B5C3-0362E901C54F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74d8e3ae1f12c3ed092a68b106e200ffaaaaad90","datavalue":{"value":"7131397","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$862942B6-C569-4914-B054-B6628BD928C0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3d91dd644b176d258cfbf9d590ecf2d6ab75492b","datavalue":{"value":"Q59050211","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$B853FB81-107F-4730-8DA6-7244804B59A8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5a61edfee27b9a0d876bc3ac3487da750de8fe51","datavalue":{"value":{"entity-type":"item","numeric-id":30968,"id":"Q30968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$4B3B7A4B-B4FF-407D-992C-E021589CE577","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":"Q2336214$5FF2F913-E2E2-4865-8065-9E70AD439005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9d98cd6fe8b5d5dd6b234efad298fe3f54a4c5f0","datavalue":{"value":{"entity-type":"item","numeric-id":14658,"id":"Q14658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$56EE7260-41FA-4793-9FA5-F8E10DBD9360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ddd31dae9cec559546306beb5fe50048bbc464af","datavalue":{"value":{"entity-type":"item","numeric-id":21898,"id":"Q21898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$C4B36206-A643-4780-9534-2D14D81D9180","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":"Q2336214$4DED78DA-5AA6-4650-A968-AD38AFB0A501","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8d8b91659d08705a49791bf9f0add8e039f26f34","datavalue":{"value":"https://doi.org/10.1155/2014/197252","type":"string"},"datatype":"url"},"type":"statement","id":"Q2336214$5AEF0CCE-415C-4A8F-A3A9-E0C9E2F4DFD0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"56e4efa4f5c874814cf4d29db7083ed5d2d8978b","datavalue":{"value":"W2029501708","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336214$0266C3D3-8293-4761-A8FD-CF705104C07C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e958d98fa90afed8c151948b50a5815e78bbf67d","datavalue":{"value":{"entity-type":"item","numeric-id":1188591,"id":"Q1188591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$09FACF57-271A-48C9-8DC8-AA91C346AB3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61afac04eb84f36706f34e95c93c5256a07b751c","datavalue":{"value":{"entity-type":"item","numeric-id":4647582,"id":"Q4647582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$B529C636-53FF-4971-B907-78352FAC0956","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d42e5dea39186928a0c58c53a8feccbddaca803e","datavalue":{"value":{"entity-type":"item","numeric-id":1764432,"id":"Q1764432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$CFEDA761-3D50-43F7-9035-AE1CB265B2BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64738746c7f98fb10a5cd52a09a9338c108e599b","datavalue":{"value":{"entity-type":"item","numeric-id":3100217,"id":"Q3100217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$872C30B8-4D8B-44B4-B931-CC0ECB1F1A86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"399b2a8f371ad538a3b28b6b50d444ee02799f3b","datavalue":{"value":{"entity-type":"item","numeric-id":4660267,"id":"Q4660267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$936A5154-8A51-4700-BDA9-EB4F225218B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52d05f02364f0e4643eddb26640cc2b83e9e4a23","datavalue":{"value":{"entity-type":"item","numeric-id":611751,"id":"Q611751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$ED988E8D-5648-4F36-B662-4C19BA67CC0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9751d8f12e3f2c7dd6bcb47ce70a0a4e9d0ee68e","datavalue":{"value":{"entity-type":"item","numeric-id":5313086,"id":"Q5313086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$A318F782-B689-4C80-A2F2-E0DB836495E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efbf9b29f74753ca9de9a61e2d0ebdd560c657a7","datavalue":{"value":{"entity-type":"item","numeric-id":2958550,"id":"Q2958550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$C18F6AFE-68C1-413A-BE2E-196AC1221234","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3da88952a37254da86caa5d2e1716d0cfee3ae06","datavalue":{"value":{"entity-type":"item","numeric-id":2773752,"id":"Q2773752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$043AB1EC-E056-4E6B-9F74-E98A1FB39237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f22cfcc1da06ae3d0a2bf7d846f01b79f14f8c1","datavalue":{"value":{"entity-type":"item","numeric-id":5678425,"id":"Q5678425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$25FB78F8-D5FC-4296-8C8F-ABD39210388D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90712b159374c96d8440cb870a686fa5cd675765","datavalue":{"value":{"entity-type":"item","numeric-id":362271,"id":"Q362271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0006a1c1cae82de1d6db1386ca159c0180b16e15","datavalue":{"value":{"amount":"+0.7641125917434692","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":"Q2336214$A447EA93-C5E4-49D2-AA3C-727E5F5043EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30de85ed16d9a2162c13d706232b2d7388026c5c","datavalue":{"value":{"entity-type":"item","numeric-id":2225123,"id":"Q2225123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"86785ab35e110106e689a27e61ea2488f9b846fd","datavalue":{"value":{"amount":"+0.7614133954048157","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":"Q2336214$92BE1771-4F99-4242-AC9D-D7471EED61E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e1eafc11d20b728fdc6253c94511f00e2d550f9","datavalue":{"value":{"entity-type":"item","numeric-id":611751,"id":"Q611751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9928826d21d480834652c68259d1f9399fca6d5c","datavalue":{"value":{"amount":"+0.748360276222229","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":"Q2336214$B4FC684B-385D-4E44-9CE4-8FC6C86038D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac8b021e3c809e504c58ab555a4b955def6a85e3","datavalue":{"value":{"entity-type":"item","numeric-id":4583790,"id":"Q4583790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be12c397e306bb152f0249f029225c541a2529eb","datavalue":{"value":{"amount":"+0.7129224538803101","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":"Q2336214$75194329-1572-46FF-8E3C-3FD56FA006D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97311b85d17b368c78a2ea6a875377f7441a650","datavalue":{"value":{"entity-type":"item","numeric-id":816219,"id":"Q816219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85192d09e8e3b94d5e3daa227840867c946428d1","datavalue":{"value":{"amount":"+0.7084521651268005","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":"Q2336214$6B9B3C4B-17AA-4634-ABCC-5D01CCBFACA6","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336214$4D312D1E-FD0A-4ABD-B230-4ED65FDAC06C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2336214","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2336214"}}}}}