{"entities":{"Q1004294":{"pageid":1006142,"ns":120,"title":"Item:Q1004294","lastrevid":66531366,"modified":"2026-04-12T10:46:15Z","type":"item","id":"Q1004294","labels":{"en":{"language":"en","value":"Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5522248"}},"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":"Q1004294$C6105793-AF81-412F-8338-EFCD0EB12DFA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e5f5c03f70b43bcce0f9097153e82d28017ecf1e","datavalue":{"value":{"text":"Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1004294$B36D10CE-A347-4BB3-BC4F-2E8672820B1F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa1e5de54bfe7b7bf1949e4928ad3e657b5d1667","datavalue":{"value":"1178.68527","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$B072448B-A4E6-4357-B876-7C40834A0EEB","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":"Q1004294$ACA0AEDC-5DBE-4249-9DAD-997738960FD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9872a9bc5860d78ec0b674d6c3c865c8a943bef5","datavalue":{"value":{"entity-type":"item","numeric-id":1004293,"id":"Q1004293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004294$8FF3B175-595B-4E9A-9E2F-451E9A27608E","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":"Q1004294$43B21F00-74C0-40BB-92E8-72698C36E9C6","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":"Q1004294$93A2412A-71F8-413E-A053-E46137EE5180","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":"Q1004294$EE97ED6D-2622-4E85-91F8-5392AC506F81","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$C1767304-39F6-482E-A3D6-7D23F221A746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"517ace4a4f9c45a5475b4a8927a567447dbdb293","datavalue":{"value":"68N99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$8A2C17B5-72F3-4CD1-9767-B5C796E5EF73","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c3d802d364ff625fdd5ad164938d75c464d5ac32","datavalue":{"value":"5522248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$0C5A47DA-FFEB-4026-93E7-4355B753464A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb934f4ae005e3c3b70d2b7dfd119ffcf7a210c7","datavalue":{"value":"grand challenge in verified software","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$19F6CCDE-C2A4-44B3-9810-C08BFA88452C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd5e97b9e251e99e4762e2cf453629c9807a59bd","datavalue":{"value":"IBM CICS","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$2A9D7814-DCFE-4AD6-AF0A-0576A58F2DDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"127282cd7c24626ba4913e02f82ef416038e00dd","datavalue":{"value":"verified software repository","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$C1CA9C36-2EB6-4D86-905C-97EE012B4BC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9538394f74932a8eca06953b8df0d498142a3a6a","datavalue":{"value":"Z notation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$DEAB1851-7FB8-49C6-AAC8-50233432F0EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcf0a890e8e3065206f385fec8f2dcdd0df906f4","datavalue":{"value":"Z/Eves","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$C7ADB4EC-A125-419F-A59E-B62A4D550CDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a891b3602e9f929e8f968f246ae0990cc6b55b0","datavalue":{"value":"file API","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$6132990A-E7B2-4326-B87D-C217CFB46D6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"590dbff0fc1606926dfa7be7cb7ff6276af65432","datavalue":{"value":"mechanical proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$B5350092-C168-4828-8B2B-5BA8F3BF9CE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$09F2D4B1-602B-443A-A393-2DBAFD20F11F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6e2713a267b42b739e573135c3d65c5be2ef70e9","datavalue":{"value":"verification challenge problems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1004294$369A621F-8B25-40C1-989A-9E50FC10E7CD","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":"Q1004294$56A592F1-502A-49F5-93BE-7FE11D35C20A","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":"Q1004294$2591BE61-8795-48C3-BE04-E90394627305","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":"Q1004294$B4CF5501-6A19-4E7C-B9E2-96315B9D0E15","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"55e75b5e546cc0c5c2edc27ca4ac59279f52ea4e","datavalue":{"value":"https://doi.org/10.1016/j.scico.2008.09.012","type":"string"},"datatype":"url"},"type":"statement","id":"Q1004294$BAA83EA6-68B9-48DF-846F-CC81DC1D54D2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a654baa9049256c315561c51d090eb31dc866429","datavalue":{"value":"W2050774808","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$9089C793-F80F-487D-A444-14FC4DB51B61","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ad56a6334989730feeee1ae01af34f0f73a349ec","datavalue":{"value":"Q126190056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$75049A04-1565-446C-96BD-B4080A9B8747","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"38f7a668766da972033a6c18555fff3129df0572","datavalue":{"value":{"entity-type":"item","numeric-id":2432233,"id":"Q2432233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004294$ED830203-B7AE-47E2-9C61-DBE1FFA1DA8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d24bd6400a856d5e4ce80af17b8396e9070d82c8","datavalue":{"value":{"entity-type":"item","numeric-id":4845488,"id":"Q4845488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1004294$04237CC4-4F40-4170-99C5-798617C5852C","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":"Q1004294$55666842-DFAE-4255-B211-7A27D1BFEB9B","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":"Q1004294$D1916DC8-B076-43AB-96D8-C46E7C7E4A2F","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":"Q1004294$85B4EDD6-F312-41DC-AB32-418B18D477AF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f487596a91126ae306db08c542c01491ecfeb8c3","datavalue":{"value":"10.1016/J.SCICO.2008.09.012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1004294$9C2A5539-7074-4280-9653-9EDAB1145E93","rank":"normal"}],"P1643":[{"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":"5d7fd2e8f85ba2b19d92e1b8c2fae17142dd5fa4","datavalue":{"value":{"amount":"+0.88482857","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1004294$F6E6022C-EB6F-45CB-929D-C2FC65B964D7","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":"ef38b53314fe0cc218a2f4b0a3664ab529d5a8d6","datavalue":{"value":{"amount":"+0.8535683","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1004294$F611CD27-0CDF-4DB7-8EBB-5C7D29E4AE36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ede137086f685454b547e4c101069ed16a05c0e3","datavalue":{"value":{"entity-type":"item","numeric-id":5166713,"id":"Q5166713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b43979bf755741d77dd674556351f532108825dc","datavalue":{"value":{"amount":"+0.8286407","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1004294$10964F9E-7B01-4E69-89E7-F333018328D7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verifying_the_CICS_file_control_API_with_Z/Eves:_An_experiment_in_the_verified_software_repository"}}}}}