{"entities":{"Q432154":{"pageid":433921,"ns":120,"title":"Item:Q432154","lastrevid":61872486,"modified":"2026-04-11T02:14:04Z","type":"item","id":"Q432154","labels":{"en":{"language":"en","value":"Experiments in program verification using Event-B"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6052559"}},"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":"Q432154$39A9C3D2-776C-4B1D-988D-05539CBB4E86","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5e394ef94b300d0be94308f291a1b3aac6dc4609","datavalue":{"value":{"text":"Experiments in program verification using Event-B","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q432154$7ACAE0A9-7267-4776-AFFA-0CD8482F8303","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8e3bea67f68321b3412f4ce26e8620b428e2580f","datavalue":{"value":"1242.68067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$8181D49F-0094-4D0F-A821-068A63AC6779","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c3cadec2ef714e5660771f9ec0500ac9b16a25e","datavalue":{"value":{"entity-type":"item","numeric-id":432153,"id":"Q432153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$CCA7D660-9B66-4E53-BA20-918F51E74BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f18d6b5c094a5b54491448ffca180723301eb8f","datavalue":{"value":{"entity-type":"item","numeric-id":418180,"id":"Q418180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$367A5655-E679-4A19-84A2-78F4722EA62C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$11F55536-A4D1-49AA-BFF8-CF2BB726FA4E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d2ba0036895bc96d003b4a03286285e72e8ca4bd","datavalue":{"value":{"time":"+2012-07-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":"Q432154$1E116CE5-12E9-43EF-8D61-67CF19A8F654","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$7AFDB13A-4CF7-4D82-A76F-E98D2654F4CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$E0DD09C4-2F4F-4DDF-8D09-BA007AB33C3B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8fb2337896aa841705172c35d7073cfa6f145e5b","datavalue":{"value":"6052559","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$C54AED67-6907-4282-9F5E-2F044C31E4A3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"04ba4bf98dd124c8c2742b84b6fb188b54821857","datavalue":{"value":"Event-B","type":"string"},"datatype":"string"},"type":"statement","id":"Q432154$D6FD273D-EA2D-44EC-9F4C-70149A7110D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4481517714437ff63c836d4b49f0e1b5127461c1","datavalue":{"value":"proof obligation","type":"string"},"datatype":"string"},"type":"statement","id":"Q432154$BCEDBBFC-5035-43A0-9F51-2A6997C32266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0c1f8ecbef520debe4ed65c00c0dc97890c1127","datavalue":{"value":"proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q432154$A2BE2390-0F4D-4141-9DB2-6A26859E8DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6fa1689d1d75ad0f547929e7713d1802840e0514","datavalue":{"value":"sequential program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q432154$9C34A438-9725-46ED-A5E2-2CC077855E62","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3dcf6ea9ac65c890e0513ced8e4b0dde71e50b0f","datavalue":{"value":{"entity-type":"item","numeric-id":19141,"id":"Q19141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$3992C6B8-35CB-40AD-AF5B-75F51DB4E159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9189048b3936abda7e80b02cf829681849623735","datavalue":{"value":{"entity-type":"item","numeric-id":33628,"id":"Q33628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$72C5F6CB-CFA1-4FAF-AC72-6543B08B3809","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$9D9193AF-970C-4AF3-A11C-D99E2D9D5024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b09b080527cf0c7be3719338f59c9e92adea2d20","datavalue":{"value":{"entity-type":"item","numeric-id":19142,"id":"Q19142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$80333A7C-631B-4816-AB75-9CBB6AEF8FF0","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":"Q432154$DB02C05C-A8C9-449D-B14A-5C0EE328121C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e751138e8b150b28783c5a210048f6817120432b","datavalue":{"value":{"entity-type":"item","numeric-id":32511,"id":"Q32511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$12E9AC00-2131-48CF-8B6A-64F5B548CDD5","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":"Q432154$073B3841-657F-4058-AE76-521436B29BBC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"418da9c50153730f874ee2d7205c8b9a7141e8ca","datavalue":{"value":"https://doi.org/10.1007/s00165-011-0205-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q432154$30C3433C-4358-4914-BA31-ABB5A87F6DCD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ac2011b319de0339bc5baf9396fd9b399dbbae44","datavalue":{"value":"W2018217105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$0A84F636-56A5-4BBD-96B8-A760014784AB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae170f67b5a99f655b51707d2e6917e4913c4d7a","datavalue":{"value":{"entity-type":"item","numeric-id":4208552,"id":"Q4208552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$0981615D-1334-4E8E-A57E-0DF3BDF87FC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a64dbb7c90690de5fbdf0d30d9b861ec41a32a6","datavalue":{"value":{"entity-type":"item","numeric-id":3569584,"id":"Q3569584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$D20258BB-57FE-4811-9929-EB118EFC05F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9ebd97ebad7f6b6543ac93ba5957bb5f6f50160","datavalue":{"value":{"entity-type":"item","numeric-id":5703804,"id":"Q5703804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$888FD346-FBF7-4B27-BB09-2C1CA565B5FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2cc3dda6b80e001f719f188bb732541291d0e04","datavalue":{"value":{"entity-type":"item","numeric-id":3630170,"id":"Q3630170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$C9667992-584B-4373-A9F8-02B3CFAD9B49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"989ffcc992d1ac31e39a63758614d7ce6f35323e","datavalue":{"value":{"entity-type":"item","numeric-id":837527,"id":"Q837527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$EE4E149E-6721-4EFF-8C32-933FA183C577","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8e7b9da18e16cd970511c07ad5cdb803278d984","datavalue":{"value":{"entity-type":"item","numeric-id":5294155,"id":"Q5294155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$5F841611-EFAF-415B-9064-2651C0ED5DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$BA78E346-1A2D-4577-93D2-18F5C0E4B415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bdd8ac16bf352ecb0ae67e413a0bcc2dcb69557","datavalue":{"value":{"entity-type":"item","numeric-id":3814785,"id":"Q3814785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$C8BCBF83-7DC6-431F-8EA6-04E240937239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d18cf84bd49d4a3b35fa5f91415e3b2e495c135e","datavalue":{"value":{"entity-type":"item","numeric-id":4429922,"id":"Q4429922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$3852567C-A63E-4E43-9017-1C2F683F9645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05a8530cc8341477c91a6a458d8bc3eaffcd6c6d","datavalue":{"value":{"entity-type":"item","numeric-id":1251072,"id":"Q1251072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$A912DDB9-AA88-44C9-9236-EDBA96054029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$B78A6F12-B846-49AA-9E0B-14D3BE0F1AB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8773a932431602bdddce87be2ab32e5880c2dfc2","datavalue":{"value":{"entity-type":"item","numeric-id":5639351,"id":"Q5639351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$F999271F-8DEC-48D5-930F-D99091EDAA91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52e7bde04e2f5a48cbd5f85a32c09510e5669342","datavalue":{"value":{"entity-type":"item","numeric-id":3638993,"id":"Q3638993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$78631FE9-9CFA-4E54-A105-EBBB4D363979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"457e380a94d38fe11d0c65a23c879f3ba8179626","datavalue":{"value":{"entity-type":"item","numeric-id":3535369,"id":"Q3535369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$0BC667A0-BB3C-4DEA-A9E3-3D31F05C3437","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a98e1d68003b0040c15c163e66f3fd9578fb9386","datavalue":{"value":{"entity-type":"item","numeric-id":3997074,"id":"Q3997074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$30E9AC2A-A719-4665-8A09-65CC90254357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"992009231a3ccf90d1f1c83b557e5dfa4622a42d","datavalue":{"value":{"entity-type":"item","numeric-id":921907,"id":"Q921907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$51FB4D8E-55D4-4E78-A574-F37A73D51F9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768da93377b5dbe67ffc466d796d0d32932c2d63","datavalue":{"value":{"entity-type":"item","numeric-id":4301161,"id":"Q4301161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$0770D716-C72A-4A4E-B72F-A0A4A1B3D7F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2185699a6442c395c0dc5c871eedf78d99a845ad","datavalue":{"value":{"entity-type":"item","numeric-id":4940107,"id":"Q4940107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$685FB887-44B6-4D79-9A9C-BDF539BDFFE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc019e2b4d5136976181164b24b3484dcfaaead6","datavalue":{"value":{"entity-type":"item","numeric-id":4808845,"id":"Q4808845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q432154$BA4D3A80-4C1D-4F57-9B3C-D217E2237A54","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":"Q432154$6B470A4B-BBCE-4EE6-ADC7-4FDF4A203BAB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"118dbef27740c3cb0ab9ea8729beb70f9d73b442","datavalue":{"value":"10.1007/S00165-011-0205-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q432154$9A88C8F5-29C3-4DB8-AA75-B294775C0CBE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dc5e356a5e9f5403b0fd5200e4d64e9f97c50b4","datavalue":{"value":{"entity-type":"item","numeric-id":2994490,"id":"Q2994490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06122f938cd7303be108d5f26b84e06061d25e19","datavalue":{"value":{"amount":"+0.9050673842430116","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":"Q432154$6B0140AE-4BBC-48D6-93B3-D1AA0EAEEB34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d44462bd8f8015d07b19728aeb91786d6dc3f619","datavalue":{"value":{"entity-type":"item","numeric-id":5298560,"id":"Q5298560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9773c9c11a12b615583da0a1141d60329f8bf06a","datavalue":{"value":{"amount":"+0.8116365671157837","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":"Q432154$440D0550-2191-49CF-BD09-02A5B5A2D08A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aaaee7e1868aafa4cfa28e34e446781d99cfd67c","datavalue":{"value":{"entity-type":"item","numeric-id":3569584,"id":"Q3569584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"585365264b11b0b092aaa98106958e11289830df","datavalue":{"value":{"amount":"+0.7660226821899414","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":"Q432154$D7ABE101-169D-4441-A57D-94001E5F0A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"692e14a89f592d32d7f34c8de661041aef2a8828","datavalue":{"value":{"entity-type":"item","numeric-id":3608889,"id":"Q3608889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"457af0a0a231924037df12bc282af881c40c6bb3","datavalue":{"value":{"amount":"+0.7416399717330933","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":"Q432154$63BCD540-FE01-4F41-BC7E-F9FA818D76E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"643eb9fb141480ce9f216570d2730d531d156056","datavalue":{"value":{"entity-type":"item","numeric-id":3535369,"id":"Q3535369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0389fda817af5b94a9fbf8ddfc53c2313b49905b","datavalue":{"value":{"amount":"+0.7394548058509827","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":"Q432154$670BFB78-27A9-429A-AD4B-EA4B9EE8D1B7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Experiments in program verification using Event-B","badges":[]}}}}}