{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:19:09Z","timestamp":1725538749105},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Some security properties go beyond what is expressible in terms of an<\/jats:p><jats:p>individual execution of a single program. In particular, many security<\/jats:p><jats:p>policies in cryptography can be naturally phrased as relational<\/jats:p><jats:p>properties of two open probabilistic programs. Writing and verifying<\/jats:p><jats:p>proofs of such properties is an error-prone task that calls for<\/jats:p><jats:p>automation and tool support. One of the main difficulties in<\/jats:p><jats:p>automating these proofs lies in finding adequate relational invariants<\/jats:p><jats:p>for loops and specifications for program holes.<\/jats:p><jats:p>In this talk we show<\/jats:p><jats:p>how to automate proofs of relational properties of open probabilistic<\/jats:p><jats:p>programs by adapting techniques for the automatic generation of<\/jats:p><jats:p>universally quantified invariants in a non-relational setting.<\/jats:p>","DOI":"10.29007\/t2h1","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:03:00Z","timestamp":1516748580000},"page":"2-0","source":"Crossref","is-referenced-by-count":0,"title":["Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)"],"prefix":"10.29007","volume":"28","author":[{"given":"Klaus","family":"von Gleissenthall","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"VPT 2014. Second International Workshop on Verification and Program Transformation"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:03:01Z","timestamp":1516748581000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/JvN1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/t2h1","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}