{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:36Z","timestamp":1775790696076,"version":"3.50.1"},"publisher-location":"Cham","reference-count":96,"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>This paper presents the main ideas behind deductive synthesis of heap-manipulating program and outlines present challenges faced by this approach as well as future opportunities for its applications.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_5","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"110-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities"],"prefix":"10.1007","author":[{"given":"Shachar","family":"Itzhaky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hila","family":"Peleg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reuben N. S.","family":"Rowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-319-94205-6_32","volume-title":"Automated Reasoning","author":"M Acclavio","year":"2018","unstructured":"Acclavio, M., Stra\u00dfburger, L.: From syntactic proofs to combinatorial proofs. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 481\u2013497. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_32"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"5_CR5","unstructured":"Balog, M., Gaunt, A.L., Brockschmidt, M., Nowozin, S., Tarlow, D.: Deepcoder: learning to write programs. arXiv preprint arXiv:1611.01989 (2016)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Barke, S., Peleg, H., Polikarpova, N.: Just-in-time learning for bottom-up enumerative synthesis. Proc. ACM Program. Lang. 4(OOPSLA), 227:1\u2013227:29 (2020)","DOI":"10.1145\/3428295"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5"},{"key":"5_CR8","unstructured":"Blaauwbroek, L., Urban, J., Geuvers, H.: Tactic learning and proving for the coq proof assistant. In: LPAR. EPiC Series in Computing, vol. 73, pp. 138\u2013150. EasyChair (2020)"},{"issue":"3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes, S., O\u2019Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47\u201365 (2016)","journal-title":"ACM SIGLOG News"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL, pp. 101\u2013112. ACM (2008)","DOI":"10.1145\/1328897.1328453"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459\u2013465. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_33"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","DOI":"10.1145\/2049697.2049700"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Chajed, T., Tassarotti, J., Kaashoek, M.F., Zeldovich, N.: Verifying concurrent, crash-safe systems with perennial. In: SOSP, pp. 243\u2013258. ACM (2019)","DOI":"10.1145\/3341301.3359632"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-030-53291-8_30","volume-title":"Computer Aided Verification","author":"Y Chen","year":"2020","unstructured":"Chen, Y., Wang, C., Bastani, O., Dillig, I., Feng, Yu.: Program synthesis using deduction-guided reinforcement learning. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 587\u2013610. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_30"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Chilimbi, T.M., Hill, M.D., Larus, J.R.: Cache-conscious structure layout. In: PLDI, pp. 1\u201312. ACM (1999)","DOI":"10.1145\/301631.301633"},{"issue":"9","key":"5_CR17","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234\u2013245. ACM (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-030-44914-8_6","volume-title":"Programming Languages and Systems","author":"A Costea","year":"2020","unstructured":"Costea, A., Zhu, A., Polikarpova, N., Sergey, I.: Concise read-only specifications for better synthesis of programs with pointers. In: ESOP 2020. LNCS, vol. 12075, pp. 141\u2013168. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_6"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Delignat-Lavaud, A., et al.: Implementing and proving the tls 1.3 record layer. In: S&P, pp. 463\u2013482. IEEE Computer Society (2017)","DOI":"10.1109\/SP.2017.58"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"T Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420\u2013447. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_16"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363\u2013377. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_26"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-02768-1_13","volume-title":"Programming Languages and Systems","author":"S Eguchi","year":"2018","unstructured":"Eguchi, S., Kobayashi, N., Tsukada, T.: Automated synthesis of functional programs with auxiliary functions. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 223\u2013241. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_13"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315\u2013327. ACM (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Ferraiuolo, A., Baumann, A., Hawblitzel, C., Parno, B.: Komodo: Using verification to disentangle secure-enclave hardware from software. In: SOSP, pp. 287\u2013305. ACM (2017)","DOI":"10.1145\/3132747.3132782"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Frankle, J., Osera, P.-M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: POPL, pp. 802\u2013815. ACM (2016)","DOI":"10.1145\/2914770.2837629"},{"key":"5_CR28","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: LPAR, EPiC Series in Computing, vol. 46, pp. 125\u2013143. EasyChair (2017)"},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"12","key":"5_CR30","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3318162","volume":"62","author":"C Le Goues","year":"2019","unstructured":"Le Goues, C., Pradel, M., Roychoudhury, A.: Automated program repair. Commun. ACM 62(12), 56\u201365 (2019)","journal-title":"Commun. ACM"},{"key":"5_CR31","unstructured":"Gu, R., et al.: Certikos: an extensible architecture for building certified concurrent OS kernels. In: OSDI, pp. 653\u2013669. USENIX Association (2016)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling enumerative and deductive program synthesis. In: PLDI, pp. 1159\u20131174. ACM (2020)","DOI":"10.1145\/3385412.3386027"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Hughes, D.J.D.: Unification nets: Canonical proof net quantifiers. In: LICS, pp. 540\u2013549. ACM (2018)","DOI":"10.1145\/3209108.3209159"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, RN.S., Sergey, I.: Cyclic program synthesis. In: PLDI. ACM (2021)","DOI":"10.1145\/3453483.3454087"},{"key":"5_CR35","unstructured":"Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, R.N.S., Sergey, I.: SuSLik (CAV 2021 Artifact): Code and Benchmarks, May 2021. https:\/\/doi.org\/10.5281\/zenodo.4850342"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL, pp. 271\u2013282. ACM (2011)","DOI":"10.1145\/1925844.1926417"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"5_CR38","doi-asserted-by":"publisher","first-page":"E20","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, E20 (2018)","journal-title":"J. Funct. Program."},{"key":"5_CR39","unstructured":"Kalyan, A., Mohta, A., Polozov, O., Batra, D., Jain, P., Gulwani, S.: Neural-guided deductive search for real-time program synthesis from examples. In: ICLR. OpenReview.net (2018)"},{"issue":"4","key":"5_CR40","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/j.microrel.2011.09.028","volume":"52","author":"T Kawahara","year":"2012","unstructured":"Kawahara, T., Ito, K., Takemura, R., Ohno, H.: Spin-transfer torque RAM technology: review and prospect. Microelectron. Reliab. 52(4), 613\u2013627 (2012)","journal-title":"Microelectron. Reliab."},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Klein, G.: SeL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-21668-3_13","volume-title":"Computer Aided Verification","author":"E Kneuss","year":"2015","unstructured":"Kneuss, E., Koukoutos, M., Kuncak, V.: Deductive program repair. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 217\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_13"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA, pp. 407\u2013426. ACM (2013)","DOI":"10.1145\/2544173.2509555"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-guided program synthesis. In: PLDI, pp. 253\u2013268. ACM (2019)","DOI":"10.1145\/3314221.3314602"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Lee, B.C., Ipek, E., Mutlu, O., Burger, D.: Architecting phase change memory as a scalable dram alternative. In: ISCA, pp. 2\u201313. ACM (2009)","DOI":"10.1145\/1555815.1555758"},{"key":"5_CR46","doi-asserted-by":"crossref","unstructured":"Lee, W., Heo, K., Alur, R., Naik, M.: Accelerating search-based program synthesis using learned probabilistic models. In: PLDI. ACM (2018)","DOI":"10.1145\/3192366.3192410"},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"Rustan, K., Leino, M., Milicevic, A.: Program extrapolation with jennisys. In: OOPSLA, pp. 411\u2013430. ACM (2012)","DOI":"10.1145\/2398857.2384646"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"5_CR49","unstructured":"Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: LPAR, EPiC Series in Computing, vol. 46, pp. 85\u2013105. EasyChair (2017)"},{"key":"5_CR50","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL, pp. 123\u2013136. ACM (2012)","DOI":"10.1145\/2103621.2103673"},{"issue":"2\u20133","key":"5_CR51","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","volume":"14","author":"G Malcolm","year":"1990","unstructured":"Malcolm, G.: Data structures and program transformation. Sci. Comput. Program. 14(2\u20133), 255\u2013279 (1990)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"5_CR52","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR53","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J Andreoli","year":"1992","unstructured":"Andreoli, J.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2, 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"5_CR54","unstructured":"Martelli, A., Montanari, U.: Additive AND\/OR graphs. In: IJCAI, pp. 1\u201311. William Kaufmann (1973)"},{"key":"5_CR55","unstructured":"Menon, A., Tamuz, O., Gulwani, S., Lampson, B., Kalai, A.: A machine learning framework for programming by example. In: International Conference on Machine Learning, pp. 187\u2013195 (2013)"},{"key":"5_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17184-1_1","volume-title":"Programming Languages and Systems","author":"G M\u00e9vel","year":"2019","unstructured":"M\u00e9vel, G., Jourdan, J.-H., Pottier, F.: Time credits and time receipts in iris. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 3\u201329. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_1"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"5_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-030-34175-6_14","volume-title":"Programming Languages and Systems","author":"Y Nagashima","year":"2019","unstructured":"Nagashima, Y.: LiFtEr: language to encode induction heuristics for Isabelle\/HOL. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 266\u2013287. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_14"},{"key":"5_CR59","unstructured":"Nagashima, Y.: Smart Induction for Isabelle\/HOL (Tool Paper). In: FMCAD, pp. 245\u2013254. IEEE (2020)"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"Nagashima, Y., He, Y.: PaMpeR: proof method recommendation system for Isabelle\/HOL. In: ASE, pp. 362\u2013372. ACM (2018)","DOI":"10.1145\/3238147.3238210"},{"key":"5_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"A Nanevski","year":"2014","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290\u2013310. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_16"},{"key":"5_CR62","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: POPL, pp. 261\u2013274. ACM (2010)","DOI":"10.1145\/1707801.1706331"},{"key":"5_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-67067-2_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T-T Nguyen","year":"2021","unstructured":"Nguyen, T.-T., Ta, Q.-T., Sergey, I., Chin, W.-N.: Automated repair of heap-manipulating programs using deductive synthesis. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 376\u2013400. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_17"},{"key":"5_CR64","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL, pp. 320\u2013333. ACM (2006)","DOI":"10.1145\/1111320.1111066"},{"issue":"1\u20133","key":"5_CR65","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"5_CR67","doi-asserted-by":"crossref","unstructured":"Osera, P.-M., Zdancewic, S.: Type-and-example-directed program synthesis. In: PLDI, pp. 619\u2013630. ACM (2015)","DOI":"10.1145\/2813885.2738007"},{"key":"5_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-54862-8_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper: complete heap verification with mixed specifications. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124\u2013139. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_9"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: PLDI, pp. 522\u2013538. ACM (2016)","DOI":"10.1145\/2980983.2908093"},{"issue":"POPL","key":"5_CR70","doi-asserted-by":"publisher","first-page":"72:1","DOI":"10.1145\/3290385","volume":"3","author":"N Polikarpova","year":"2019","unstructured":"Polikarpova, N., Sergey, I.: Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 3(POPL), 72:1-72:30 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"5_CR71","doi-asserted-by":"crossref","unstructured":"Protzenko, J., et al.: Evercrypt: a fast, verified, cross-platform cryptographic provider. In: S&P, pp. 983\u20131002. IEEE Computer Society (2020)","DOI":"10.1109\/SP40000.2020.00114"},{"key":"5_CR72","doi-asserted-by":"crossref","unstructured":"Qiu, X., Solar-Lezama, A.: Natural synthesis of provably-correct data-structure manipulations. PACMPL 1(OOPSLA), 65:1\u201365:28 (2017)","DOI":"10.1145\/3133889"},{"key":"5_CR73","unstructured":"Ramananandro, T., et al.: Everparse: verified secure zero-copy parsers for authenticated message formats. In: USENIX Security Symposium, pp. 1465\u20131482. USENIX Association (2019)"},{"issue":"2","key":"5_CR74","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-017-0270-2","volume":"55","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C.W., Deters, M.: Refutation-based synthesis in SMT. Formal Meth. Syst. Des. 55(2), 73\u2013102 (2019)","journal-title":"Formal Meth. Syst. Des."},{"key":"5_CR75","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)"},{"key":"5_CR76","doi-asserted-by":"crossref","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP, pp. 53\u201365. ACM (2017)","DOI":"10.1145\/3018610.3018623"},{"key":"5_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-319-21690-4_26","volume-title":"Computer Aided Verification","author":"S Saha","year":"2015","unstructured":"Saha, S., Garg, P., Madhusudan, P.: Alchemist: learning guarded affine functions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 440\u2013446. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_26"},{"key":"5_CR78","doi-asserted-by":"crossref","unstructured":"Sanchez-Stern, A., Alhessi, Y., Saul, L., Lerner, S.: Generating correctness proofs with neural networks. In: Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pp. 1\u201310. ACM (2020)","DOI":"10.1145\/3394450.3397466"},{"key":"5_CR79","doi-asserted-by":"crossref","unstructured":"Scherer, G., R\u00e9my, D.: Which simple types have a unique inhabitant? In: ICFP, pp. 243\u2013255. ACM (2015)","DOI":"10.1145\/2858949.2784757"},{"key":"5_CR80","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77\u201387. ACM (2015)","DOI":"10.1145\/2813885.2737964"},{"key":"5_CR81","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A., Delbianco, G.A.: Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In: OOPSLA, pp. 92\u2013110. ACM (2016)","DOI":"10.1145\/3022671.2983999"},{"key":"5_CR82","unstructured":"Si, X., Yang, Y., Dai, H., Naik, M., Song, L.: Learning a meta-solver for syntax-guided program synthesis. In: International Conference on Learning Representations (2019)"},{"key":"5_CR83","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326. ACM (2010)","DOI":"10.1145\/1707801.1706337"},{"key":"5_CR84","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1038\/nature06932","volume":"453","author":"DB Strukov","year":"2008","unstructured":"Strukov, D.B., Snider, G.S., Stewart, D.R., Williams, R.S.: The missing memristor found. Nature 453, 80\u201383 (2008)","journal-title":"Nature"},{"key":"5_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9"},{"key":"5_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-03542-0_8","volume-title":"Programming Languages and Systems","author":"M-T Trinh","year":"2013","unstructured":"Trinh, M.-T., Le, Q.L., David, C., Chin, W.-N.: Bi-abduction with pure properties for specification inference. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 107\u2013123. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_8"},{"key":"5_CR87","unstructured":"Turon, A.: Understanding and expressing scalable concurrency. Ph.D. thesis, Northeastern University (2013)"},{"key":"5_CR88","doi-asserted-by":"crossref","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL, pp. 343\u2013356. ACM (2013)","DOI":"10.1145\/2480359.2429111"},{"key":"5_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"key":"5_CR90","doi-asserted-by":"crossref","unstructured":"van Tonder, R., Le Goues, C.: Static automated program repair for heap properties. In: ICSE, pp. 151\u2013162 ACM (2018)","DOI":"10.1145\/3180155.3180250"},{"key":"5_CR91","doi-asserted-by":"crossref","unstructured":"Vollmer, M., Koparkar, C., Rainey, M., Sakka, L., Kulkarni, M., Newton, R.R.: LoCal: a language for programs operating on serialized data. In: PLDI, pp. 48\u201362. ACM (2019)","DOI":"10.1145\/3314221.3314631"},{"key":"5_CR92","unstructured":"Vollmer, M., et al.: Compiling tree transforms to operate on packed representations. In: ECOOP. LIPIcs, , vol. 74, pp. 26:1\u201326:29. Schloss Dagstuhl (2017)"},{"key":"5_CR93","doi-asserted-by":"crossref","unstructured":"Watanabe, Y., Gopinathan, K., P\u00eerlea, G., Polikarpova, N., Sergey, I.: Certifying the synthesis of heap-manipulating programs (2021). Conditionally accepted at ICFP\u201921","DOI":"10.1145\/3473589"},{"key":"5_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-319-63387-9_27","volume-title":"Computer Aided Verification","author":"M Windsor","year":"2017","unstructured":"Windsor, M., Dodds, M., Simner, B., Parkinson, M.J.: Starling: lightweight concurrency verification with views. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 544\u2013569. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_27"},{"key":"5_CR95","unstructured":"Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: ICML. PMLR, , vol. 97, pp. 6984\u20136994 (2019)"},{"key":"5_CR96","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.-K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: CCS, pp. 1789\u20131806. ACM (2017)","DOI":"10.1145\/3133956.3134043"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:43:24Z","timestamp":1672857804000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_5"}},"subtitle":["(Invited Paper)"],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":96,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_5","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)"}}]}}