{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:29:49Z","timestamp":1680816589411},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,8,1]],"date-time":"2015-08-01T00:00:00Z","timestamp":1438387200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10703-015-0231-6","type":"journal-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T09:38:05Z","timestamp":1440409085000},"page":"120-157","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists"],"prefix":"10.1007","volume":"47","author":[{"given":"Pranav","family":"Garg","sequence":"first","affiliation":[]},{"given":"Christof","family":"L\u00f6ding","sequence":"additional","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,25]]},"reference":[{"key":"231_CR1","doi-asserted-by":"crossref","unstructured":"Alberti F, Bruttomesso R, Ghilardi S, Sharygina N (2012) SMT-based abstraction for arrays with interpolants. In: Madhusudan P, Seshia SA (eds) Computer Aided Verification\u201424th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 679\u2013685","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"231_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: CAV, pp 548\u2013562","DOI":"10.1007\/11513988_52"},{"issue":"2","key":"231_CR3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87\u2013106","journal-title":"Inf Comput"},{"key":"231_CR4","unstructured":"Bollig B, Katoen JP, Kern C, Leucker M, Neider D (2010) Piegdon, D.R.: libalf: The automata learning framework. In: CAV, Springer, Berlin, pp 360\u2013364"},{"key":"231_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Dragoi C, Enea C, Sighireanu M (2012) Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak V, Rybalchenko A (eds) VMCAI. Lecture notes in computer science, vol 7148. Springer, Berlin, pp 1\u201322","DOI":"10.1007\/978-3-642-27940-9_1"},{"key":"231_CR6","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt DA (eds) VMCAI. Lecture notes in computer science, vol 6538. Springer, Berlin, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"231_CR7","unstructured":"Bradley AR, Manna Z, Sipma HB (2006) What\u2019s decidable about arrays? In: Emerson EA, Namjoshi KS (eds) VMCAI. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 427\u2013442"},{"key":"231_CR8","unstructured":"Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves R, van Renesse R (eds.) 8th USENIX symposium on operating systems design and implementation, OSDI 2008, Dec 8\u201310, USENIX Association, San Diego, pp 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"231_CR9","doi-asserted-by":"crossref","unstructured":"Chen YF, Farzan A, Clarke EM, Tsay YK,Wang BY (2009) Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski S, Philippou A (eds) TACAS. Lecture notes in computer science, vol 5505. Springer, Berlin, pp 31\u201345","DOI":"10.1007\/978-3-642-00768-2_3"},{"key":"231_CR10","doi-asserted-by":"crossref","unstructured":"Chen YF, Wang BY (2012) Learning boolean functions incrementally. In: In: Madhusudan P, Seshia SA (eds) Computer Aided Verification\u201424th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 55\u201370","DOI":"10.1007\/978-3-642-31424-7_10"},{"key":"231_CR11","doi-asserted-by":"crossref","unstructured":"Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) TACAS. Lecture notes in computer science, vol 2619. Springer, Berlin, pp 331\u2013346","DOI":"10.1007\/3-540-36577-X_24"},{"key":"231_CR12","doi-asserted-by":"crossref","unstructured":"Distefano D, O\u2019Hearn PW, Yang H (2006) A local shape analysis based on separation logic. In: Hermanns H, Palsberg J (eds.) Tools and algorithms for the construction and analysis of systems, 12th international conference, TACAS 2006 Held as Part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, Mar 25\u2013 Apr 2. Lecture notes in computer science, vol 3920, Springer, Berlin, pp 287\u2013302. Springer doi: 10.1007\/11691372_19","DOI":"10.1007\/11691372_19"},{"key":"231_CR13","doi-asserted-by":"crossref","unstructured":"Ernst MD, Czeisler A, Griswold WG, Notkin D (2000) Quickly detecting relevant program invariants. In: ICSE, pp 449\u2013458","DOI":"10.1109\/ICSE.2000.870435"},{"key":"231_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC\/Java. In: Oliveira JN, Zave P (eds) FME. Lecture notes in computer science, vol 2021. Springer, Berlin, pp 500\u2013517","DOI":"10.1007\/3-540-45251-6_29"},{"key":"231_CR15","doi-asserted-by":"crossref","unstructured":"Garg P, L\u00f6ding C, Madhusudan P, Neider D (2014) ICE: a robust framework for learning invariants. In: Biere A, Bloem R (eds) CAV. Lecture notes in computer science, vol 8559. Springer, Berlin, pp 69\u201387","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"231_CR16","doi-asserted-by":"crossref","unstructured":"Garg P, Madhusudan P, Parlato G (2013) Quantified data automata on skinny trees: An abstract domain for lists. In: Logozzo F, F\u00e4hndrich M (eds) SAS. Lecture notes in computer science, vol 7935. Springer, Berlin, pp 172\u2013193","DOI":"10.1007\/978-3-642-38856-9_11"},{"issue":"5","key":"231_CR17","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"EM Gold","year":"1967","unstructured":"Gold EM (1967) Language identification in the limit. Inf Control 10(5):447\u2013474","journal-title":"Inf Control"},{"key":"231_CR18","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games, vol 2500. Springer, Heidelberg","DOI":"10.1007\/3-540-36387-4"},{"key":"231_CR19","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan KL (2007) Array abstractions from proofs. In: Damm W, Hermanns H (eds) CAV. Lecture notes in computer science, vol 4590, Springer, Heidelberg, pp 193\u2013206","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"231_CR20","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An introduction to computational learning theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. MIT Press, Cambridge"},{"key":"231_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0171-7","volume-title":"Automata theory and its applications","author":"B Khoussainov","year":"2001","unstructured":"Khoussainov B, Nerode A (2001) Automata theory and its applications. Birkhauser, Boston"},{"key":"231_CR22","volume-title":"Switching and finite automata theory","author":"Z Kohavi","year":"1970","unstructured":"Kohavi Z (1970) Switching and finite automata theory. McGraw-Hill, Blacklick"},{"key":"231_CR23","doi-asserted-by":"crossref","unstructured":"Kong S, Jung Y, David C, Wang BY, Yi K (2010) Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: APLAS, pp 328\u2013343. Springer, Heidelberg","DOI":"10.1007\/978-3-642-17164-2_23"},{"key":"231_CR24","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Parlato G, Qiu X (2011) Decidable logics combining heap structures and data. In: Ball T, Sagiv M (eds.) POPL, pp 611\u2013622. ACM, New York","DOI":"10.1145\/1926385.1926455"},{"key":"231_CR25","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Qiu X (2011) Efficient decision procedures for heaps using STRAND. In: Yahav E (ed) SAS. Lecture notes in computer science, vol 6887. Springer, Berlin, pp 43\u201359","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"231_CR26","doi-asserted-by":"crossref","unstructured":"Mai H, Pek E, Xue H, King ST, Madhusudan P (2013) Verifying security invariants in ExpressOS. In: V. Sarkar, R. Bod\u00edk (eds.) ASPLOS, pp 293\u2013304. ACM, New York","DOI":"10.1145\/2451116.2451148"},{"key":"231_CR27","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr., Senzi F (eds.) CAV. Lecture notes in computer science, vol. 2725, Springer, Berlin, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"231_CR28","doi-asserted-by":"crossref","unstructured":"McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction andanalysis of systems. 14th international conference, TACAS 2008, held as part of thejoint European conferences on theory and practice of software, ETAPS 2008, Budapest, Mar 29\u2013Apr 6. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 413\u2013427","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"231_CR29","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N, (2007) Efficient E-matching for SMT solvers. In: Pfenning F (ed) CADE. Lecture notes in computer science,vol 4603. Springer, Berlin, pp 183\u2013198","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"231_CR30","doi-asserted-by":"crossref","unstructured":"de Moura, LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction andanalysis of systems. 14th international conference, TACAS 2008, held as part of thejoint European conferences on theory and practice of software, ETAPS 2008, Budapest, Mar 29\u2013Apr 6. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"231_CR31","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299\u2013347","journal-title":"Inf Comput"},{"issue":"3","key":"231_CR32","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Progr Lang Syst 24(3):217\u2013298","journal-title":"ACM Trans Progr Lang Syst"},{"key":"231_CR33","doi-asserted-by":"crossref","unstructured":"Seghir MN, Podelski A, Wies T (2009) Abstraction refinement for quantified array assertions. In: Palsberg J, Su Z (eds) SAS. Lecture notes in computer science, vol 5673. Springer, Berlin, pp 3\u201318","DOI":"10.1007\/978-3-642-03237-0_3"},{"key":"231_CR34","doi-asserted-by":"crossref","unstructured":"Sharma R, Nori AV, Aiken A (2012) Interpolants as classifiers. In: Madhusudan P, Seshia SA (eds) Computer Aided Verification\u201424th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 71\u201387","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"231_CR35","doi-asserted-by":"crossref","unstructured":"Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Hind M, Diwan A (eds.) PLDI, pp 223\u2013234. ACM, New York","DOI":"10.1145\/1542476.1542501"},{"key":"231_CR36","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of formal language theory","author":"W Thomas","year":"1997","unstructured":"Thomas W (1997) Languages, automata, and logic. In: Rozenberg G, Salomaa A (eds) Handbook of formal language theory, vol III. Springer, Heidelberg, pp 389\u2013455"},{"key":"231_CR37","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, IEEE Computer Society, pp 332\u2013344"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0231-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0231-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0231-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T19:17:25Z","timestamp":1567106245000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0231-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["231"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0231-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8]]}}}