{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:52:15Z","timestamp":1770295935408,"version":"3.49.0"},"reference-count":49,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894277","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"170-178","source":"Crossref","is-referenced-by-count":14,"title":["Verifying Relational Properties using Trace Logic"],"prefix":"10.23919","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renate","family":"Eilers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pamina","family":"Georgiou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Gleiss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Kovacs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Maffei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.35"},{"key":"ref38","article-title":"Completely Automated Equivalence Proofs","volume":"abs 1705 3110","author":"zhou","year":"2017","journal-title":"CoRR"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_7"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133998"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_16"},{"key":"ref37","first-page":"349","article-title":"Automating Regression Verification","author":"felsing","year":"2014","journal-title":"ASE"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1145\/3167090","article-title":"A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations","author":"grimm","year":"2018","journal-title":"CPP"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.25"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98047-8_3"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"ref21","first-page":"157","article-title":"Generalized Property Directed Reachability","author":"hoder","year":"2012","journal-title":"SAT"},{"key":"ref24","first-page":"634","article-title":"InvGen: An Efficient Invariant Generator","author":"gupta","year":"2009","journal-title":"CAV"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_51"},{"key":"ref25","first-page":"381","article-title":"Loop Analysis by Quantification over Iterations","author":"gleiss","year":"2018","journal-title":"LPAR"},{"key":"ref10","first-page":"1","article-title":"First-Order Theorem Proving and Vampire","author":"kov\u00e1cs","year":"2013","journal-title":"CAV"},{"key":"ref11","article-title":"Verifying Relational Properties using Trace Logic","volume":"abs 1906 9899","author":"barthe","year":"2019","journal-title":"CoRR"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_19"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"ref14","article-title":"Using Joana for Information Flow Control in Java Programs – A Practical Guide","author":"graf","year":"2013","journal-title":"Software Engineering 2013 – Workshopband"},{"key":"ref15","author":"barrett","year":"2017","journal-title":"The SMT-LIB Standard Version 2 6"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009887"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"ref18","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"TACAS"},{"key":"ref19","first-page":"171","article-title":"CVC4","author":"barrett","year":"2011","journal-title":"CAV"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"ref6","first-page":"200","article-title":"Relational Verification Using Product Programs","author":"barthe","year":"2011","journal-title":"FM"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"ref49","first-page":"265","article-title":"Temporal Logics for Hyperproperties","author":"clarkson","year":"2014","journal-title":"POSTA"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111046"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.10"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660322"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"ref42","first-page":"712","article-title":"SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs","author":"lahiri","year":"2012","journal-title":"CAV"},{"key":"ref41","first-page":"811","article-title":"Abstract Semantic Differencing via Speculative Correlation","author":"partush","year":"2014","journal-title":"OOPSLA"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3276535"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","location":"San Jose, CA, USA","start":{"date-parts":[[2019,10,22]]},"end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894277.pdf?arnumber=8894277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,3]],"date-time":"2021-02-03T01:29:50Z","timestamp":1612315790000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894277\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":49,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894277","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}