{"entities":{"Q5370919":{"pageid":7400493,"ns":120,"title":"Item:Q5370919","lastrevid":41556837,"modified":"2025-05-05T20:25:31Z","type":"item","id":"Q5370919","labels":{"en":{"language":"en","value":"LMS-Verify: abstraction without regret for verified systems programming"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6794700"}},"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":"Q5370919$390FE6EC-3262-4137-93C3-81BD5AEB546B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"71693eb602e8229f6eef6e334d9838d81186a421","datavalue":{"value":{"text":"LMS-Verify: abstraction without regret for verified systems programming","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5370919$8C52C056-5102-481B-BC38-41B10E7500F5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8ca6effc1662fee042eb3a02b9d5347b6f199dda","datavalue":{"value":"1380.68080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$4A345BC4-1F3E-4A7F-A501-D89310FE317A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f10639eb764aa0c6e6ee59118d2ca5ac9f9bad3f","datavalue":{"value":"10.1145/3009837.3009867","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$7FC8E33C-534F-423C-8D74-DA1405945713","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"941f5c14a885322e3ecd0f71e3617d2d3ebf556e","datavalue":{"value":{"entity-type":"item","numeric-id":2931831,"id":"Q2931831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$C2074F37-F417-4BD2-828C-769B4C6B7B97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"190240ccdaa97cbbe3bab5aa8731843a2be48cd9","datavalue":{"value":{"entity-type":"item","numeric-id":2931829,"id":"Q2931829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$4E2934A8-D268-4750-9644-23377FF83300","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e2300a4bb532724f6695014ad32dc9335c9fdde3","datavalue":{"value":{"entity-type":"item","numeric-id":5370840,"id":"Q5370840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$D7428D7E-5DA1-43FC-A2F9-90A22D30F9F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c23b22abb6cd47509eac4c3e5d58b13717e9ea4","datavalue":{"value":{"time":"+2017-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5370919$C040C70C-D249-4C9E-8C61-070C98FC6635","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$F78606AF-9903-41D6-B653-AF91659FB57C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"32395a8f87f6b1b3429d14e531229c93f1a3794d","datavalue":{"value":"6794700","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$8E431E03-05FE-462D-A23D-AE2A03D97E2B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01724e563a8a23e45890bcb47300ee27a032d142","datavalue":{"value":"DSLs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$8490909B-4464-45FF-960B-4E6A41C0798B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e59b6fbd93e932ad270b3f0bab8c6d74c6d46279","datavalue":{"value":"Frama-C","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$F77A8BFE-9059-4311-89D4-18CC52541543","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02dac6b2ecdfd8a4cddfee929d3c125495163b67","datavalue":{"value":"LMS","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$93719D5E-1589-4EA8-B692-24F093E4791C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0cec728a9c845fad15b06daa658e3c701e124d96","datavalue":{"value":"blame","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$44511C21-125E-4294-92A9-D63B991D236C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6839e7a5bf845c5aa2d2c6fcdf96d0d9976a520","datavalue":{"value":"contracts","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$5C8748C9-B707-4767-B6C7-DE8813E82CC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa365f462f7bd1b9fdf8abaedd14810c00851a5f","datavalue":{"value":"memory safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$791E7CFD-9230-424A-AC51-845BF433338D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"84c612e97d0bbc5f0fc0c1fc6c648d85c6d9bbe2","datavalue":{"value":"security","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$6FCD0F3A-8875-42C1-BF70-9D1543269517","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370919$FA901377-2C90-40C3-A798-4CC111D353CB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3fa0ba30f2225a69a75d233361703cec68c39010","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$A6085382-0F53-40E3-B73A-938E6DCD915A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$FB2CD320-89F0-4FD1-BF45-EB59B23C6F1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bdfb2551e094d395731ce98c96deedd86ac027b7","datavalue":{"value":{"entity-type":"item","numeric-id":17257,"id":"Q17257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$8069AD4D-DFC2-4CC1-8027-0125F334C47D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dee6d695234cdfbc4a272f03f51845f9fcd03368","datavalue":{"value":{"entity-type":"item","numeric-id":16399,"id":"Q16399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$309CAF30-2E56-4A35-B883-C36BE846CB7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"94a83aebbff287adfc2566cf5a58d543fa9638cc","datavalue":{"value":{"entity-type":"item","numeric-id":21152,"id":"Q21152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$7C432035-908D-495C-99DA-31DE2330C6DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d1bc951072aa6fcd7c9de0e485148951c5b2e7be","datavalue":{"value":{"entity-type":"item","numeric-id":31814,"id":"Q31814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370919$83C581C1-C1E1-4C04-8E6E-FADA44102D8D","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":"Q5370919$88968EBE-C27A-45EE-9924-62B5002F6100","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"01a0d1c30c9abe4c17dbcfa6bce46c920ba9bd62","datavalue":{"value":"https://doi.org/10.1145/3009837.3009867","type":"string"},"datatype":"url"},"type":"statement","id":"Q5370919$0BE440BF-24C0-4471-8903-487BB43E1B5F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aa86914899154b46193b16d5273928582d3c55b6","datavalue":{"value":"W2562397426","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$C4B78BAC-95EA-48AB-9C65-52AC54427A1A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d1b83c55465cb9ae7554b9528760c250a16f69bb","datavalue":{"value":"Q131121844","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370919$944E32D3-E01D-4D8B-A172-386D27648897","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9b5b99b202273c22d99309871c4c484e279db9e","datavalue":{"value":{"entity-type":"item","numeric-id":2801764,"id":"Q2801764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a72b870e674cad60939a7bfdfa7dabbff38f4fb5","datavalue":{"value":{"amount":"+0.8747221","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":"Q5370919$2154453A-4C1C-482F-8E43-241753310691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05ee8fff1c76d4e0123eb64394bb6ab65223b5cb","datavalue":{"value":{"entity-type":"item","numeric-id":5194962,"id":"Q5194962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6f6d62720840e39e6e76e2901c9fccd3131feb4","datavalue":{"value":{"amount":"+0.8672075","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":"Q5370919$37BA7B72-F342-4944-A835-AA4009904F7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b8da9fb4f9eab46bd6e16b4f154c7a638708e1a","datavalue":{"value":{"entity-type":"item","numeric-id":5452604,"id":"Q5452604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85bd9444d449b893de11a9b037c1d1402efcb0d0","datavalue":{"value":{"amount":"+0.86412764","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":"Q5370919$AF43C512-7A78-41C3-A99A-0AC109ACB601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920846cee47ebcd0c156e2badd883856874915ab","datavalue":{"value":{"entity-type":"item","numeric-id":681346,"id":"Q681346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d363a2fd5e2d658d8d4f7abe917e9f8ce6f60402","datavalue":{"value":{"amount":"+0.85918826","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":"Q5370919$9A03E013-6FA2-4EB5-9350-8277AC4D70B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5beef82811c1ed410a89dd64b21f082cf77902e7","datavalue":{"value":{"entity-type":"item","numeric-id":5172657,"id":"Q5172657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d363a2fd5e2d658d8d4f7abe917e9f8ce6f60402","datavalue":{"value":{"amount":"+0.85918826","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":"Q5370919$6C21C776-731A-4C16-A6A4-068A4E643060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4272bd6738545a81c2018c26962d92a456a460e5","datavalue":{"value":{"entity-type":"item","numeric-id":3132070,"id":"Q3132070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b58f60059e98fa58025e845db10bf52e767fa74","datavalue":{"value":{"amount":"+0.8589052","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":"Q5370919$DF295517-DEC0-470E-9603-FE83E1BBB152","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5370919","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5370919"}}}}}