{"entities":{"Q5919481":{"pageid":8051074,"ns":120,"title":"Item:Q5919481","lastrevid":57635664,"modified":"2026-03-31T17:13:57Z","type":"item","id":"Q5919481","labels":{"en":{"language":"en","value":"Automatically verifying temporal properties of pointer programs with cyclic proof"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7176610"}},"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":"Q5919481$9F3541CC-3DD5-4D0D-BF9B-FD9B919B9246","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6102ae6773bd7b721ac89ffb8bc0e3c6179ed661","datavalue":{"value":{"text":"Automatically verifying temporal properties of pointer programs with cyclic proof","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5919481$8BE4EBAB-5994-4AD0-ABCB-35C7AEAB5073","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7ad2640ae39a5c68f3f2c9129d03963f4b947649","datavalue":{"value":"1468.68137","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$0F49756D-2B51-4582-8D2C-60246F91EE6E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"862b8afa3123f53fe4a5f9864314e14cf7e2f7a8","datavalue":{"value":{"entity-type":"item","numeric-id":2303252,"id":"Q2303252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$97203FDA-3D13-4AAE-BC3F-1F58877526F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b218d394a4f78b8be43b552938ed5e21a7cf904e","datavalue":{"value":{"entity-type":"item","numeric-id":1401935,"id":"Q1401935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$0F027EB9-1694-47B9-A0F0-B0342AD671CC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$963883B7-B33D-400D-A325-21786257AEFC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61e2e5951dfff50ebb9b8606073c3ef7da57bd09","datavalue":{"value":{"time":"+2020-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5919481$64FB4A3D-BE20-42A9-828F-1D92A314CD91","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$8FAC7E4C-94F3-46B2-B855-4043AC908B09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$14D32A67-AE7B-46D3-BFF9-89156791977D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$366B2794-6B79-496D-8576-5D8904789C79","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ed10c8ca2c71d45ea32211a49ef0caeb1c1648d0","datavalue":{"value":"7176610","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$5B2A9F23-BC68-4DC2-83EC-9C74084A5CFA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a81c26c178c84ff50de2a092c1964baa741ed82f","datavalue":{"value":"cyclic proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919481$18573333-CA99-4317-AE64-D7AB7FE62DB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919481$377CFCBA-9AFC-4AA4-AD88-EAE9BC8F2B4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919481$B32B9966-358C-4574-8FF7-B11970F1087E","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":"Q5919481$B07033A9-E868-4A37-A77A-4777D1DABA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f078e243cc5b2a268355ae913e6ed1ca3bb0dc8","datavalue":{"value":{"entity-type":"item","numeric-id":20519,"id":"Q20519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$3EACDB18-8164-4C0A-B4FA-D8617E81CB39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fdab07d39556d0075d882dcfd5a58c05fcf1a7e9","datavalue":{"value":{"entity-type":"item","numeric-id":21698,"id":"Q21698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$C50D4775-A3B1-4FBA-B329-4E054928E8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f7cbd45ecb73cef1c098eba204d848b9a2d6639","datavalue":{"value":{"entity-type":"item","numeric-id":30358,"id":"Q30358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$8191F20C-D760-4C1C-88F7-EEA2EF6715C5","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":"Q5919481$1285EF32-D37F-4B94-A443-9FA0950A21F2","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":"Q5919481$C6DAAB84-E6D0-4CE8-9B08-CFDE985D873E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"83b15b78659eaae4bbff5044735a9498fbec3859","datavalue":{"value":"https://doi.org/10.1007/s10817-019-09532-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q5919481$16D8DA01-52AD-4440-8BD3-9E249DAD537F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7519df585c699342a8810f07fcff96bb09142170","datavalue":{"value":"W2967943502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$EF58DCEE-0048-4788-B004-D03749CBC0BD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c642b8a2a51ea751f61c4db5e751f89086f5237","datavalue":{"value":{"entity-type":"item","numeric-id":5465888,"id":"Q5465888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$2BCE0D0B-BCF7-4AD1-9E7C-CEC900451D8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f9e8e1fe138d59390014af6d7c1a08c93029421","datavalue":{"value":{"entity-type":"item","numeric-id":3611996,"id":"Q3611996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$62C3AD6A-DEDD-463C-8C99-679D2565C2A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea8839917919f90fa144382a094d8dea8f58a77f","datavalue":{"value":{"entity-type":"item","numeric-id":3189830,"id":"Q3189830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$3F2BF9F6-A03F-4AB5-BC8F-826CE52D3C37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60159374e2e3f1fa60e69dc94c949ae9174a77c0","datavalue":{"value":{"entity-type":"item","numeric-id":5308405,"id":"Q5308405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$0281C66B-6B1F-41CA-8466-3BB9AC8E987C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb9167a15a02d50f8531d7407b8aced98fa4dc9","datavalue":{"value":{"entity-type":"item","numeric-id":3336675,"id":"Q3336675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$20A21B0F-F885-4503-A599-268870E18406","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0f7b2ff21c29b868e86b16c540a19ece6dbb830","datavalue":{"value":{"entity-type":"item","numeric-id":3189807,"id":"Q3189807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$9011BD97-3EF6-4642-9B38-586E784572E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50d3aa0210782da37126ac4f34c7beb5d58468c5","datavalue":{"value":{"entity-type":"item","numeric-id":1702907,"id":"Q1702907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$E06F384B-B057-4306-98AE-83E8A5B599F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5317d011f6522f5a129d65a3c878ff84c282b532","datavalue":{"value":{"entity-type":"item","numeric-id":5408559,"id":"Q5408559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$717F4690-FF76-4694-8219-8E2CF3258A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cd56f820547becaf1640ba57e415b67b2dccf11","datavalue":{"value":{"entity-type":"item","numeric-id":3766825,"id":"Q3766825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$ED440EC8-17C1-4C04-A664-87F667203D69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd6deb278e1f91c3de81d9974d31adceca1632bc","datavalue":{"value":{"entity-type":"item","numeric-id":4885623,"id":"Q4885623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$7B9CACB1-9759-420C-9E5E-85DFC49D4DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e33b53c9004b61a90401a2052769d8efa2f34a0","datavalue":{"value":{"entity-type":"item","numeric-id":4120115,"id":"Q4120115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$3A955B62-91BA-4809-8A01-D0A9EA160C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8aa9813c5d44205ab458818c2c071032f8d571d6","datavalue":{"value":{"entity-type":"item","numeric-id":5255075,"id":"Q5255075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$0D5D36BF-6824-4F35-BF9C-7E52B95C695F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a2b1afdfd50f7f4404e431384ee3957a9cf5c28","datavalue":{"value":{"entity-type":"item","numeric-id":1176248,"id":"Q1176248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$DC16457B-99F0-44AE-9554-C98020764740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d53d19922c3a7c2ab66b49e3b99548004028739","datavalue":{"value":{"entity-type":"item","numeric-id":3940830,"id":"Q3940830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$B568E7C1-44A0-4446-9711-77E915079617","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cd21ad2b3de9b7229918c441084c25ebdbf827a","datavalue":{"value":{"entity-type":"item","numeric-id":4738238,"id":"Q4738238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$A14621A5-7AC8-45FD-A26D-B0879B6E00EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f79af7c6c26413e6cf62b9d55caa06072ad927ad","datavalue":{"value":{"entity-type":"item","numeric-id":4417874,"id":"Q4417874"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$753A078F-E015-419B-B439-CB3B2110F40B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e42f666afe3b457071a11357bcb42a2f8e00fe0","datavalue":{"value":{"entity-type":"item","numeric-id":5920091,"id":"Q5920091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$9C690983-537C-4A0A-BEB0-DCDAD03D36E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13221a28888c9beff2950e6426d16471a2f129f1","datavalue":{"value":{"entity-type":"item","numeric-id":3525642,"id":"Q3525642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$433EAB02-3CB5-495B-B8D3-5135F238AA8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7a9ad4d889d3380a47b465c17efa91abd3be07b","datavalue":{"value":{"entity-type":"item","numeric-id":2277249,"id":"Q2277249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$3FD181AB-FA9D-4217-B446-EDC675ED96EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23f30d092bd9392a273a20f47ef06ab4dc28e2f7","datavalue":{"value":{"entity-type":"item","numeric-id":1856161,"id":"Q1856161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919481$5819103D-3130-4FCC-9BAF-500970220BE2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"276e9d3a10937ab3070347839d9b194a50ef5c56","datavalue":{"value":"Q127392044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$DD70D313-FEFC-4B7F-B949-6A6242BF3CAE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cd38ee88745f9653cf313327e079997efb16a6b6","datavalue":{"value":"10.1007/S10817-019-09532-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919481$1E1116E4-7B58-47E4-A481-94FA01721AF9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2c4b076b7e3b230969177f9dc444fb15289fe73","datavalue":{"value":{"entity-type":"item","numeric-id":5920091,"id":"Q5920091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29f8b10600d3c0f6c8b9a38cf850bab9c8de35db","datavalue":{"value":{"amount":"+0.984506607055664","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":"Q5919481$240BA6CB-E8B1-44BD-86CC-89224E80B649","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9babaf2bd52e8d0585eb0dfafb2c1d459313c380","datavalue":{"value":{"entity-type":"item","numeric-id":2908486,"id":"Q2908486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21e28aa772f77de72758bc20aa802a1f14d25c58","datavalue":{"value":{"amount":"+0.7767148613929749","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":"Q5919481$93802EC2-56E5-4E62-B5B6-3A9876A8C636","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55e28678e420ac861ca2aa5c03cb223e436c57d0","datavalue":{"value":{"entity-type":"item","numeric-id":4417895,"id":"Q4417895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"289b747a808827e32d3ae42da391044b8c543c7d","datavalue":{"value":{"amount":"+0.757669985294342","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":"Q5919481$DD722476-A399-4E08-ADA1-B195FD61D9F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa7200f243c8cbbc7535d3efc4d1545d4be56548","datavalue":{"value":{"entity-type":"item","numeric-id":3424121,"id":"Q3424121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5adb42a4a8ebd3163d8566e9bc056cd861ed2e7","datavalue":{"value":{"amount":"+0.7576697468757629","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":"Q5919481$85F77FAB-BDB5-4A98-B2CE-516652150FE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea93506793d7ae3e9f100eda6c9ed8d96448d9b1","datavalue":{"value":{"entity-type":"item","numeric-id":436400,"id":"Q436400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"063e964106d904c3327b70e129c021a7c3f32271","datavalue":{"value":{"amount":"+0.7545273303985596","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":"Q5919481$37B93665-6245-47F9-9A9E-762383E487A6","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":"Q5919481$CFF38F1E-AA08-4E34-BD14-F94395DCA3E0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5919481","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5919481"}}}}}