{"entities":{"Q5164171":{"pageid":7193742,"ns":120,"title":"Item:Q5164171","lastrevid":57685716,"modified":"2026-03-31T22:03:30Z","type":"item","id":"Q5164171","labels":{"en":{"language":"en","value":"Highly automated formal proofs over memory usage of assembly code"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7423369"}},"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":"Q5164171$47D03DCF-0510-43A7-AF2B-0CF4B9A13741","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1ede00579c2ed99850d7b97c5673effb6c9f572a","datavalue":{"value":{"text":"Highly Automated Formal Proofs over Memory Usage of Assembly Code","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5164171$2A55E022-ED2C-4C7E-BAFD-0CD19D959653","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ec92018b8a398a9dfc6a8a31fa55bfdf9d2506e5","datavalue":{"value":"1483.68211","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$DE3A8D0A-EDE7-44E3-8B9A-7AA66B65B136","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"779cdaf134c1db9420ce3ae474d325bfb9a41188","datavalue":{"value":"10.1007/978-3-030-45237-7_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$499FD00F-0F9E-47F8-9C20-66D94B18871A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d4bf01e8df1c87de639938e4e74854e4e2315839","datavalue":{"value":{"entity-type":"item","numeric-id":437038,"id":"Q437038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$DA0B3548-3A7E-4B73-BBAF-A973C5C68BC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7bb61dc959d352f749f23d027ff4e8506dc5710d","datavalue":{"value":{"entity-type":"item","numeric-id":5164170,"id":"Q5164170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$50B7B2A9-4BD4-40E6-8378-01CA50AD45E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ba80e0c39cba5ea7df8d1c8803db9f59e5a7a626","datavalue":{"value":{"entity-type":"item","numeric-id":202509,"id":"Q202509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$79E9D718-3838-440E-8906-DD83AE0DA98E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$2CB23CBD-63C4-4C85-B07D-B78ECAAB983B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e41df14f190dd9eb0cc664848f84d930123fd453","datavalue":{"value":{"time":"+2021-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":"Q5164171$A2A20244-F3B3-42AF-80BA-C63D5F252C03","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$1365E1E2-4BBB-4229-B76D-5D87F022EB0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$C30937B2-8927-4151-8A70-A2B054D4F5A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$378F5073-9DD4-4A7D-A087-6ABB68A550CB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4265c6f5986ae95e35b5984fac07fc0f3ab4abe0","datavalue":{"value":"7423369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$13BF71D0-3DC7-44D3-98F8-A69FB26EFE7F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5164171$590235C4-3CC3-4417-AB2C-86B84AD85B60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54becc67f9990c02508216e035db78a990087af9","datavalue":{"value":"assembly","type":"string"},"datatype":"string"},"type":"statement","id":"Q5164171$66E85E2C-FA57-44BB-812F-9D55C49533DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"603c2cfc3888648d1d2123caae87d7bffe82439d","datavalue":{"value":"x86-64","type":"string"},"datatype":"string"},"type":"statement","id":"Q5164171$CD71A3AC-AB6C-4051-A401-89C461C4B2D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"656d33a5cfe2caddb3b70f2adbdd15528cdbd7ff","datavalue":{"value":"memory usage","type":"string"},"datatype":"string"},"type":"statement","id":"Q5164171$F518ACA8-A65B-4198-984C-3D3865E7D32A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$3D9D057F-1E0A-4518-A7C8-1E595C95CF3E","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":"Q5164171$AEFB63DB-0AED-4B29-808F-A0C7C0F7C671","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"12c5d2dc030513c5b64e45ae295042b1144a72e7","datavalue":{"value":"https://doi.org/10.1007/978-3-030-45237-7_6","type":"string"},"datatype":"url"},"type":"statement","id":"Q5164171$18077242-CDAD-48A8-8E1A-B555C6A8A87D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"46772c5e487b8d8ceca3255d92323e40e6e115f6","datavalue":{"value":"W3017122865","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164171$B23107ED-B51C-4E0A-9CE3-8632699D5E09","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be67f799ffc5b3fd133657f657d0609a463820d","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$176F94AB-AEB3-4996-8F59-A997D0CEFCD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$F863D1D9-A2F8-4FD5-896E-72875773FB55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fba4064bdf078febee6c0f0306d2549b942863d8","datavalue":{"value":{"entity-type":"item","numeric-id":4371519,"id":"Q4371519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$88DF756A-8053-4EA8-AA8C-A91804E31CF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0092ca3b21f3f9cb157bf2001ff878cfeab4655","datavalue":{"value":{"entity-type":"item","numeric-id":5261525,"id":"Q5261525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$568FEF89-4387-4499-B030-A34F6B2C20B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$1F1CEFE3-2FEE-4963-8944-CCB9428F5177","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c51840355e08753d0377af591c495ff9f8053cee","datavalue":{"value":{"entity-type":"item","numeric-id":5747653,"id":"Q5747653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$79506FE2-E370-47A3-90A9-6B8FEC7959B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb644c5841dd8ef7fdeb2c27817dada70761fc00","datavalue":{"value":{"entity-type":"item","numeric-id":5429343,"id":"Q5429343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$82830B32-9E21-469A-BFD9-D47BFB0A4082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb6a694c413940271a785e87645155d12c05123","datavalue":{"value":{"entity-type":"item","numeric-id":2914735,"id":"Q2914735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$1305C1CE-5D33-45C8-8B5C-DE7D9634C92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$3DA4FF97-76FB-42B4-8E3E-6DD9DF0C1306","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"004642c985382b5c70e78b542aebcb6240614609","datavalue":{"value":{"entity-type":"item","numeric-id":4162644,"id":"Q4162644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$21E0ADFE-5DEF-49CA-B5E3-11818D1DF97E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed61338c8ff56191aea0588b04cb2088071ef44d","datavalue":{"value":{"entity-type":"item","numeric-id":2988664,"id":"Q2988664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$0E588D05-2D2E-4CB2-988F-A415BA8989EB","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":"Q5164171$5A383210-7F9D-4F63-9D68-72359327159F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d8a6a7f4a099b96912e5cba667c8ca70d007bb8","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$A3D9F712-2CE5-4599-AC4C-704B9D930427","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80015c982f395703eb961f7d88d9ea85973eed1d","datavalue":{"value":{"entity-type":"item","numeric-id":5387904,"id":"Q5387904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$9E6925E9-AE53-423D-A6D5-902A6FF090D4","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":"Q5164171$D8747E30-CEBF-466F-B200-1C78F6DD044A","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":"Q5164171$DF3E1DD4-9C11-4D07-8FE4-66D15B3D5152","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":"Q5164171$AF5F6A93-76AB-4396-9FF7-94DC1F49C048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e129a2d157f11eb104b6683d0c548da586ae805","datavalue":{"value":{"entity-type":"item","numeric-id":5823276,"id":"Q5823276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$E125F837-85C3-46E5-B61B-ACA54BD0A8A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$8FFB704B-0895-4662-87BF-FD26242A9559","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81ed7ae54210088547f50aa25fcf3f04d43110c8","datavalue":{"value":{"entity-type":"item","numeric-id":1630029,"id":"Q1630029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13242addf0a7d6c2aba62ea9cd7f6ee33eb241ee","datavalue":{"value":{"amount":"+0.7412438988685608","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":"Q5164171$FD3D6695-5E25-44A2-A3E6-313A9956C2D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efe92806a81bbea1cd5444ec3bcbd3de48fd0186","datavalue":{"value":{"entity-type":"item","numeric-id":945054,"id":"Q945054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4fe3a4d4e291f656e03f8b3ebbba90b16851f7d","datavalue":{"value":{"amount":"+0.7212440967559814","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":"Q5164171$0A05B425-4907-4AA5-B857-34EA8CB9E9ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c71ff9416a35b311f2fbf027327ee933036f7e41","datavalue":{"value":{"entity-type":"item","numeric-id":6166149,"id":"Q6166149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b173c30e7eabfe830ca2bb3b2da4d089e0eea62","datavalue":{"value":{"amount":"+0.7203149199485779","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":"Q5164171$50A8FF17-86A2-495E-90DF-AF69EA5215B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35748ffee00ce724a7ead9e1f30b786018fda879","datavalue":{"value":{"entity-type":"item","numeric-id":5758130,"id":"Q5758130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"609298b9ee3635738c13993fbc45dc982d97b455","datavalue":{"value":{"amount":"+0.7195947766304016","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":"Q5164171$88E316A3-DBDB-48E0-AA10-43DBBA48D327","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c692e4c37c0674c33839cb0a8a1ab50912d2566","datavalue":{"value":{"entity-type":"item","numeric-id":4414379,"id":"Q4414379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95371bd37bb311356ce5ff8ba20182ae0848c259","datavalue":{"value":{"amount":"+0.7186693549156189","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":"Q5164171$E3C2A812-4DB6-4FAE-A054-B2F700337BA6","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164171$836908AA-83CD-4997-A3E9-C278F9F2EFA3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5164171","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5164171"}}}}}