{"entities":{"Q1004295":{"pageid":1006143,"ns":120,"title":"Item:Q1004295","lastrevid":66531375,"modified":"2026-04-12T10:46:16Z","type":"item","id":"Q1004295","labels":{"en":{"language":"en","value":"Mechanising a formal model of flash memory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5522249"}},"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":"Q1004295$FB461C5C-3A43-4ECC-A2C5-687F5EF90AF6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d19c2334bf495f56911b741f78da28bb6596126a","datavalue":{"value":{"text":"Mechanising a formal model of flash memory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1004295$E0722EBE-C647-4D55-861E-123932E28CB3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1bed55a7de7c1ee3f2e2e08c3eebaf6b3dc41ea6","datavalue":{"value":"1162.68387","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$47E1E87B-CBDB-423C-8966-C358F626F080","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bcc2517d7f29a0c99d871175f905014f619cab8","datavalue":{"value":{"entity-type":"item","numeric-id":539164,"id":"Q539164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$0B7A99FF-1EFE-4C77-9C75-21A20F1976D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a554aec36fc4a6a6f650f34c2516421d15681542","datavalue":{"value":{"entity-type":"item","numeric-id":1004292,"id":"Q1004292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$654B9E42-F18D-453F-A3E8-FC58F2A5A0F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9f50520e0dfe9b201fccdcdaf0b58056733a7110","datavalue":{"value":{"entity-type":"item","numeric-id":826051,"id":"Q826051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$BF3CDABB-5851-434B-8F1D-803885BAB5F6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$8262D1CC-6DA6-4FA7-B6F2-1BDFD527373D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5283b5da341717bddcc5514d88caea6acf73b725","datavalue":{"value":{"time":"+2009-03-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1004295$E0B301A0-5EF8-42E4-BE98-C6DF4F21CDA8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"06aaf19f4bbdd9676f0ed308701e830d30be51c5","datavalue":{"value":"68M99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$599601B6-A77E-4ED9-9AA8-EF0FCBBD9989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$034BD144-25C3-4A57-8EFF-D9B26B194F04","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f3718be20e1fdcfe911f0f6cb75c1c5c93373eb8","datavalue":{"value":"5522249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$62CAA4A5-E822-4557-9B74-87474B85EE96","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01a81bbd623405216ae4a5a6198d74c83f99ef2e","datavalue":{"value":"grand challenge","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004295$760199F0-64E8-4B68-9544-5884E7630AC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004295$34438A54-98BA-415F-B29B-B4D3B8C3DBD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6b59478b615c5ecf7215694d96ce7f716bdef8d","datavalue":{"value":"flash hardware","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004295$6F22E0A8-5AC9-4011-BEE8-3495D0333872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004295$B2301FCF-A6D8-49B1-95F9-58FB75E0BB79","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"272b1a9e09e3e0c648f0668682ab92d2e1d0ba63","datavalue":{"value":{"entity-type":"item","numeric-id":22226,"id":"Q22226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$E040D98A-6EDB-487B-9350-DE9778F6AD57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56183f18c1b7292025f517695163436751950f86","datavalue":{"value":{"entity-type":"item","numeric-id":22253,"id":"Q22253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$CC652B4C-7F04-4274-AD38-CA14E6E53741","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":"Q1004295$25883EAD-F977-4355-A4A2-49DEEFFD9142","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a5c81eb1bf6922d10855c53cb5b723796cf5b95b","datavalue":{"value":"https://doi.org/10.1016/j.scico.2008.09.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q1004295$7F27ACDF-925D-4588-9DA9-041CCB359459","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a270b9ab6ed3f9f65fa89596ed9d66732a9f4655","datavalue":{"value":"W2039336509","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$CA058ED5-9E94-4C2E-9958-1CF582D451A1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"097beafc05a97f0c4e666d19252acf96b5d4d7e6","datavalue":{"value":{"entity-type":"item","numeric-id":4417801,"id":"Q4417801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$7DE38EEF-A269-4A42-AF1E-A5A5ED68BE90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cc8eac40142f19f8a0519a932eaf2be5e0ba0e6","datavalue":{"value":{"entity-type":"item","numeric-id":2643130,"id":"Q2643130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$1E356EAD-6DC9-48B7-B536-84BC6C251DA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"398d44412f4db1adf75a492fb0d957243a508bb2","datavalue":{"value":{"entity-type":"item","numeric-id":3314973,"id":"Q3314973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$6EA90C06-40EB-4BDD-BFF0-655CC83C1DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a2c73ea523922ddf10917d5a60c3c9e9df84e94","datavalue":{"value":{"entity-type":"item","numeric-id":3995087,"id":"Q3995087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$6A9229EF-9DA3-43E2-A2DA-D64405250D51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bdd97facb3bf2a9c2c615550ed3786e6ac0e057","datavalue":{"value":{"entity-type":"item","numeric-id":3525137,"id":"Q3525137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004295$3A13AF8F-E314-44FA-A6BB-BA95C6F42F6B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2dfd67cd36ad68a55ec69db24b67acd312693723","datavalue":{"value":"10.1016/J.SCICO.2008.09.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004295$9139B462-D475-4061-8487-F3058866C78B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebecb0daa2d5e44555b21980270fc129076aea5d","datavalue":{"value":{"entity-type":"item","numeric-id":617930,"id":"Q617930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e9d1dfe8c7847684f45c3ca1a9cfd124c088b80","datavalue":{"value":{"amount":"+0.7307127714157104","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":"Q1004295$2115F3DB-1073-456C-B501-A8196225822C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ba83feba1be4951b2507336d05662777d195de9","datavalue":{"value":{"entity-type":"item","numeric-id":835773,"id":"Q835773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3de7834677c1c1b5c411aed4883791f8e2b1e88","datavalue":{"value":{"amount":"+0.6891762018203735","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":"Q1004295$065D4BB7-1ABC-4395-9ED4-B3529CD65660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e81c2ddeba7944cdb91d156797bab90cd6e16463","datavalue":{"value":{"entity-type":"item","numeric-id":5387859,"id":"Q5387859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa26d0b2cc73b655f705d56142440a80ea968f60","datavalue":{"value":{"amount":"+0.67670738697052","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":"Q1004295$64E7425B-6D42-4F45-9B25-8D19FA741DA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68eac9af76447b305b35b7b74fc1a0677e3894da","datavalue":{"value":{"entity-type":"item","numeric-id":1004296,"id":"Q1004296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fab304a2fd330a082e6ff4cac0fcb3f6477c695","datavalue":{"value":{"amount":"+0.6744334101676941","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":"Q1004295$8F3D521D-40B5-4837-8A82-477F0955E07E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7b2af2f6ec3f11430690519da20467a939786bb","datavalue":{"value":{"entity-type":"item","numeric-id":2643130,"id":"Q2643130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f1d0eac33ad93c5e1f8770be3feb33649a6adeb","datavalue":{"value":{"amount":"+0.6690844297409058","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":"Q1004295$4144412B-BC09-4EA1-B785-E0E6852CE54E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanising a formal model of flash memory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanising_a_formal_model_of_flash_memory"}}}}}