{"entities":{"Q1004296":{"pageid":1006144,"ns":120,"title":"Item:Q1004296","lastrevid":66531384,"modified":"2026-04-12T10:46:16Z","type":"item","id":"Q1004296","labels":{"en":{"language":"en","value":"POSIX file store in Z/Eves: An experiment in the verified software repository"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5522250"}},"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":"Q1004296$5F92EC31-0549-48BC-B50A-9390CB032A6F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e35520cce7460be3fc9299428c13aa0edaa33132","datavalue":{"value":{"text":"POSIX file store in Z/Eves: An experiment in the verified software repository","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1004296$6F3DA04F-C70A-464B-9717-F74B97C0168D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"38f4757b1d3d2002d3d8af7a2a25839635813a25","datavalue":{"value":"1162.68388","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$97E6ECB8-1EE2-4009-918A-CB86039C1F57","rank":"normal"}],"P16":[{"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":"Q1004296$E94828A1-BE48-43C0-B1CE-7F35481DECD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"70c757fff92022da750d5c20861a8c8f3fac01ce","datavalue":{"value":{"entity-type":"item","numeric-id":352026,"id":"Q352026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$A7F6170F-3476-472C-8238-0AE7DAA3C3C9","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":"Q1004296$E014086B-DECA-4650-A675-E16DD10D740D","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":"Q1004296$CC5D02C5-ECDF-4521-8AA3-F37BB3360E08","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":"Q1004296$D314D8FB-61C9-45F1-8270-4FD66DFECCF5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"06aaf19f4bbdd9676f0ed308701e830d30be51c5","datavalue":{"value":"68M99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$3B714743-855C-45C4-BF55-6A80D09982DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$CC01E443-5DD6-4A9E-802F-286C0F2138B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$FEABC00A-DF6E-4F5D-9B87-A43A59CDF4A0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c65f386c451c5c9cf798a061662e09e37d66a8e1","datavalue":{"value":"5522250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$7E2EA6E6-E688-4881-A051-5609C989220C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01a81bbd623405216ae4a5a6198d74c83f99ef2e","datavalue":{"value":"grand challenge","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$B5669C41-94C5-4E41-BD58-ABC7792B4AA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$798D2573-063C-46B2-9D47-51EC2DC13E2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21884761c7d22547050d436712a82ffc85a4cf93","datavalue":{"value":"POSIX","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$98C92990-D6DA-4900-9A2B-8FF3B330F6C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e720cb2d15b89f1fd5730906233db5039b6ccf4","datavalue":{"value":"file systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$262C6D80-5A80-44CB-BA20-67159F7705FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a422a645a6aa51e238248983a076824af489978","datavalue":{"value":"flash memory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$0DCB6544-16BE-48A2-ACF3-35303C669B44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004296$C8042B27-085D-4D5A-8FBB-61B2C703E7F1","rank":"normal"}],"P1463":[{"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":"Q1004296$15D0D383-A8B6-4B0A-9A68-BB11E092ABE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"beb205139d0971fca32ffa61e5b55aaac31a7181","datavalue":{"value":{"entity-type":"item","numeric-id":16768,"id":"Q16768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$BC9E74F4-9C5F-4FA5-879A-3DB5179B435C","rank":"normal"},{"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":"Q1004296$D65E181D-82B3-4EB3-809D-D453EF6DDB5F","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":"Q1004296$A5573003-D6F9-4C52-824B-3A8C515E9868","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"015a3020b7b047ebed9d06f5f7e8e8e123e1e8d5","datavalue":{"value":"https://doi.org/10.1016/j.scico.2008.08.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q1004296$CB345D87-7823-4256-AD70-D33541CBB0FF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"39b889df4fd608eba9a7f4bd29f3362f91fc94ac","datavalue":{"value":"W1982220991","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$6A9029B8-0E3A-4780-A3B7-BD187EF2C087","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"399da09cb148df17bed8bb8c65504e4a8b89345d","datavalue":{"value":{"entity-type":"item","numeric-id":1004296,"id":"Q1004296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$1D346E4A-BDAA-47FB-AF1A-3EFF66660312","rank":"normal"},{"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":"Q1004296$C8439768-AE5D-4031-9D0C-252A417C395A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e01b51a15cfb4a137078371d8e4ef36fd1bf9baa","datavalue":{"value":{"entity-type":"item","numeric-id":4808693,"id":"Q4808693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$AFB461A2-F60A-4105-9DC1-D8F4B8A537F4","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":"Q1004296$E91DCE97-BA41-4DE4-8B5D-AA6C15F85F11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de2147fedd3b575c8a39b15b3764faa17a12a2fb","datavalue":{"value":{"entity-type":"item","numeric-id":5256772,"id":"Q5256772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$D5D82519-755B-45D7-B440-B9FA941DCB97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"695a4e35247aa2e5c3bbb7784969e9d49ca24ac9","datavalue":{"value":{"entity-type":"item","numeric-id":3526934,"id":"Q3526934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$29E2941E-FC23-4CC0-9D7D-4F434B5037CC","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":"Q1004296$5B1EDD66-4374-4EE5-8C6D-E11082F491E7","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":"Q1004296$0FA66F79-942A-4CB4-96C8-92BF5DDA46B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc22454e59c42890989b223acb2a7da42f9239c9","datavalue":{"value":{"entity-type":"item","numeric-id":4301167,"id":"Q4301167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004296$548B7E98-DE67-48FE-AB03-7A9F1156C773","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":"Q1004296$286BF108-5376-4245-97D8-69A866F90738","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1927a38a3869a2a450ba66a068329d0eea6614d2","datavalue":{"value":"10.1016/J.SCICO.2008.08.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004296$D508A3E1-A520-4E36-B35C-BF86D4EEA81F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f58ff1f9ae75810d09cf3b4fd11b33aa271dd92","datavalue":{"value":{"entity-type":"item","numeric-id":1004294,"id":"Q1004294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d5cd79342e948449b38a1fdcc136d510115b201","datavalue":{"value":{"amount":"+0.8078115582466125","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":"Q1004296$077C9913-B99A-4A09-85DA-A5132D44D22C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7833298f7b4bcee38aad70caa6bfc39f468bd1e5","datavalue":{"value":{"entity-type":"item","numeric-id":2432233,"id":"Q2432233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"007c34bc76e4b2bb8965e287ba1275070108d360","datavalue":{"value":{"amount":"+0.7498462200164795","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":"Q1004296$37A14CEC-0EAB-4625-ADEF-CBDDDB6FDC72","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":"d8ef73fdc78bcc3d70f728e7be3e1800784d88cf","datavalue":{"value":{"amount":"+0.7060974836349487","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":"Q1004296$1CD2ABD6-CFBE-4DD8-AF7B-FE5D07B98168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d74575d9dda513fb4dbf73a5150199c97ecf843","datavalue":{"value":{"entity-type":"item","numeric-id":432156,"id":"Q432156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"217ea6e69f8b4173a9d624c2b89e297a5cdf03e6","datavalue":{"value":{"amount":"+0.7004528045654297","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":"Q1004296$9962EA9A-6B41-40E7-AD56-2D437795C9EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9711f31f60a375f78ce514ac85e85e6989641b4","datavalue":{"value":{"entity-type":"item","numeric-id":3525137,"id":"Q3525137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71c84dca1e599ee6ad149577898a6614720c0459","datavalue":{"value":{"amount":"+0.6968677639961243","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":"Q1004296$C7F185A8-9895-4EF9-A941-6EBEFEE80694","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"POSIX file store in Z/Eves: An experiment in the verified software repository","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/POSIX_file_store_in_Z/Eves:_An_experiment_in_the_verified_software_repository"}}}}}