{"entities":{"Q5133670":{"pageid":7163242,"ns":120,"title":"Item:Q5133670","lastrevid":53868473,"modified":"2026-01-25T20:44:35Z","type":"item","id":"Q5133670","labels":{"en":{"language":"en","value":"Formal specification and verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7272524"}},"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":"Q5133670$BEB09A68-ADF2-4E2B-860A-E044D142A1A1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"77d04d95f924e48f17b26d6f419a2e024a2ca03e","datavalue":{"value":{"text":"Formal specification and verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5133670$96E2086C-C0B4-431B-B265-26DAB5F2E8F5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4f39437e9058243757f28749c4660fbdc8d78a2a","datavalue":{"value":"1455.68016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$0D8C901F-E12D-4A9A-868B-ECA7FEC9E82E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"99eb3910b3040a0f73270f76969203d5864e3f8f","datavalue":{"value":"10.1145/3335772.3335780","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$C01526F3-74DF-4D86-8E2D-33705617063A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5a4b473513180cf93e4a8c86844a2c4dad9ce336","datavalue":{"value":{"entity-type":"item","numeric-id":820130,"id":"Q820130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5133670$EAD05AC3-ED01-48C5-9CAF-E77A75C94C07","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7a5e7eac8bd68f1b852d9821d1c90130dc221370","datavalue":{"value":{"entity-type":"item","numeric-id":5133663,"id":"Q5133663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5133670$316F4B3D-D68F-4538-8402-09404D229965","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d9f22268837797e046dca0302ad58b944858f292","datavalue":{"value":{"time":"+2020-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5133670$063CD060-D188-49C5-A108-738C9BF063ED","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a00fe7e8d5c1f49ffe8a44bf4f2dcc306d52113","datavalue":{"value":"https://hal.inria.fr/hal-02387780/file/lamport-book-only-formal.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5133670$79415020-EE5D-4E4F-AEA2-F12FBC2F821E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$E1C9A2CF-1A5A-4849-A5EA-45A663D20762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$977D85C8-1929-48E1-95CB-677C999278F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$51FD456B-42E3-4D29-BFC8-1A076EE663E8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c81008d738acee638a708d9aa13ccf8f1b5b9b7","datavalue":{"value":"7272524","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$9C7FB3CF-576B-47FC-8C20-6E67E53D6DB5","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":"Q5133670$FE243A0B-E60C-4C6F-B1CE-E4216B2E5EED","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a77dc67e38327ab0ca98b4b3c934fd91d6b920be","datavalue":{"value":"W2980032873","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5133670$749C7EFE-94CD-42BF-9840-F68208272C88","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b603f9a2204ddc0915373daffeaa615ab14400a","datavalue":{"value":{"entity-type":"item","numeric-id":4490359,"id":"Q4490359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00be385ced9f1282ecaf01c11216dea45b8f45d9","datavalue":{"value":{"amount":"+0.7859379649162292","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":"Q5133670$02B90C44-45FE-49D0-A124-7DCB0600B646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"400daeba872d01174f63c096f657979ecca7b403","datavalue":{"value":{"entity-type":"item","numeric-id":2281632,"id":"Q2281632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00be385ced9f1282ecaf01c11216dea45b8f45d9","datavalue":{"value":{"amount":"+0.7859379649162292","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":"Q5133670$CD69404B-2EE9-47B8-A664-071B772BF677","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"074fc49899c2af0bbba15842ddb799ce0c6efe54","datavalue":{"value":{"entity-type":"item","numeric-id":4885875,"id":"Q4885875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d582ed03263ee33c7764d85d414eefef73de4c8","datavalue":{"value":{"amount":"+0.7633335590362549","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":"Q5133670$CD65C823-6360-4442-B4F0-B0EABEAFBDBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e3ba249465de83fb5116831d036f45a44bd8d46","datavalue":{"value":{"entity-type":"item","numeric-id":4938420,"id":"Q4938420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f306229c7b0090469b672efa2d3537f46a75e09","datavalue":{"value":{"amount":"+0.7629793286323547","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":"Q5133670$8D3C284C-24FE-42F8-9AF2-78B0183551AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"372b69ab1939ba06752a09e11e53f8645776f9c8","datavalue":{"value":{"entity-type":"item","numeric-id":4017600,"id":"Q4017600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0236d1fe5390cd45476d96865e18925e39e314a6","datavalue":{"value":{"amount":"+0.7602583765983582","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":"Q5133670$223EB9E2-BD51-434C-B071-4CAD2C5EAB09","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5133670","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5133670"}}}}}