{"entities":{"Q2829268":{"pageid":2840006,"ns":120,"title":"Item:Q2829268","lastrevid":52660112,"modified":"2026-01-23T05:18:39Z","type":"item","id":"Q2829268","labels":{"en":{"language":"en","value":"A framework for the automatic formal verification of refinement from \\textsc{Cogent} to C"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6644752"}},"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":"Q2829268$EC7D4969-B5FF-427E-BEC1-9F9185106337","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cbcef258b353f29f2aa9e64e45933f80084c3b5a","datavalue":{"value":{"text":"A Framework for the Automatic Formal Verification of Refinement from Cogent to C","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2829268$C7986165-11F5-4807-8999-7828A672C0AC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"44797ebb1526ec8af9c807f6bb9cf95ff33c3775","datavalue":{"value":"1478.68048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$C1E9A474-D3FF-4B12-8CC4-F154B5D353DE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5c9d5e4e4bbc7caadd09a91ffa27413cd340830a","datavalue":{"value":"10.1007/978-3-319-43144-4_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$D615C508-3539-45BF-AFCB-E710B15D39F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"686f26ef2102dec34f922caacebd6571ad7fe765","datavalue":{"value":{"entity-type":"item","numeric-id":1786740,"id":"Q1786740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$2E0E8CD9-58AD-42C8-901B-F1BD0C43F1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fe58740a0dd2515eb5c2689375a6dfac950c43b","datavalue":{"value":{"entity-type":"item","numeric-id":2829266,"id":"Q2829266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$E9167E4C-BE95-4C53-AA7C-3694E7890102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad250d2383a6addb9f20421ad8f0febdd8925ab","datavalue":{"value":{"entity-type":"item","numeric-id":1798970,"id":"Q1798970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$DBB6D299-5D13-40C2-AF00-81677638A9F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"50d312af30877232f30bb9c23fdc31fcdcb768e4","datavalue":{"value":{"entity-type":"item","numeric-id":2631536,"id":"Q2631536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$850337F2-0FE0-47F4-9397-3BF555AD9232","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cf5bf73d892ad168b08770f308e46cff0968e0c9","datavalue":{"value":{"entity-type":"item","numeric-id":2115978,"id":"Q2115978"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$5D3FF113-CAF1-4E6F-842C-3202FDEC8FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dd6094f21c1e1d5be129c3232983e75a4ab79dfb","datavalue":{"value":{"entity-type":"item","numeric-id":2829267,"id":"Q2829267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$E8CBCFD3-9A00-4FD1-804E-8CC516053735","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"45e6c2a5937a40e685c427c9b959ad4c359ca8cc","datavalue":{"value":{"entity-type":"item","numeric-id":287363,"id":"Q287363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$40465B63-8E88-4617-B52E-64F014F2EFB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"11826fe8b3f5997f99246ef3200f2753c8a6d89b","datavalue":{"value":{"entity-type":"item","numeric-id":2163160,"id":"Q2163160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$5A319B55-9FDF-4C26-A11B-5E4501C576CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"008a47245ae11ee2f12e0bd284b000b43ab772af","datavalue":{"value":{"entity-type":"item","numeric-id":736847,"id":"Q736847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$421A3F13-3836-4574-B65A-B0FC7A849929","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$4CE5CC7A-59BF-4995-94DE-D64831ECD8CC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3adf6ceedb6d880e3aaf819e51e828456bb3558d","datavalue":{"value":{"time":"+2016-10-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2829268$24FD1E6D-46E1-4D00-9823-48AE74F44FFF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$1C5D2F93-A88F-4A63-A96B-8269097317D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$DC34E388-02B9-4269-88DF-AA046E733596","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb940840e127d32ef37e5b6d45171a45e829a8f0","datavalue":{"value":"6644752","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$AB49EC40-4477-4609-8112-D031F625DF59","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dd9f12cfff5e16518b98dae67da0e7342fa8b7f","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$BE4102D1-2804-405A-9D16-02A255CC20E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a386259d7b6de278f96d59178a0ebe00c941a927","datavalue":{"value":{"entity-type":"item","numeric-id":3543657,"id":"Q3543657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$4FC77722-BF28-4C69-86F2-25FA1655603F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d1e46bde366c9665559a7c22a84b5c9d3a328b4","datavalue":{"value":{"entity-type":"item","numeric-id":5408415,"id":"Q5408415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$A068DD26-DD41-47A7-8436-54496BB12154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$2458AC28-158B-401D-A1A9-F5528D8069C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e6d1f02d1dff7e0706b804b37a3cfa574fb6579","datavalue":{"value":{"entity-type":"item","numeric-id":2982005,"id":"Q2982005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$9D45506D-0EDA-4CAA-9CFD-FEF25D27473A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ec976db9fee9bededf233dd7d31c7e9ef2213c8","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$1B8F4FC6-FB25-4EBC-90A1-B98B0649F92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19d68f92fffaefe72b592d24843b2770631f989c","datavalue":{"value":{"entity-type":"item","numeric-id":3189788,"id":"Q3189788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$8F9B56D4-02A7-4072-BD52-F86B99E7F7A6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$F36F7F76-1D89-4D70-AE8D-3297EC698AEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$22E2C3CC-C68A-4CB3-A057-8DB7156F289A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$35CC20EE-95A2-4E17-B885-B43DEA34A785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"13f67486c0c58686d48c68220b3db374c3676e3d","datavalue":{"value":{"entity-type":"item","numeric-id":30361,"id":"Q30361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$6C03EDEA-5D41-4B32-A0B9-432531A01DFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829268$5F627808-9AFD-417D-9F0C-95F4A44F65BE","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":"Q2829268$27D01A58-C205-4DFD-AC2A-B9F61D6E2504","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"181e8a87095d12068f4737c33db4fa92c6ab9367","datavalue":{"value":"https://doi.org/10.1007/978-3-319-43144-4_20","type":"string"},"datatype":"url"},"type":"statement","id":"Q2829268$20361A7B-A7EB-40FE-81B4-E3E918459F56","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f667b0d136d878e5dc1d502cab657f908ba11d8a","datavalue":{"value":"W2412986331","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829268$83EF8F25-F2C2-409A-B950-11F2D6533610","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52b915282581e36755a7886b56f9dd0ef41fb437","datavalue":{"value":{"entity-type":"item","numeric-id":2982005,"id":"Q2982005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f38d86184aa1d67b36b22c0f689f27966061c6b8","datavalue":{"value":{"amount":"+0.837146520614624","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":"Q2829268$D296D757-4E39-43BA-960C-A0FEE368D157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ff1b3edacc699431ac79f72e3fadd5641186cde","datavalue":{"value":{"entity-type":"item","numeric-id":4808847,"id":"Q4808847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f6aace9dcb251aec48a47baf46464af89d168a2","datavalue":{"value":{"amount":"+0.7482523918151855","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":"Q2829268$772DB661-EC01-470D-B337-742ACC608597","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edc3df6eda0adfbde599dd1004027faf5061f90e","datavalue":{"value":{"entity-type":"item","numeric-id":5716570,"id":"Q5716570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7eca4508125615decc433942adeb7eb4cf6ff47","datavalue":{"value":{"amount":"+0.7455108761787415","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":"Q2829268$CB653F8C-6257-480B-ABC1-2A225A5C5F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a215fc588401e3c34e118dbe74ffb7d61a35c133","datavalue":{"value":{"entity-type":"item","numeric-id":396975,"id":"Q396975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28c7095f81e4a0a195bc36f33a6ba82c1ea30fa7","datavalue":{"value":{"amount":"+0.7362911701202393","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":"Q2829268$FFB90438-CC38-40DC-A33D-8A1A3FB4AFE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc28ae7c08274cf206e5bfc796ffc6b2a46c3f23","datavalue":{"value":{"entity-type":"item","numeric-id":5019022,"id":"Q5019022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06221a5130627814ac15ba7502cbb5e8b7c9dbec","datavalue":{"value":{"amount":"+0.7278873920440674","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":"Q2829268$D4CF8009-E1C1-4F36-AF54-0CB81EB8E79A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2829268","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2829268"}}}}}