{"entities":{"Q1426941":{"pageid":1437681,"ns":120,"title":"Item:Q1426941","lastrevid":70377129,"modified":"2026-04-13T14:22:04Z","type":"item","id":"Q1426941","labels":{"en":{"language":"en","value":"Formal verification of a complex pipelined processor"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2057417"}},"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":"Q1426941$4C0DC25A-E00D-4FCE-8B8A-E8E23A6A5648","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8a5a40ec443efcfbc55de1401cbe7f7904c50304","datavalue":{"value":{"text":"Formal verification of a complex pipelined processor","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1426941$88912EDD-541D-4ED7-8667-FA900F74A05C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bc0e98d233ca1a68cd7fed9ae9156dd2f26b9da8","datavalue":{"value":"1057.68062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426941$A81ABA37-B77B-437C-9F37-CB826A780178","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b9fda306348b49db8dc5a3a247bfd79e24f47ae3","datavalue":{"value":"10.1023/A:1024716316140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426941$986F90B4-40C6-4FFB-A1EA-2A4D94F98E50","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e636eb034f2f1ee54df415dc4165e8e6fadb37f0","datavalue":{"value":{"entity-type":"item","numeric-id":1426940,"id":"Q1426940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426941$E0161DE6-D3EB-4EFD-9CD0-A2F2BDC8D3F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6bb25cd5bff61dd98c69faa32322d3d5f5b3963d","datavalue":{"value":{"entity-type":"item","numeric-id":239161,"id":"Q239161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426941$0283AED5-DF8D-4526-B351-C0713FDF864D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"98daa176291d3f31b004bb8af3845f694af2604d","datavalue":{"value":{"entity-type":"item","numeric-id":1095644,"id":"Q1095644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426941$A1859F34-5C98-4AD5-83A6-F3D7CBF0CD5F","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":"Q1426941$1A60C067-B46D-4E4F-9CE2-8D20BA50B9FB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"47829e28918d048336111de08a0f0c93aec92d0a","datavalue":{"value":{"time":"+2004-03-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1426941$BE6D1ABC-5A08-4E82-83F1-8B1202AC4AB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426941$09CE5B77-25F4-4E79-93F8-85DBEA1091F8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"70f21c5092fed8dcffcbd2f2042cdd1ac37865ae","datavalue":{"value":"2057417","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426941$56F7DEE5-C93A-4C3D-A0DC-5FD25702121C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426941$F95881D1-08C2-45B5-8DC2-B6ECE820A879","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"80d1ba463693a4280b486b9fc22220770148aec1","datavalue":{"value":"processor verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426941$1F4DD141-2B03-4C7C-88D7-0861EE523245","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b99467a5e2d06655ec5b8c1219b344ee80423951","datavalue":{"value":"completion functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426941$13CA6FBE-B9C5-4E0F-A444-DC7BE8F39E0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426941$72FD70EF-D294-4FE3-AAB3-6737C9600253","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":"Q1426941$9F203DC5-E7E9-40D0-A690-C18E7CC0E722","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":"Q1426941$1A3AB62B-B179-4027-A2F8-10D1F4223B2A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"22aa667355577cf729b81505b8a7f7878e126ac8","datavalue":{"value":"https://doi.org/10.1023/a:1024716316140","type":"string"},"datatype":"url"},"type":"statement","id":"Q1426941$D390B1E8-2C09-43AA-A9C7-19186ACFB2DF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"62c64f63333d88a74e99039246cb058a838fca23","datavalue":{"value":"W1861031206","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426941$54EFCE28-4625-4ECD-89AE-77D6D41FCF3C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abb8af04e508d3d612db58da55932aaad94210b3","datavalue":{"value":{"entity-type":"item","numeric-id":4804904,"id":"Q4804904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a762aeb338067da093434b7a24b2a922f3fa177","datavalue":{"value":{"amount":"+0.8284633159637451","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":"Q1426941$2CA74D7D-295E-4232-9F3C-DA4ED1DF3B4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a10e85e7181590b50a29ad123b345e2886469d86","datavalue":{"value":{"entity-type":"item","numeric-id":2754092,"id":"Q2754092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4533019a95f84902e5f570fcbdb4e0fe912e61a2","datavalue":{"value":{"amount":"+0.8239912986755371","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":"Q1426941$0EECB2C6-A2E4-4A0A-8A02-75217971FA2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11caca4f7a7cde7700d075ffa6c8f3b558c07bbf","datavalue":{"value":{"entity-type":"item","numeric-id":4817532,"id":"Q4817532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"608699e0f96fe7d11626c019809f25408c7fcf33","datavalue":{"value":{"amount":"+0.8140572309494019","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":"Q1426941$CCB88756-86EC-4F94-86E2-533FA57EB53A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb57dac5e9733bbbaad6a936013c102dabfd2939","datavalue":{"value":{"entity-type":"item","numeric-id":4419604,"id":"Q4419604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e85bcb926bdff77d2fdfa5bce09cd403db7e7742","datavalue":{"value":{"amount":"+0.811176598072052","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":"Q1426941$C8B4C3E8-3FD7-4721-BDBE-B9C6D7E0E967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37fbafcccaf439e1f7cb33ef651e7a286c92fdd6","datavalue":{"value":{"entity-type":"item","numeric-id":1604722,"id":"Q1604722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d404876b4ba11c93c798748a7a846367b367ec0","datavalue":{"value":{"amount":"+0.804797887802124","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":"Q1426941$8F44C5C4-A5BA-4638-8CFA-0277CE5470F8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal verification of a complex pipelined processor","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_verification_of_a_complex_pipelined_processor"}}}}}