{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:02:53Z","timestamp":1773478973865,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":86,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,7,18]]},"DOI":"10.1145\/3533767.3534381","type":"proceedings-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T14:28:50Z","timestamp":1657895330000},"page":"352-364","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Almost correct invariants: synthesizing inductive invariants by fuzzing proofs"],"prefix":"10.1145","author":[{"given":"Sumit","family":"Lahiri","sequence":"first","affiliation":[{"name":"IIT Kanpur, India"}]},{"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[{"name":"IIT Kanpur, India"}]}],"member":"320","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Hacker\u2019s Delight","unstructured":"[n.d.]. Hacker\u2019s Delight , Second Edition [Book]. https:\/\/dl.acm.org\/doi\/book\/10.5555\/2462741 [n.d.]. Hacker\u2019s Delight, Second Edition [Book]. https:\/\/dl.acm.org\/doi\/book\/10.5555\/2462741"},{"key":"e_1_3_2_1_2_1","unstructured":"AFL. 2020. american fuzzy lop. https:\/\/lcamtuf.coredump.cx\/afl\/ \t\t\t\t\t  AFL. 2020. american fuzzy lop. https:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"e_1_3_2_1_4_1","unstructured":"Miltiadis Allamanis Marc Brockschmidt and Mahmoud Khademi. 2018. Learning to Represent Programs with Graphs. In In Proceeding of ICLR. https:\/\/openreview.net\/forum?id=BJOFETxR- \t\t\t\t\t  Miltiadis Allamanis Marc Brockschmidt and Mahmoud Khademi. 2018. Learning to Represent Programs with Graphs. In In Proceeding of ICLR. https:\/\/openreview.net\/forum?id=BJOFETxR-"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 29th Annual ACM\/IEEE International Symposium on Microarchitecture (MICRO 29)","author":"Ball Thomas","year":"1867","unstructured":"Thomas Ball and James R. Larus . 1996. Efficient Path Profiling . In Proceedings of the 29th Annual ACM\/IEEE International Symposium on Microarchitecture (MICRO 29) . 46\u201357. isbn:08 1867 6418 Thomas Ball and James R. Larus. 1996. Efficient Path Profiling. In Proceedings of the 29th Annual ACM\/IEEE International Symposium on Microarchitecture (MICRO 29). 46\u201357. isbn:0818676418"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984014"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462188"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Marc Brockschmidt Yuxin Chen Pushmeet Kohli Siddharth Krishna and Daniel Tarlow. 2017. Learning shape analysis. In SAS\u201917. 66\u201387. \t\t\t\t\t  Marc Brockschmidt Yuxin Chen Pushmeet Kohli Siddharth Krishna and Daniel Tarlow. 2017. Learning shape analysis. In SAS\u201917. 66\u201387.","DOI":"10.1007\/978-3-319-66706-5_4"},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 8th USENIX Conference OSDI (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference OSDI (OSDI\u201908) . USENIX Association, 209\u2013224. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference OSDI (OSDI\u201908). USENIX Association, 209\u2013224."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/226"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00046"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 2013 IEEE\/ACM International Symposium on CGO\u201913","author":"Chouhan R.","unstructured":"R. Chouhan , S. Roy , and S. Baswana . 2013. Pertinent path profiling: Tracking interactions among relevant statements . In Proceedings of the 2013 IEEE\/ACM International Symposium on CGO\u201913 . 1\u201312. R. Chouhan, S. Roy, and S. Baswana. 2013. Pertinent path profiling: Tracking interactions among relevant statements. In Proceedings of the 2013 IEEE\/ACM International Symposium on CGO\u201913. 1\u201312."},{"key":"e_1_3_2_1_15_1","unstructured":"CodeProject. 2006. Using Inline Assembly in C\/C++ - CodeProject. https:\/\/www.codeproject.com\/Articles\/15971\/Using-Inline-Assembly-in-C-C \t\t\t\t\t  CodeProject. 2006. Using Inline Assembly in C\/C++ - CodeProject. https:\/\/www.codeproject.com\/Articles\/15971\/Using-Inline-Assembly-in-C-C"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Michael Col\u00f3n S. Sankaranarayanan and H. B. Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV\u201913. \t\t\t\t\t  Michael Col\u00f3n S. Sankaranarayanan and H. B. Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV\u201913.","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_17_1","unstructured":"Greatest common divisor. [n.d.]. Greatest common divisor - Rosetta Code. http:\/\/rosettacode.org\/wiki\/Greatest_common_divisor \t\t\t\t\t  Greatest common divisor. [n.d.]. Greatest common divisor - Rosetta Code. http:\/\/rosettacode.org\/wiki\/Greatest_common_divisor"},{"key":"e_1_3_2_1_18_1","unstructured":"CP-Algorithms-Factorial. 2014. Factorial modulo P - Competitive Programming Algorithms. https:\/\/cp-algorithms.com\/algebra\/factorial-modulo.html \t\t\t\t\t  CP-Algorithms-Factorial. 2014. Factorial modulo P - Competitive Programming Algorithms. https:\/\/cp-algorithms.com\/algebra\/factorial-modulo.html"},{"key":"e_1_3_2_1_19_1","unstructured":"CP-Algorithms-GCD. 2014. Euclidean algorithm for computing the greatest common divisor - Competitive Programming Algorithms. https:\/\/cp-algorithms.com\/algebra\/euclid-algorithm.html \t\t\t\t\t  CP-Algorithms-GCD. 2014. Euclidean algorithm for computing the greatest common divisor - Competitive Programming Algorithms. https:\/\/cp-algorithms.com\/algebra\/euclid-algorithm.html"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_21_1","volume-title":"Discriminative Embeddings of Latent Variable Models for Structured Data. In In Proceedings of The 33rd ICML. 2702\u20132711","author":"Dai Hanjun","year":"2016","unstructured":"Hanjun Dai , Bo Dai , and Le Song . 2016 . Discriminative Embeddings of Latent Variable Models for Structured Data. In In Proceedings of The 33rd ICML. 2702\u20132711 . http:\/\/proceedings.mlr.press\/v48\/daib16.html Hanjun Dai, Bo Dai, and Le Song. 2016. Discriminative Embeddings of Latent Variable Models for Structured Data. In In Proceedings of The 33rd ICML. 2702\u20132711. http:\/\/proceedings.mlr.press\/v48\/daib16.html"},{"key":"e_1_3_2_1_22_1","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. isbn:978-3-540-78800-3 \t\t\t\t\t  Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. isbn:978-3-540-78800-3"},{"key":"e_1_3_2_1_23_1","unstructured":"Dana Drachsler-Cohen Sharon Shoham and Eran Yahav. 2017. Synthesis with Abstract Examples. In CAV. 254\u2013278. isbn:978-3-319-63387-9 \t\t\t\t\t  Dana Drachsler-Cohen Sharon Shoham and Eran Yahav. 2017. Synthesis with Abstract Examples. In CAV. 254\u2013278. isbn:978-3-319-63387-9"},{"key":"e_1_3_2_1_24_1","volume-title":"Seshia","author":"Dreossi Tommaso","year":"2019","unstructured":"Tommaso Dreossi , Daniel J. Fremont , Shromona Ghosh , Edward Kim , Hadi Ravanbakhsh , Marcell Vazquez-Chanlatte , and Sanjit A . Seshia . 2019 . VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. In CAV\u2019 19. isbn:978-3-030-25540-4 Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. 2019. VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. In CAV\u201919. isbn:978-3-030-25540-4"},{"key":"e_1_3_2_1_25_1","unstructured":"Parasara Sridhar Duggirala Sayan Mitra Mahesh Viswanathan and Matthew Potok. 2015. C2E2: A Verification Tool for Stateflow Models. In Tools and Algorithms for the Construction and Analysis of Systems. isbn:978-3-662-46681-0 \t\t\t\t\t  Parasara Sridhar Duggirala Sayan Mitra Mahesh Viswanathan and Matthew Potok. 2015. C2E2: A Verification Tool for Stateflow Models. In Tools and Algorithms for the Construction and Analysis of Systems. isbn:978-3-662-46681-0"},{"key":"e_1_3_2_1_26_1","unstructured":"David K Duvenaud Dougal Maclaurin Jorge Iparraguirre Rafael Bombarell Timothy Hirzel Alan Aspuru-Guzik and Ryan P Adams. 2015. Convolutional Networks on Graphs for Learning Molecular Fingerprints. In In Proceeding of NIPS\u201915. https:\/\/proceedings.neurips.cc\/paper\/2015\/file\/f9be311e65d81a9ad8150a60844bb94c-Paper.pdf \t\t\t\t\t  David K Duvenaud Dougal Maclaurin Jorge Iparraguirre Rafael Bombarell Timothy Hirzel Alan Aspuru-Guzik and Ryan P Adams. 2015. Convolutional Networks on Graphs for Learning Molecular Fingerprints. In In Proceeding of NIPS\u201915. https:\/\/proceedings.neurips.cc\/paper\/2015\/file\/f9be311e65d81a9ad8150a60844bb94c-Paper.pdf"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_7"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Pranav Garg Christof L\u00f6ding P. Madhusudan and Daniel Neider. 2014. ICE:\u00a0A\u00a0Robust\u00a0Framework\u00a0for\u00a0Learning\u00a0Invariants. In CAV. 69\u201387. \t\t\t\t\t  Pranav Garg Christof L\u00f6ding P. Madhusudan and Daniel Neider. 2014. ICE:\u00a0A\u00a0Robust\u00a0Framework\u00a0for\u00a0Learning\u00a0Invariants. In CAV. 69\u201387.","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_34_1","volume-title":"Meel","author":"Golia Priyanka","year":"2020","unstructured":"Priyanka Golia , Subhajit Roy , and Kuldeep S . Meel . 2020 . Manthan : A Data-Driven Approach for Boolean Function Synthesis. In CAV\u2019 20. 611\u2013633. Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel. 2020. Manthan: A Data-Driven Approach for Boolean Function Synthesis. In CAV\u201920. 611\u2013633."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/261"},{"key":"e_1_3_2_1_36_1","volume-title":"Meel","author":"Golia Priyanka","year":"2021","unstructured":"Priyanka Golia , Subhajit Roy , Friedrich Slivovsky , and Kuldeep S . Meel . 2021 . Engineering an Efficient Boolean Functional Synthesis Engine. In ICCAD. Priyanka Golia, Subhajit Roy, Friedrich Slivovsky, and Kuldeep S. Meel. 2021. Engineering an Efficient Boolean Functional Synthesis Engine. In ICCAD."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993506"},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 22nd USENIX Conference on Security (SEC\u201913)","author":"Haller Istvan","year":"2013","unstructured":"Istvan Haller , Asia Slowinska , Matthias Neugschwandtner , and Herbert Bos . 2013 . Dowsing for Overflows: A Guided Fuzzer to Find Buffer Boundary Violations . In Proceedings of the 22nd USENIX Conference on Security (SEC\u201913) . USENIX Association, 49\u201364. isbn:978 1931971034 Istvan Haller, Asia Slowinska, Matthias Neugschwandtner, and Herbert Bos. 2013. Dowsing for Overflows: A Guided Fuzzer to Find Buffer Boundary Violations. In Proceedings of the 22nd USENIX Conference on Security (SEC\u201913). USENIX Association, 49\u201364. isbn:9781931971034"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_40_1","unstructured":"Honggfuzz. 2020. Honggfuzz. https:\/\/honggfuzz.dev\/ \t\t\t\t\t  Honggfuzz. 2020. Honggfuzz. https:\/\/honggfuzz.dev\/"},{"key":"e_1_3_2_1_41_1","volume-title":"Foster","author":"Jeon Jinseong","year":"2015","unstructured":"Jinseong Jeon , Xiaokang Qiu , Armando Solar-Lezama , and Jeffrey S . Foster . 2015 . Adaptive Concretization for Parallel Program Synthesis. In CAV. 377\u2013394. isbn:978-3-319-21668-3 Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, and Jeffrey S. Foster. 2015. Adaptive Concretization for Parallel Program Synthesis. In CAV. 377\u2013394. isbn:978-3-319-21668-3"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0269-8"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_44_1","unstructured":"Temesghen Kahsai Yeting Ge and Cesare Tinelli. 2011. Instantiation-Based Invariant Discovery. NFM\u201911. 15 pages. isbn:9783642203978 \t\t\t\t\t  Temesghen Kahsai Yeting Ge and Cesare Tinelli. 2011. Instantiation-Based Invariant Discovery. NFM\u201911. 15 pages. isbn:9783642203978"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6534229"},{"key":"e_1_3_2_1_46_1","unstructured":"Sumit Lahiri and Subhajit Roy. 2022. Docker Image for Achar Tool.. https:\/\/hub.docker.com\/repository\/docker\/acharver1\/achar \t\t\t\t\t  Sumit Lahiri and Subhajit Roy. 2022. Docker Image for Achar Tool.. https:\/\/hub.docker.com\/repository\/docker\/acharver1\/achar"},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the 31st ICML -","volume":"32","author":"Le Quoc","year":"2014","unstructured":"Quoc Le and Tomas Mikolov . 2014 . Distributed Representations of Sentences and Documents . In Proceedings of the 31st ICML - Volume 32 (ICML\u201914). JMLR.org, II\u20131188\u2013II\u20131196. Quoc Le and Tomas Mikolov. 2014. Distributed Representations of Sentences and Documents. In Proceedings of the 31st ICML - Volume 32 (ICML\u201914). JMLR.org, II\u20131188\u2013II\u20131196."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738002"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/W14-1618"},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the 27th NIPS -","volume":"2","author":"Levy Omer","year":"2014","unstructured":"Omer Levy and Yoav Goldberg . 2014 . Neural Word Embedding as Implicit Matrix Factorization . In Proceedings of the 27th NIPS - Volume 2 (NIPS\u201914). MIT Press. Omer Levy and Yoav Goldberg. 2014. Neural Word Embedding as Implicit Matrix Factorization. In Proceedings of the 27th NIPS - Volume 2 (NIPS\u201914). MIT Press."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106295"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699026.2699098"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"e_1_3_2_1_56_1","unstructured":"Elements of Programming Interviews. [n.d.]. Elements of Programming Interviews. https:\/\/elementsofprogramminginterviews.com\/ \t\t\t\t\t  Elements of Programming Interviews. [n.d.]. Elements of Programming Interviews. https:\/\/elementsofprogramminginterviews.com\/"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133889"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"crossref","unstructured":"Sanjay Rawat Vivek Jain Ashish Kumar L. Cojocar Cristiano Giuffrida and H. Bos. 2017. VUzzer: Application-aware Evolutionary Fuzzing. In NDSS. \t\t\t\t\t  Sanjay Rawat Vivek Jain Ashish Kumar L. Cojocar Cristiano Giuffrida and H. Bos. 2017. VUzzer: Application-aware Evolutionary Fuzzing. In NDSS.","DOI":"10.14722\/ndss.2017.23404"},{"key":"e_1_3_2_1_62_1","unstructured":"Integer Cube Root. [n.d.]. Integer Cube Root - Hacker\u2019s Delight [Book]. \t\t\t\t\t  Integer Cube Root. [n.d.]. Integer Cube Root - Hacker\u2019s Delight [Book]."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_9"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00060"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236084"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.11"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.2008.2005605"},{"key":"e_1_3_2_1_69_1","unstructured":"Fibonacci sequence. [n.d.]. Fibonacci sequence - Rosetta Code. http:\/\/rosettacode.org\/wiki\/Fibonacci_sequence \t\t\t\t\t  Fibonacci sequence. [n.d.]. Fibonacci sequence - Rosetta Code. http:\/\/rosettacode.org\/wiki\/Fibonacci_sequence"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_1_71_1","volume-title":"Nori","author":"Sharma Rahul","year":"2013","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , Percy Liang , and Aditya V . Nori . 2013 . A Data Driven Approach for Algebraic Loop Invariants. In Programming Languages and Systems . 574\u2013592. Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori. 2013. A Data Driven Approach for Algebraic Loop Invariants. In Programming Languages and Systems. 574\u2013592."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"crossref","unstructured":"Rahul Sharma Aditya V. Nori and Alex Aiken. 2012. Interpolants as Classifiers. In CAV. 71\u201387. \t\t\t\t\t  Rahul Sharma Aditya V. Nori and Alex Aiken. 2012. Interpolants as Classifiers. In CAV. 71\u201387.","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_1_73_1","volume-title":"Proceedings of the 32nd International Conference NIPS (NIPS\u201918)","author":"Si Xujie","year":"2018","unstructured":"Xujie Si , Hanjun Dai , Mukund Raghothaman , Mayur Naik , and Le Song . 2018 . Learning Loop Invariants for Program Verification . In Proceedings of the 32nd International Conference NIPS (NIPS\u201918) . Curran Associates Inc., 7762\u20137773. Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning Loop Invariants for Program Verification. In Proceedings of the 32nd International Conference NIPS (NIPS\u201918). Curran Associates Inc., 7762\u20137773."},{"key":"e_1_3_2_1_74_1","unstructured":"Xujie Si Aaditya Naik Hanjun Dai Mayur Naik and Le Song. 2020. Code2Inv: A Deep Learning Framework for Program Verification. In CAV. \t\t\t\t\t  Xujie Si Aaditya Naik Hanjun Dai Mayur Naik and Le Song. 2020. Code2Inv: A Deep Learning Framework for Program Verification. In CAV."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.29007\/2ndp"},{"key":"e_1_3_2_1_76_1","unstructured":"Integer square root. 2021. Integer square root - Wikipedia. https:\/\/en.wikipedia.org\/wiki\/Integer_square_root \t\t\t\t\t  Integer square root. 2021. Integer square root - Wikipedia. https:\/\/en.wikipedia.org\/wiki\/Integer_square_root"},{"key":"e_1_3_2_1_77_1","unstructured":"SyGus. 2017. SyGuS-Comp 2017. https:\/\/sygus.org\/comp\/2017\/ \t\t\t\t\t  SyGus. 2017. SyGuS-Comp 2017. https:\/\/sygus.org\/comp\/2017\/"},{"key":"e_1_3_2_1_78_1","volume-title":"HOLL: Program Synthesis for Higher Order Logic Locking. In TACAS. 3\u201324. isbn:978-3-030-99524-9","author":"Takhar Gourav","year":"2022","unstructured":"Gourav Takhar , Ramesh Karri , Christian Pilato , and Subhajit Roy . 2022 . HOLL: Program Synthesis for Higher Order Logic Locking. In TACAS. 3\u201324. isbn:978-3-030-99524-9 Gourav Takhar, Ramesh Karri, Christian Pilato, and Subhajit Roy. 2022. HOLL: Program Synthesis for Higher Order Logic Locking. In TACAS. 3\u201324. isbn:978-3-030-99524-9"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377910"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106263"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"crossref","unstructured":"Sahil Verma and Subhajit Roy. 2022. Debug-localize-repair: a symbiotic construction for heap manipulations. In Formal Methods in System Design. \t\t\t\t\t  Sahil Verma and Subhajit Roy. 2022. Debug-localize-repair: a symbiotic construction for heap manipulations. In Formal Methods in System Design.","DOI":"10.1007\/s10703-021-00387-z"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.37"},{"key":"e_1_3_2_1_83_1","volume-title":"The Free Encyclopedia.","unstructured":"Wikipedia. 2021. John Selfridge \u2014 Wikipedia , The Free Encyclopedia. Wikipedia. 2021. John Selfridge \u2014 Wikipedia, The Free Encyclopedia."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2011.29"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908088"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"event":{"name":"ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual South Korea","acronym":"ISSTA '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534381","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3533767.3534381","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:40Z","timestamp":1750272220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534381"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":86,"alternative-id":["10.1145\/3533767.3534381","10.1145\/3533767"],"URL":"https:\/\/doi.org\/10.1145\/3533767.3534381","relation":{},"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"2022-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}