{"entities":{"Q1683698":{"pageid":1694439,"ns":120,"title":"Item:Q1683698","lastrevid":71967219,"modified":"2026-04-14T01:46:08Z","type":"item","id":"Q1683698","labels":{"en":{"language":"en","value":"Formally verifying exceptions for low-level code with separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6814736"}},"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":"Q1683698$07BA1881-442C-4AF7-B6FC-044775BB3BA1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd8a8d301b0889189a547cf5860f5aa81ba3426f","datavalue":{"value":{"text":"Formally verifying exceptions for low-level code with separation logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1683698$0A063AF2-E704-4B9E-A626-145DBDE6CAE2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"17b353a66b7b0d5876c796346d425a790b8d3079","datavalue":{"value":"1382.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$A6CB456B-953D-4FAA-A889-2E31ACE3E1AB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"31b7c3bc2f5e57d91d112c0ae0116bc7c92ed6da","datavalue":{"value":{"entity-type":"item","numeric-id":1683697,"id":"Q1683697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$48B02BA2-5293-468F-ABFE-5201CD4527CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4016e1f23463ca2cfa7c5bb34d7ce64f66d3ab32","datavalue":{"value":{"entity-type":"item","numeric-id":287320,"id":"Q287320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$42071C9A-9803-43E6-A7E5-ACCD705BF89F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$C2A0BCE7-27BA-42D2-983A-2474433A049C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e0b35d2e482cf5e430246ef005011e53c42974f0","datavalue":{"value":{"time":"+2017-12-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1683698$62780923-9CA1-4862-94DA-C893E1C3F3C4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d7aece285745e41234618e9f77abdc0b033e4659","datavalue":{"value":"https://kar.kent.ac.uk/67658/2/jlamp.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1683698$E3D61B02-CF4F-4335-8661-3B9C0BF3BB6F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$D0465760-F5CB-4D6C-8E13-D4C668DDBDA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$42BB3609-1C3D-4535-B487-2247500AC3C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$4D012C5C-5DF4-4632-AAB8-6B5C554A187C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$ADD512D5-DE25-45D9-919A-F0B0F61B8225","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4128332743ff652a0c593563dea5090932127f89","datavalue":{"value":"6814736","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$F160CB1D-1EE8-424E-9B28-FD49CF049CF5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$2F4F7858-B63C-42B4-B3F8-F881CB094584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$D8EC0B32-7140-436D-B5E5-896BF248E00D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54becc67f9990c02508216e035db78a990087af9","datavalue":{"value":"assembly","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$60005DD2-0459-41F2-9151-C75B8341704B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$EF1E3866-BB90-4D6A-911A-DDE4E68422A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"16260849d15e6a1f1a5e5b052c5f4dea3365792c","datavalue":{"value":"exceptions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$4A2EC352-7194-45AD-A60E-CDE4EE2FBBBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26f184cfe25f9b3d9687d793c2fb3c66c6d5cb10","datavalue":{"value":"step-indexed models","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$8CA85FCF-503F-4A8B-9A65-B698AD67F85F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1683698$F6A71FF0-9B47-4BA1-BCED-D9A31A1E4594","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"605960617776ba8ed66a185753927e4ca021062f","datavalue":{"value":{"entity-type":"item","numeric-id":34522,"id":"Q34522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$2D06ED68-2184-453E-85B9-C1ACCF1CBF38","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":"Q1683698$5A1D3DA3-BABC-4849-894B-7C39A71CDA8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7ee2575b4b00dc5c48fe05a1a87740d06a1036d4","datavalue":{"value":{"entity-type":"item","numeric-id":21498,"id":"Q21498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$E8E01501-C501-40A9-B8B0-6291724C7B10","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":"Q1683698$1EE9AA59-D1A4-4DC1-A7BF-025779CEDD5E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c63f03074ff7309b17aed246d7704ba009b284b3","datavalue":{"value":"W2763243490","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$05E50AD9-6334-4EFD-9FA4-B1295AD87CD7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"db60aa38e98e0710c59268a6db48219f49912366","datavalue":{"value":{"entity-type":"item","numeric-id":3189790,"id":"Q3189790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$F33C4084-3D10-4C8B-9630-F995683CCBB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c46319975d5f428b28cf95457785c347fec2d0df","datavalue":{"value":{"entity-type":"item","numeric-id":5494381,"id":"Q5494381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$E5B9ACEB-5AFD-406F-925D-0D52BDDA1D2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e949d01eb7df08ca150012cd94d15a2478e4bc1","datavalue":{"value":{"entity-type":"item","numeric-id":2914751,"id":"Q2914751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$1C10CD41-299B-43AD-85BF-1E2DBA8EB389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3c1819ebc3ca4c31460cf0d96175b695d4d4a32","datavalue":{"value":{"entity-type":"item","numeric-id":3087993,"id":"Q3087993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$E1CB8271-A86F-4E89-A760-C272B7EECE93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6456459239ab3bc5fb70e6036ded27e15251da27","datavalue":{"value":{"entity-type":"item","numeric-id":3166222,"id":"Q3166222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$1828054A-4CA8-4614-B62F-DA719F80DE65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3622affd036941377c9e52665161c351be7b4478","datavalue":{"value":{"entity-type":"item","numeric-id":1874283,"id":"Q1874283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$9733C31F-9D0B-4DAE-91D5-E40136EFE8E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec74d20684f0db92c7b7c4239af905bf28ce3849","datavalue":{"value":{"entity-type":"item","numeric-id":1663225,"id":"Q1663225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$4CD92615-EA66-4AD2-9A1F-E77C8E6AB325","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fada031ed317bb64d11da1455ad747b8e2232454","datavalue":{"value":{"entity-type":"item","numeric-id":835764,"id":"Q835764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$2ED0ABD9-C559-461F-AF20-1C7BD28F081D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac23d65a9afeff852c7bda4556ad42907e525e44","datavalue":{"value":{"entity-type":"item","numeric-id":5178870,"id":"Q5178870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$B2F169D1-6B90-4EB5-802C-673147A4F129","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcf06957483d96f85ec0bb9bf6a5c5b9186a884d","datavalue":{"value":{"entity-type":"item","numeric-id":2931805,"id":"Q2931805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$36A77C9B-1207-4F51-8832-6037F4E6CDDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac30c585b3eca0009fc86a02535b9a25c0d03553","datavalue":{"value":{"entity-type":"item","numeric-id":5758130,"id":"Q5758130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$77BE326B-C965-44E3-811A-EC63EFA57BF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb5c384f83cfe304bd792549ed6786939a461655","datavalue":{"value":{"entity-type":"item","numeric-id":4783297,"id":"Q4783297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$253D35BE-2B11-40C4-823E-9ECE9C8AF038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"582ad9ea0ec7d5d79d9b8f6e0bf88a1f856e52d7","datavalue":{"value":{"entity-type":"item","numeric-id":1887735,"id":"Q1887735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$8E7DE6AD-D67F-4E93-BCA6-1ADD32E5FD40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad9d568636dc034cf5bea0b01c0319383e3edc3a","datavalue":{"value":{"entity-type":"item","numeric-id":5410698,"id":"Q5410698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1683698$B6ABE79E-703D-4BD3-B356-1CA57AA374D4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"488a224cbad8bdc92ce07acc0344d92a0472488a","datavalue":{"value":"10.1016/J.JLAMP.2017.09.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1683698$07CB4A0E-C317-4F50-A343-4ADF73C5CF88","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfec3ced7587ca1876c7fa59a35e6c50dc496243","datavalue":{"value":{"entity-type":"item","numeric-id":2931805,"id":"Q2931805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7641905d6a071936e5dd3557caf81654c224cc6","datavalue":{"value":{"amount":"+0.7269206047058105","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":"Q1683698$FE66041D-CBAB-4C5E-B82D-E7BE835D73F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4ea7909e9397407fcbedc7c4f2e8d498454d7b4","datavalue":{"value":{"entity-type":"item","numeric-id":3189788,"id":"Q3189788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d065e80e5f01cc5d61177933dc5ac83c8dbec83","datavalue":{"value":{"amount":"+0.7178685069084167","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":"Q1683698$38D82EE9-1D3C-4B8F-9652-4D4EEDE47B17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66c4ceea5ea1c95a9cf7d540f6fdefb2a4b5cdf7","datavalue":{"value":{"entity-type":"item","numeric-id":3613337,"id":"Q3613337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5215c6c7c954544eb11ce197ff73f0f36181234d","datavalue":{"value":{"amount":"+0.7038456797599792","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":"Q1683698$757F48AF-E2CB-4CA9-B78F-699A594B07CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b06efda812282aabf24afc850612bc127dba7a9e","datavalue":{"value":{"entity-type":"item","numeric-id":835764,"id":"Q835764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e78363b08119a915811d311e6cf48a22779e8f87","datavalue":{"value":{"amount":"+0.7006523609161377","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":"Q1683698$8843E7D8-72A0-400D-811F-8BF326CD83FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21fa0d61d638319b6d1f1971ef4caf16a0f2c7d7","datavalue":{"value":{"entity-type":"item","numeric-id":3523161,"id":"Q3523161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ea99e0679488ad6c00cbf2cfe3597a438d8ff02","datavalue":{"value":{"amount":"+0.6930189728736877","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":"Q1683698$B11087CC-AC23-47D3-AE3E-C2F2DE17FD4B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formally verifying exceptions for low-level code with separation logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formally_verifying_exceptions_for_low-level_code_with_separation_logic"}}}}}