{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:29:19Z","timestamp":1770272959724,"version":"3.49.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,11,21]],"date-time":"2017-11-21T00:00:00Z","timestamp":1511222400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100004358","name":"Samsung","doi-asserted-by":"publisher","award":["SRFC-IT1502-07"],"award-info":[{"award-number":["SRFC-IT1502-07"]}],"id":[{"id":"10.13039\/100004358","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003621","name":"Ministry of Science, ICT and Future Planning","doi-asserted-by":"publisher","award":["R0190-16-2011"],"award-info":[{"award-number":["R0190-16-2011"]}],"id":[{"id":"10.13039\/501100003621","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003621","name":"Ministry of Science, ICT and Future Planning","doi-asserted-by":"publisher","award":["B0717-16-0098"],"award-info":[{"award-number":["B0717-16-0098"]}],"id":[{"id":"10.13039\/501100003621","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["NRF-2016R1C1B2014062"],"award-info":[{"award-number":["NRF-2016R1C1B2014062"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10703-017-0306-7","type":"journal-article","created":{"date-parts":[[2017,11,21]],"date-time":"2017-11-21T08:56:56Z","timestamp":1511254616000},"page":"189-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Learning analysis strategies for octagon and context sensitivity from labeled data generated by static analyses"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2671-0142","authenticated-orcid":false,"given":"Kihong","family":"Heo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hakjoo","family":"Oh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,21]]},"reference":[{"key":"306_CR1","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: PLDI","DOI":"10.1145\/781151.781153"},{"key":"306_CR2","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman L (2001) Random forests. Machine Learning 45:5\u201332","journal-title":"Machine Learning"},{"key":"306_CR3","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL","DOI":"10.1145\/512760.512770"},{"key":"306_CR4","doi-asserted-by":"crossref","unstructured":"Garg P, Neider D, Madhusudan P, Roth D (2016) Learning invariants using decision trees and implication counterexamples. In: POPL, pp 499\u2013512","DOI":"10.1145\/2837614.2837664"},{"key":"306_CR5","doi-asserted-by":"crossref","unstructured":"Grigore R, Yang H (2016) Abstraction refinement guided by a learnt probabilistic model. In: POPL","DOI":"10.1145\/2837614.2837663"},{"key":"306_CR6","doi-asserted-by":"crossref","unstructured":"Heo K, Oh H, Yang H (2016) Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In: SAS","DOI":"10.1007\/978-3-662-53413-7_12"},{"key":"306_CR7","doi-asserted-by":"crossref","unstructured":"Jeannet B, Min\u00e9 A (2009) Apron: a library of numerical abstract domains for static analysis. In: CAV","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"306_CR8","doi-asserted-by":"crossref","unstructured":"Mangal R, Zhang X, Nori AV, Naik M (2015) A user-guided approach to program analysis. In: ESEC\/FSE, pp 462\u2013473","DOI":"10.1145\/2786805.2786851"},{"key":"306_CR9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. Higher-Order Symb Comput 19:31\u2013100","journal-title":"Higher-Order Symb Comput"},{"key":"306_CR10","volume-title":"Machine learning","author":"TM Mitchell","year":"1997","unstructured":"Mitchell TM (1997) Machine learning. McGraw-Hill Inc, New York"},{"key":"306_CR11","unstructured":"Murphy KP (2012) Machine learning: a probabilistic perspective (adaptive computation and machine learning series). Mit Press ISBN"},{"key":"306_CR12","unstructured":"Nori AV, Sharma R (2013) Termination proofs from tests. In: FSE, pp 246\u2013256"},{"key":"306_CR13","doi-asserted-by":"crossref","unstructured":"Octeau D, Jha S, Dering M, McDaniel P, Bartel A, Li L, Klein J, Le Traon Y (2016) Combining static analysis with probabilistic models to enable market-scale android inter-component analysis. In: POPL, pp 469\u2013484","DOI":"10.1145\/2837614.2837661"},{"key":"306_CR14","doi-asserted-by":"publisher","unstructured":"Oh H, Heo K, Lee W, Lee W, Park D, Kang J, Yi K (2014) Global sparse analysis framework. ACM Trans Program Lang Syst 36(3):8:1\u20138:44. https:\/\/doi.org\/10.1145\/2590811","DOI":"10.1145\/2590811"},{"key":"306_CR15","doi-asserted-by":"crossref","unstructured":"Oh H, Heo K, Lee W, Lee W, Yi K (2012) Design and implementation of sparse global analyses for C-like languages. In: PLDI","DOI":"10.1145\/2254064.2254092"},{"key":"306_CR16","doi-asserted-by":"crossref","unstructured":"Oh H, Lee W, Heo K, Yang H, Yi K (2014) Selective context-sensitivity guided by impact pre-analysis. In: PLDI","DOI":"10.1145\/2594291.2594318"},{"key":"306_CR17","doi-asserted-by":"crossref","unstructured":"Oh H, Yang H, Yi K (2015) Learning a strategy for adapting a program analysis via bayesian optimisation. In: OOPSLA","DOI":"10.1145\/2814270.2814309"},{"key":"306_CR18","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa F, Varoquaux G, Gramfort A, Michel V, Thirion B, Grisel O, Blondel M, Prettenhofer P, Weiss R, Dubourg V, Vanderplas J, Passos A, Cournapeau D, Brucher M, Perrot M, Duchesnay \u00c9 (2011) Scikit-learn: machine learning in python. J Mach Learn Res 12:2825\u20132830","journal-title":"J Mach Learn Res"},{"key":"306_CR19","doi-asserted-by":"crossref","unstructured":"Raychev V, Bielik P, Vechev MT, Krause A (2016) Learning programs from noisy data. In: POPL, pp. 761\u2013774","DOI":"10.1145\/2837614.2837671"},{"key":"306_CR20","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Chaudhuri S, Ivan\u010di\u0107 F, Gupta A (2008) Dynamic inference of likely data preconditions over predicates by tree learning. In: ISSTA, pp 295\u2013306","DOI":"10.1145\/1390630.1390666"},{"key":"306_CR21","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Ivan\u010di\u0107 F, Gupta A (2008) Mining library specifications using inductive logic programming. In: ICSE, pp 131\u2013140","DOI":"10.1145\/1368088.1368107"},{"key":"306_CR22","first-page":"189","volume-title":"Program flow analysis: theory and applications","author":"M Sharir","year":"1981","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. Program flow analysis: theory and applications. Prentice-Hall, Englewood Cliffs, pp 189\u2013234"},{"key":"306_CR23","doi-asserted-by":"publisher","unstructured":"Sharma R, Gupta S, Hariharan B, Aiken A, Liang P, Nori AV (2013) A data driven approach for algebraic loop invariants. In: ESOP, pp 574\u2013592. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"306_CR24","doi-asserted-by":"crossref","unstructured":"Sharma R, Gupta S, Hariharan B, Aiken A, Nori AV (2013) Verification as learning geometric concepts. In: SAS, pp 388\u2013411","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"306_CR25","doi-asserted-by":"crossref","unstructured":"Sharma R, Nori AV, Aiken A (2012) Interpolants as classifiers. In: CAV, pp 71\u201387","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"306_CR26","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M (2015) Making Numerical Program Analysis Fast. In: PLDI","DOI":"10.1145\/2737924.2738000"},{"key":"306_CR27","unstructured":"Sparrow: http:\/\/ropas.snu.ac.kr\/sparrow"},{"key":"306_CR28","doi-asserted-by":"crossref","unstructured":"Venet A, Brat G (2004) Precise and efficient static array bound checking for large embedded C programs. In: PLDI","DOI":"10.1145\/996841.996869"},{"issue":"2\u20133","key":"306_CR29","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/j.ipl.2006.11.004","volume":"102","author":"K Yi","year":"2007","unstructured":"Yi K, Choi H, Kim J, Kim Y (2007) An empirical study on classification methods for alarms from a bug-finding static C analyzer. Inf Process Lett 102(2\u20133):118\u2013123","journal-title":"Inf Process Lett"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0306-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0306-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0306-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T07:57:41Z","timestamp":1570348661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0306-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,21]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["306"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0306-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,21]]}}}