{"entities":{"Q877828":{"pageid":879676,"ns":120,"title":"Item:Q877828","lastrevid":65062626,"modified":"2026-04-12T00:03:57Z","type":"item","id":"Q877828","labels":{"en":{"language":"en","value":"A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5149171"}},"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":"Q877828$B0E54725-2D00-4439-A5E0-9E27080741D8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9b415e0f1c48c83c91ccedb79bff7136c34465a2","datavalue":{"value":{"text":"A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q877828$D3525893-4032-41F9-9F03-1992ACC2F3EE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f105843b6bf8fa21057a82c2a7b874f22d974a7c","datavalue":{"value":"1113.68091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$8F63B1A6-0916-4040-8B6D-D728C7A0EE2A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"07ef5bce62b88cfecff16603e8667fcc383b0d99","datavalue":{"value":{"entity-type":"item","numeric-id":479822,"id":"Q479822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$2B4BCD70-5B9D-4596-944D-2A882DECA351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca0d8ddf7b0d38f9b642c89def3a8f0d1cf2f6df","datavalue":{"value":{"entity-type":"item","numeric-id":877827,"id":"Q877827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$F76409A5-5D0D-4D45-9EE3-6B023F2BBBB1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$DC7E2A71-D18B-4A92-BBAC-9ABE925F7947","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"705732f6c443403985df27568b16305b8e45450f","datavalue":{"value":{"time":"+2007-05-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q877828$938DD333-1546-471A-9C30-477504A2A20F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$24003C19-0640-40D1-845F-71AC26123562","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$90F1988F-F9D4-4B4A-B2DC-0C3929FF53B8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3e8c97b7030ae89224439ca75e5a36115a00291","datavalue":{"value":"5149171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$B079A587-895F-4A32-9498-28A89C407334","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ea4a5639c3a57c4944b22d6c95c581eab656a58","datavalue":{"value":"term-level pipelined machine models","type":"string"},"datatype":"string"},"type":"statement","id":"Q877828$57E927C6-CD0C-455B-8C50-99A7F9BE3822","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7a35a47cef9f2baec76c3bfc2bf8f6032431cb1c","datavalue":{"value":{"entity-type":"item","numeric-id":16827,"id":"Q16827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$9304FE36-585C-4695-99BD-8D405B087144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f705e695e5daf5c1a4b07b9d249dfa9eda3d87b3","datavalue":{"value":{"entity-type":"item","numeric-id":16613,"id":"Q16613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$D31F4211-E3AD-47DE-906D-1D45262B7238","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":"Q877828$835F02A2-7D96-4C89-95C7-09CE2395B538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$1039C332-5863-4999-B1D4-3918E96617BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$60562C0E-34FD-429F-8D9C-5E742CBD3117","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":"Q877828$E0A26AE0-D7B0-420E-80AD-524658B307D6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1ef515e9ef459c44e3caf843ad8c4f54f5b863d9","datavalue":{"value":"https://doi.org/10.1007/s10817-006-9035-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q877828$8AC1496E-841E-45EE-8ADE-66E2EDE34D00","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bbfb421c542f2d5a2cac2d91e036c29f4b5962f5","datavalue":{"value":"W1992409933","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$8926C272-D219-4A40-940E-9FDFAF5136BA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"09caa7beb8d3eefa06ce47df5edefd82c31c123b","datavalue":{"value":{"entity-type":"item","numeric-id":2729088,"id":"Q2729088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$0FF34812-3298-4E55-82D7-AFB4F6840235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f484c50ffc3ac7b39ec0997882c937f455ca39bc","datavalue":{"value":{"entity-type":"item","numeric-id":5716555,"id":"Q5716555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$BD02F0BF-1D5F-424C-84C9-84359FF076F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7eb3e97929024d2ee37616602a13d3244533bbb2","datavalue":{"value":{"entity-type":"item","numeric-id":3835049,"id":"Q3835049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$3FC04CE9-75DB-4BB6-A6A3-131C39DECFBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21ba3964561c6339cb3ba43543aed014dc7a60d0","datavalue":{"value":{"entity-type":"item","numeric-id":1123183,"id":"Q1123183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$4A564280-958D-4330-A111-46C5CF3E2055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7cc71ec79ab682a2437b8f7373d5a54c44417af","datavalue":{"value":{"entity-type":"item","numeric-id":4818814,"id":"Q4818814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$9DB9499A-F094-4ADE-BCA7-0E1BF2053E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e242557b370e70ca22794bd752775ec0bac8856","datavalue":{"value":{"entity-type":"item","numeric-id":4804887,"id":"Q4804887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$1D7063E8-A21D-4617-ACC4-C4E6169E80A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da96dfa99f70c6b2b69c48b417a516b8fa851830","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$A0828265-27BB-4BAD-BBDA-329A740F049B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94d35ac0fdc56d78fa0b05b08a404b4c5aa1732e","datavalue":{"value":{"entity-type":"item","numeric-id":4817532,"id":"Q4817532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$252FEE47-517F-46F3-8762-164616D96DB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6115a87f8666aec32f37456650912a5a8315beb","datavalue":{"value":{"entity-type":"item","numeric-id":1059054,"id":"Q1059054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$91E40EF4-2E96-45BA-8A2E-EFEA995C7EDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"187ac37ffc9a6cd026f976080d84a63a34f01dbb","datavalue":{"value":{"entity-type":"item","numeric-id":4427901,"id":"Q4427901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$20ACC79E-753F-47AF-8EC7-EE0FE1E20E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"991ac21545d55e33054a32161d4696ec2df1036c","datavalue":{"value":{"entity-type":"item","numeric-id":5312932,"id":"Q5312932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$4C6A2A68-0DA5-4B10-9C88-BFF47D8B8104","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87f7bcfffc49742b219cd84a695191ca8beef7cd","datavalue":{"value":{"entity-type":"item","numeric-id":5734774,"id":"Q5734774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$638C3439-B871-4A0D-A95D-7A349635A0F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15d86757aed588d819db82dae30fd8dcbf504d44","datavalue":{"value":{"entity-type":"item","numeric-id":5897075,"id":"Q5897075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$57483D52-0DCB-4F6A-988E-6D0F8F0E1F7C","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":"Q877828$7AE00700-EF62-4F2B-9592-E2509636E7A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a692c084bea02080372f65e7b3d4b4fadbd2e807","datavalue":{"value":{"entity-type":"item","numeric-id":5897074,"id":"Q5897074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$8C677CFD-2AFC-47FD-A9C1-01E0C18E6718","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6d45d62552afebf5e9758a073f084970fe802e7","datavalue":{"value":{"entity-type":"item","numeric-id":1290337,"id":"Q1290337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877828$5BC73F02-C6EF-4AFE-AE92-319CA3FB5393","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":"Q877828$EE77D277-C189-4F3D-81E7-908DAE572EFB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ab33f5a36f1f0ef4a4217ea1a9a71d8a49b8b189","datavalue":{"value":"10.1007/S10817-006-9035-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877828$2FA98165-22AC-4000-AD52-9A1286FF22E7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20f4c170b79e09ad78a840a7aaadd1f881f54a7c","datavalue":{"value":{"entity-type":"item","numeric-id":5312915,"id":"Q5312915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9389cb52d0af769f7b481cd18d3b1a99cf20321b","datavalue":{"value":{"amount":"+0.782039999961853","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":"Q877828$7DEBA636-591E-4EAE-8474-73B2DAA38DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69ee81091b55b0966f4b674e7cf88a8a5bbdec60","datavalue":{"value":{"entity-type":"item","numeric-id":5899157,"id":"Q5899157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78cd629c9714e6fb85685c44f195fb211968de26","datavalue":{"value":{"amount":"+0.7466548085212708","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":"Q877828$54050027-AFDE-4404-867B-B8E0F6189179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7cc02d0ff6261e63ae865751d8ffc8ed4d82af1","datavalue":{"value":{"entity-type":"item","numeric-id":5394618,"id":"Q5394618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4ce61dda7a6bce2de2760237cffc3e4ab4b4998","datavalue":{"value":{"amount":"+0.721736490726471","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":"Q877828$D35914A5-2719-4AFD-B448-7C71932AD799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7b97148ac17a4158636b28a0c57c327ff2aabd3","datavalue":{"value":{"entity-type":"item","numeric-id":1426941,"id":"Q1426941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de3d7b3a6ce86355f6d57d44ea09e580e4148149","datavalue":{"value":{"amount":"+0.7193588018417358","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":"Q877828$7E570B54-B8F4-4D1A-9761-2A38C7B5B33A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71537978e6eba52208eaf0885350004f62bf6048","datavalue":{"value":{"entity-type":"item","numeric-id":4364538,"id":"Q4364538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"055cf20926641b52de481b83902714ee13c0aade","datavalue":{"value":{"amount":"+0.7185288667678833","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":"Q877828$AE6B817F-62F7-4BF7-B28E-DF495AA8F058","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_framework_for_verifying_bit-level_pipelined_machines_based_on_automated_deduction_and_decision_procedures"}}}}}