{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:09:59Z","timestamp":1784844599802,"version":"3.55.0"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {CHCs}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>CHCs<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond <jats:italic>k<\/jats:italic>-safety such as generalized non-interference and co-termination.<\/jats:p><jats:p>This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {pfwCSP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>pfwCSP<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {CHCs}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>CHCs<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate <jats:italic>schedulers<\/jats:italic> (or <jats:italic>alignment<\/jats:italic>) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {pfwCSP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>pfwCSP<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> based on <jats:italic>stratified<\/jats:italic> CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.<\/jats:p><jats:p>We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_35","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"742-766","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":49,"title":["Constraint-Based Relational Verification"],"prefix":"10.1007","author":[{"given":"Hiroshi","family":"Unno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. J. Funct. Program. 29, E16 (2019)","DOI":"10.1017\/S0956796819000145"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8"},{"key":"35_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 (2017)","DOI":"10.1145\/3062341.3062378"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional programs by first-order refinement. In: PEPM (2015)","DOI":"10.1145\/2678015.2682546"},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: POPL (2017)","DOI":"10.1145\/3009837.3009889"},{"key":"35_CR6","unstructured":"Barthe, G.: An introduction to relational program verification (2020)"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: FM (2011)","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"35_CR8","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW (2004)"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"issue":"7","key":"35_CR10","first-page":"483","volume":"79","author":"L Beringer","year":"2010","unstructured":"Beringer, L.: Relational bytecode correlations. J. Log. Alg. Meth. Pro. 79(7), 483\u2013514 (2010)","journal-title":"J. Log. Alg. Meth. Pro."},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. Arch. Formal Proofs (2008)","DOI":"10.1109\/CSF.2007.30"},{"key":"35_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_61"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-89960-2_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Champion","year":"2018","unstructured":"Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 365\u2013384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_20"},{"key":"35_CR15","doi-asserted-by":"crossref","unstructured":"Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: PLDI (2019)","DOI":"10.1145\/3314221.3314596"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"Clochard, M., March\u00e9, C., Paskevich, A.: Deductive verification with ghost monitors. In: PACMPL, vol. 4, no. POPL (2020)","DOI":"10.1145\/3371070"},{"key":"35_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"N Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"\u00c1 Darvas","year":"2005","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193\u2013209. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32004-3_20"},{"issue":"1","key":"35_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3324783","volume":"42","author":"M Eilers","year":"2020","unstructured":"Eilers, M., M\u00fcller, P., Hitz, S.: Modular product programs. TOPLAS 42(1), 1\u201337 (2020)","journal-title":"TOPLAS"},{"issue":"OOPSLA","key":"35_CR22","first-page":"1","volume":"2","author":"P Ezudheen","year":"2018","unstructured":"Ezudheen, P., Neider, D., D\u2019Souza, D., Garg, P., Madhusudan, P.: Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2(OOPSLA), 1\u201325 (2018)","journal-title":"PACMPL"},{"key":"35_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-030-25540-4_11","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2019","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 200\u2013218. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11"},{"key":"35_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-96145-3_7","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2018","unstructured":"Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 124\u2013143. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_7"},{"key":"35_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"35_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"35_CR27","doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL (2016)","DOI":"10.1145\/2837614.2837664"},{"key":"35_CR28","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: PLDI (2015)","DOI":"10.1145\/2737924.2737976"},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"35_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"35_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-38574-2_20","volume-title":"Automated Deduction \u2013 CADE-24","author":"C Hawblitzel","year":"2013","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 282\u2013299. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_20"},{"key":"35_CR32","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica horn solver. In: FMCAD (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"35_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-22110-1_38","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2011","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: verifying functional programs using abstract interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 470\u2013485. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_38"},{"key":"35_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_33"},{"key":"35_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"key":"35_CR36","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI (2011)","DOI":"10.1145\/1993498.1993525"},{"key":"35_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"35_CR38","unstructured":"Krishna, S., Puhrsch, C., Wies, T.: Learning invariants using decision trees. CoRR abs\/1501.04725 (2015)"},{"key":"35_CR39","doi-asserted-by":"crossref","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. LMCS 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"35_CR40","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: SP (1988)"},{"key":"35_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"35_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11863908_18","volume-title":"Computer Security \u2013 ESORICS 2006","author":"DA Naumann","year":"2006","unstructured":"Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 279\u2013296. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11863908_18"},{"key":"35_CR43","doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: Thirty-seven years of relational hoare logic: remarks on its principles and history. CoRR abs\/2007.06421 (2020)","DOI":"10.1007\/978-3-030-61470-6_7"},{"key":"35_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-25540-4_17","volume-title":"Computer Aided Verification","author":"S Padhi","year":"2019","unstructured":"Padhi, S., Millstein, T., Nori, A., Sharma, R.: Overfitting in synthesis: theory and practice. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 315\u2013334. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_17"},{"key":"35_CR45","doi-asserted-by":"crossref","unstructured":"Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: PLDI (2016)","DOI":"10.1145\/2908080.2908099"},{"key":"35_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-96145-3_9","volume-title":"Computer Aided Verification","author":"L Pick","year":"2018","unstructured":"Pick, L., Fedyukovich, G., Gupta, A.: Exploiting synchrony and symmetry in relational verification. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 164\u2013182. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_9"},{"key":"35_CR47","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice Hall (1981)"},{"key":"35_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-642-37036-6_31","volume-title":"Programming Languages and Systems","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574\u2013592. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31"},{"key":"35_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-38856-9_21","volume-title":"Static Analysis","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 388\u2013411. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_21"},{"key":"35_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-25540-4_9","volume-title":"Computer Aided Verification","author":"R Shemer","year":"2019","unstructured":"Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 161\u2013179. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9"},{"key":"35_CR51","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"35_CR52","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: PLDI (2016)","DOI":"10.1145\/2908080.2908092"},{"key":"35_CR53","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: POPL (2010)","DOI":"10.1145\/1706299.1706315"},{"key":"35_CR54","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":"35_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/978-3-662-46669-8_25","volume-title":"Programming Languages and Systems","author":"T Terauchi","year":"2015","unstructured":"Terauchi, T., Unno, H.: Relaxed stratification: a new approach to practical complete predicate refinement. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 610\u2013633. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_25"},{"key":"35_CR56","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP (2009)","DOI":"10.1145\/1599410.1599445"},{"key":"35_CR57","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N., Yonezawa, A.: Combining type-based analysis and model checking for finding counterexamples against non-interference. In: PLAS (2006)","DOI":"10.1145\/1134744.1134750"},{"key":"35_CR58","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational verification (2021). http:\/\/www.cs.tsukuba.ac.jp\/~uhiro\/"},{"key":"35_CR59","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"},{"key":"35_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","volume-title":"Static Analysis","author":"C Urban","year":"2013","unstructured":"Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 43\u201362. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_5"},{"key":"35_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-54833-8_22","volume-title":"Programming Languages and Systems","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 412\u2013431. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_22"},{"issue":"2\u20133","key":"35_CR62","first-page":"167","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano, D.M., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Compt. Secr. 4(2\u20133), 167\u2013187 (1996)","journal-title":"J. Compt. Secr."},{"key":"35_CR63","unstructured":"Volpano, D.M., Smith, G.: Eliminating covert flows with minimum typings. In: CSFW (1997)"},{"key":"35_CR64","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"},{"key":"35_CR65","doi-asserted-by":"crossref","unstructured":"Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: PLDI (2018)","DOI":"10.1145\/3192366.3192416"},{"key":"35_CR66","doi-asserted-by":"crossref","unstructured":"Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: ICFP (2015)","DOI":"10.1145\/2784731.2784766"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:11:09Z","timestamp":1626480669000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}