{"entities":{"Q7361858":{"pageid":31521113,"ns":120,"title":"Item:Q7361858","lastrevid":105369947,"modified":"2026-10-07T13:38:44Z","type":"item","id":"Q7361858","labels":{"en":{"language":"en","value":"A Formal CHERI-C Memory Model"}},"descriptions":{"en":{"language":"en","value":"AFP entry CHERI-C_Memory_Model"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ca51b86818996f9b94ccdb7d891c9695601650b6","datavalue":{"value":"https://isa-afp.org/entries/CHERI-C_Memory_Model.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361858$73334BDD-46D5-49FC-A31A-56FEC4869967","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c060d113c1068dd6f40e3e29523773f7cb38f522","datavalue":{"value":{"time":"+2022-11-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361858$E4A892C8-2F7F-4B4A-80E1-E32C3386130E","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"750e6e3d11a86369cd7729e08eca3d6a6bbe81b9","datavalue":{"value":"Seung Hoon Park","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361858$59246205-468F-44A5-97FC-03C126943E6A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"34e5c3a26c993d6b04bb812e5fa2566662abe7c6","datavalue":{"value":{"text":"A Formal CHERI-C Memory Model","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361858$3EE38BDF-6C38-4246-9102-A009EC7187C3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0d35ddf02ebc95def7bb610cac046ac5a050ba60","datavalue":{"value":"In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs with uncompressed capabilities in a 'purecap' environment. We present a CHERI-C memory model theory with properties suitable for verification and potentially other types of analyses. Our theory generates an OCaml executable instance of the memory model, which is then used to instantiate the parametric Gillian program analysis framework, enabling concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361858$6BA6B176-747A-4D4F-A9BC-0C8878329A50","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$80252D65-8680-4D10-939B-90801F6D7635","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fbfcea2166cf55628dc74bb062db5b5b011195","datavalue":{"value":{"entity-type":"item","numeric-id":2914753,"id":"Q2914753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$600FB7CE-6D5B-4837-A856-87A95C1AE2D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54d5771c8aca82b2755e9866a06faec0085cdf7e","datavalue":{"value":{"entity-type":"item","numeric-id":1694027,"id":"Q1694027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$44EF87DF-CE70-4712-A4E3-EC199195B989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7a1ce015f9a6115f5e15ce96a4b6a73ac4d89f9","datavalue":{"value":{"entity-type":"item","numeric-id":5327340,"id":"Q5327340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$7CAF01B0-89FB-4833-B416-A19BD92FC5A0","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":"Q7361858$9BABEF5B-2685-4D13-A2E5-62C941DF02D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"196fd0683804d25f0de4557c02121011297ac821","datavalue":{"value":{"entity-type":"item","numeric-id":2233459,"id":"Q2233459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$0DE5476D-E0F1-41E2-95DD-46960779643B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97baeab46b0692e5e4140b1df7919bcaed4e26a3","datavalue":{"value":{"entity-type":"item","numeric-id":835768,"id":"Q835768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$40A024A9-52EF-4F85-BBE2-4EF48BFB1EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acd01c50bfe5a380e9f75ae1b7b05768b5cd1260","datavalue":{"value":{"entity-type":"item","numeric-id":6050919,"id":"Q6050919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$B03EC24A-29EE-48E4-8DCF-FF917CD3462A","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$27FE5858-2884-4089-907B-B1BD574CA92E","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"472350d0e5dd5ba9def2e15a38c587b54d3979fa","datavalue":{"value":{"entity-type":"item","numeric-id":7361428,"id":"Q7361428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$32FD95B7-FA48-4054-BC90-4B51744489CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"3312bc3932b5098d4ebd90c9f7efc9b5caa5d14a","datavalue":{"value":{"entity-type":"item","numeric-id":7361853,"id":"Q7361853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$230FA695-B9A8-40DB-99F5-A2C57028CC5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e63516e58241acf42ac71681fd6610456ac84f3f","datavalue":{"value":{"entity-type":"item","numeric-id":7361376,"id":"Q7361376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$BBC077C1-802A-4568-9FDB-844616A7221A","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65dbfb47d0b5da65bd2cdfbc8cab28721a9f7690","datavalue":{"value":{"entity-type":"item","numeric-id":7360803,"id":"Q7360803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$0704FE4E-8AE1-4FC0-AE0D-039EBD2259B5","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361858$F17726CA-5132-499B-A6BA-722A9364D97B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Formal CHERI-C Memory Model","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Formal_CHERI-C_Memory_Model"}}}}}