{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T21:06:43Z","timestamp":1725656803907},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce a language-parametric calculus for k-safety verification - Cartesian Reach- ability logic (CRL).<\/jats:p><jats:p>In recent years, formal verification of hyperproperties has become an important topic in the formal methods community. An interesting class of hyperproperties is known as k-safety properties, which express the absence of a bad k-tuple of execution traces. Many security policies, such as noninterference, and functional properties, such as commutativity, monotonicity, and transitivity, are k-safety properties. A prominent example of a logic that can reason about k-safety properties of software systems is Cartesian Hoare logic (CHL). However, CHL targets a specific, small imperative language. In order to use it for sound verification of programs in a different language, one needs to extend it with the desired features or hand-craft a translation. Both these approaches require a lot of tedious, error- prone work.<\/jats:p><jats:p>Unlike CHL, CRL is language-parametric: it can be instantiated with an operational semantics (of a certain kind) of any deterministic language. Its soundness theorem is proved once and for all, with no need to adapt or re-prove it for different languages or their variants. This approach can significantly reduce the development costs of tools and techniques for sound k-safety verification of programs in deterministic languages: for exam- ple, of smart contracts written for EVM (the language powering the Ethereum blockchain), which already has an operational semantics serving as a reference.<\/jats:p>","DOI":"10.29007\/1874","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:10Z","timestamp":1685830210000},"page":"405-352","source":"Crossref","is-referenced-by-count":0,"title":["Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties"],"prefix":"10.29007","volume":"94","author":[{"given":"Jan","family":"Tu\u0161il","sequence":"first","affiliation":[]},{"given":"Traian","family":"Serbanuta","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Obdrzalek","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:11Z","timestamp":1685830211000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/8vTf"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/1874","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}