{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:11Z","timestamp":1775873531690,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_9","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T22:25:55Z","timestamp":1532125555000},"page":"164-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Exploiting Synchrony and Symmetry in Relational Verification"],"prefix":"10.1007","author":[{"given":"Lauren","family":"Pick","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"9_CR1","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX, pp. 53\u201370. USENIX Association (2016)"},{"issue":"5","key":"9_CR2","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"FA Aloul","year":"2006","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Comput. 55(5), 549\u2013558 (2006)","journal-title":"IEEE Trans. Comput."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: PLDI, pp. 362\u2013375 (2017)","DOI":"10.1145\/3062341.3062378"},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.scico.2016.02.007","volume":"137","author":"K Asada","year":"2017","unstructured":"Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. 137, 2\u201362 (2017)","journal-title":"Sci. Comput. Program."},{"key":"9_CR5","unstructured":"Banerjee, A., Naumann, D.A., Nikouei, M.: Relational logic with framing and hypotheses. In: IARCS. LIPIcs, vol. 65, pp. 11:1\u201311:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100\u2013114. IEEE (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14\u201325 (2004)","DOI":"10.1145\/964001.964003"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. In: CSF, pp. 233\u2013248. IEEE Computer Society (2007)","DOI":"10.1109\/CSF.2007.30"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Chen, J., Feng, Y., Dillig, I.: Precise detection of side-channel vulnerabilities using quantitative Cartesian hoare logic. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 875\u2013890 (2017)","DOI":"10.1145\/3133956.3134058"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-56922-7_37","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"1993","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450\u2013462. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_37"},{"key":"9_CR12","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: KR, pp. 148\u2013159 (1996)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-662-53413-7_8","volume-title":"Static Analysis","author":"E Angelis De","year":"2016","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Relational verification through horn clause transformation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 147\u2013169. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_8"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"Computer Aided Verification","author":"A Donaldson","year":"2011","unstructured":"Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356\u2013371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_28"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-56922-7_38","volume-title":"Computer Aided Verification","author":"EA Emerson","year":"1993","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463\u2013478. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_38"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-319-41540-6_24","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2016","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Property directed equivalence via abstract simulation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 433\u2013453. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_24"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ASE, pp. 349\u2013360. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/3-540-63166-6_52","volume-title":"Computer Aided Verification","author":"P Godefroid","year":"1997","unstructured":"Godefroid, P.: VeriSoft: a tool for the automatic analysis of concurrent reactive software. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 476\u2013479. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_52"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC, pp. 466\u2013471. ACM (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61474-5_65","volume-title":"Computer Aided Verification","author":"CN Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Verifying systems with replicated components in mur$${\\upphi }$$\u03d5. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 147\u2013158. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_65"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-319-48869-1_12","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"M Kiefer","year":"2016","unstructured":"Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 149\u2013165. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_12"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: FSE, pp. 345\u2013355. ACM (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: towards usable verification. In: PLDI, p. 32. ACM (2014)","DOI":"10.1145\/2666356.2594326"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Mordvinov, D., Fedyukovich, G.: Synchronizing constrained horn clauses. In: LPAR. EPiC Series in Computing, vol. 46, pp. 338\u2013355. EasyChair (2017)","DOI":"10.29007\/gr5c"},{"key":"9_CR25","unstructured":"Mordvinov, D., Fedyukovich, G.: Verifying safety of functional programs with rosette\/unbound. CoRR, abs\/1704.04558 (2017). https:\/\/github.com\/dvvrd\/rosette"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Pick, L., Fedyukovich, G., Gupta, A.: Exploiting synchrony and symmetry in relational verification (extended version of CAV 2018 paper). https:\/\/cs.princeton.edu\/%7Eaartig\/papers\/synonym-cav18.pdf","DOI":"10.1007\/978-3-319-96145-3_9"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: PLDI, pp. 57\u201369. ACM (2016)","DOI":"10.1145\/2908080.2908092"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-319-48989-6_39","volume-title":"FM 2016: Formal Methods","author":"O Strichman","year":"2016","unstructured":"Strichman, O., Veitsman, M.: Regression verification for unbalanced recursive functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 645\u2013658. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_39"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-319-63390-9_30","volume-title":"Computer Aided Verification","author":"H Unno","year":"2017","unstructured":"Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 571\u2013591. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_30"},{"issue":"1\u20133","key":"9_CR31","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. Theoret. Comput. Sci. 375(1\u20133), 308\u2013334 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35\u201351. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T23:02:20Z","timestamp":1751756540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}