{"entities":{"Q2120963":{"pageid":2131706,"ns":120,"title":"Item:Q2120963","lastrevid":57111867,"modified":"2026-03-26T16:22:02Z","type":"item","id":"Q2120963","labels":{"en":{"language":"en","value":"Formal verification of parallel prefix sum and stream compaction algorithms in CUDA"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7501976"}},"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":"Q2120963$28A846E7-870D-4605-947A-300E17D99702","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f915669b7c3b707bcb1491ae5819e10b8e205f25","datavalue":{"value":{"text":"Formal verification of parallel prefix sum and stream compaction algorithms in CUDA","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2120963$09B256B8-F649-4790-95B6-FF070EEBD30B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"551a54f3a08f8731996e12e16a70c34821e58629","datavalue":{"value":"1483.68091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$385E547B-1F5A-4255-9DC7-075069C071C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"75fb5243196322cb363d0d50557908676ddcffb6","datavalue":{"value":{"entity-type":"item","numeric-id":1698755,"id":"Q1698755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$B90EA0BE-D654-432A-B485-6796074384FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3772d5f7c7aac4e0fdecccd336d0d84f954a370a","datavalue":{"value":{"entity-type":"item","numeric-id":225075,"id":"Q225075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$78C1473E-4107-4F4A-A727-A00CDBFEEE36","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$61B7E5A0-BA20-4885-AC61-1BF2313419CA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61a1c46f4eee8fdcf70f057ed8a6245e7bfc68f9","datavalue":{"value":{"time":"+2022-04-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2120963$2AF475E7-626D-491D-8CF2-98F1BA836AAD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$F74E5544-05ED-47A9-8662-592AA8917568","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$0D094240-F526-4DB6-9DDA-0F155EC9EA46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$C574CC9C-1B62-454C-9FC3-FB611BB52577","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1de3565cfd3393000dd87ca545f95ff84d4c1446","datavalue":{"value":"68W10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$6D50A25A-042F-42BB-8F76-4A1E7CEB1C57","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"32eb527af093cb4b319fc6ef0acaa1fe7e7c80dd","datavalue":{"value":"7501976","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$2BB5C3F2-7DCD-4904-BEA8-E4423F554707","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ec9be654142adc63799990c0a53c05f55b53a29","datavalue":{"value":"GPU verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$1B7C333B-8578-4154-840D-41664DF72960","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d8fd07f1d71589a66f37ce986e7b2e4ddaba95ea","datavalue":{"value":"CUDA","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$4EECF0D1-7EB8-4DF5-96E1-1B7622A066CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$506EFBFF-F481-4D4D-BEF7-A01D27238629","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$23832127-F5AA-4F87-83FB-5ED29F411E42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf8087e1a6dd95e8dba2578397411d727991e9ea","datavalue":{"value":"prefix sum","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$C1E159BF-AAD9-4332-9EF0-9DF4399D0F1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec8d6a3bd500a476830034d5a0b76df6dd973143","datavalue":{"value":"stream compaction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2120963$88624871-3DB0-4AF0-8EB1-DBC516EB50A1","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":"Q2120963$7968FF5E-A3CE-487C-B5A8-FD5D559C441D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"493c4272f3e5f72c11a4ab08cd3c037673ba4268","datavalue":{"value":{"entity-type":"item","numeric-id":21766,"id":"Q21766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$948BA025-4198-4EF7-8F45-AB85755C5502","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aa3e15f325ed150088c4e410d88474936a717bb7","datavalue":{"value":{"entity-type":"item","numeric-id":23205,"id":"Q23205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$1822022A-D8A9-4883-BE57-70AE2C63273D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b8eb406da0bebd03f9ecb41f74e5badb7396eef3","datavalue":{"value":{"entity-type":"item","numeric-id":23206,"id":"Q23206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$20D47662-D0B6-42CA-A2FB-02C66AADBC3B","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":"Q2120963$EF85DDC6-5A09-494A-BB78-2516879FDFEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5abf8d928191e065723c7e79bd3c4074a4a7dd34","datavalue":{"value":{"entity-type":"item","numeric-id":40559,"id":"Q40559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$A2E362E5-493B-489C-86CB-56C81E9E4265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0b6896818a79869d8a15b52ee5a33caa6345b309","datavalue":{"value":{"entity-type":"item","numeric-id":1353390,"id":"Q1353390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$035A6F83-1030-40FE-89B7-A0BF9B3EDBC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8d8f10a93b523882fb84087e4f3ec3a91618d463","datavalue":{"value":{"entity-type":"item","numeric-id":24718,"id":"Q24718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$54DB6C37-F6FB-44B3-B3AC-B2F840072A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3a054baa4efca75beada6ac9f2f664c52ac32a0","datavalue":{"value":{"entity-type":"item","numeric-id":15791,"id":"Q15791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$59A5400D-8D3E-4652-A7BD-AD0E1FAB7939","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":"Q2120963$5E0D1615-3459-4C31-B967-5A44A819F6ED","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":"Q2120963$1DA9FD32-E911-427F-B8A3-BF974E8A0448","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ee81c7bdb3148948e6dacc6d7fda1e82211917b7","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2022.02.027","type":"string"},"datatype":"url"},"type":"statement","id":"Q2120963$7A65B8EB-B052-4675-B47D-10DBDB5DCC53","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b52b85aed05f5fe1631f12e03c52945e61b5b88e","datavalue":{"value":"W4214815337","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$915F797F-845A-42B1-B28E-3DDDA52B78A0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"91b08ff1b0d4539c99f6902ec8427b7b8b6cea46","datavalue":{"value":{"entity-type":"item","numeric-id":5276151,"id":"Q5276151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$4CC6217D-A7C3-4718-A0B6-6555BA83AC2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b6f86e69e4182fe9dee7c3758ceccac77217422","datavalue":{"value":{"entity-type":"item","numeric-id":4813391,"id":"Q4813391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$93E2CB34-9092-40C2-AA2B-7A5A4C68E3AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdb2be559bc16db998d32e6fa75898d44807cf88","datavalue":{"value":{"entity-type":"item","numeric-id":3934311,"id":"Q3934311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$1A5FB093-21E5-4AC3-B1A0-C3701C8CB5AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5260555482aaa3df778f28a6ed8ff34e7c741fe8","datavalue":{"value":{"entity-type":"item","numeric-id":5408435,"id":"Q5408435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$1D728148-0C1D-4848-BF3F-0681DE0873B3","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":"Q2120963$A938D5DD-3A47-46FA-A340-FFE96C1A4569","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":"Q2120963$C6796F14-381F-4C3F-945D-31BA1E53CA07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f4ce9103adcafab6054fd16b67fb4798a0430d2","datavalue":{"value":{"entity-type":"item","numeric-id":2037943,"id":"Q2037943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2120963$A8ECE68F-644C-4F0B-9A9C-FD06A192E61D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dab4eaf4e972eea5f9ace51fbaa63bd6b59a7077","datavalue":{"value":"10.1016/J.TCS.2022.02.027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2120963$D4A06FD0-7125-4C97-B0E5-39B5EC583922","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3b5555bd553a019fcdf079c7139717bb35a55ff","datavalue":{"value":{"entity-type":"item","numeric-id":1703009,"id":"Q1703009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb8100a7a556e300dfe67bbdaf5e978d93840bac","datavalue":{"value":{"amount":"+0.7469301819801331","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":"Q2120963$FCDB4CBE-0E74-4D6B-8881-475BB3B954F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f575379838e82e3e4258cf4e7d2e910c31967595","datavalue":{"value":{"entity-type":"item","numeric-id":5408435,"id":"Q5408435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e272a4c5322779715a276c0d09607908c3454b66","datavalue":{"value":{"amount":"+0.7331300377845764","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":"Q2120963$C47453A9-BEDF-493C-B71E-84F750019561","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba8f2d8d493ce04202060d636fc0f2c19e874e54","datavalue":{"value":{"entity-type":"item","numeric-id":5255854,"id":"Q5255854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb0bc9af052033c73f359163dfba4d0fd5101d91","datavalue":{"value":{"amount":"+0.7067325711250305","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":"Q2120963$9AF7BC00-3742-4495-84BE-140AD8503906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11e2b54aa024f9e69fd600b2d4e1d6296d79960e","datavalue":{"value":{"entity-type":"item","numeric-id":832190,"id":"Q832190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"800cabba85ce9ddbfc2ab6229cc84062a26c5b3c","datavalue":{"value":{"amount":"+0.6704542636871338","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":"Q2120963$5735E5B0-2009-48E0-9D69-0FBED63A71A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73f50693389a9759291aba99560def84abed668c","datavalue":{"value":{"entity-type":"item","numeric-id":2215621,"id":"Q2215621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a24925918b3fc95fdef77c7de6c9444b56315829","datavalue":{"value":{"amount":"+0.6697835326194763","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":"Q2120963$417E5A0A-9D2F-424E-BAD2-6E4664E49069","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":"Q2120963$DEDC128D-FD3C-46A2-98C6-17F9EDE4E889","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2120963","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2120963"}}}}}