{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:18:08Z","timestamp":1784233088618,"version":"3.55.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["#1453386"],"award-info":[{"award-number":["#1453386"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["#FA8750-20-C-0208"],"award-info":[{"award-number":["#FA8750-20-C-0208"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>Several real-world libraries (e.g., reentrant locks, GUI frameworks, serialization libraries) require their clients to use the provided API in a manner that conforms to a context-free specification. Motivated by this observation, this paper describes a new technique for verifying the correct usage of context-free API protocols. The key idea underlying our technique is to over-approximate the program\u2019s feasible API call sequences using a context-free grammar (CFG) and then check language inclusion between this grammar and the specification. However, since this inclusion check may fail due to imprecision in the program\u2019s CFG abstraction, we propose a novel refinement technique to progressively improve the CFG. In particular, our method obtains counterexamples from CFG inclusion queries and uses them to introduce new non-terminals and productions to the grammar while still over-approximating the program\u2019s relevant behavior.<\/jats:p>\n                  <jats:p>We have implemented the proposed algorithm in a tool called CFPChecker and evaluate it on 10 popular Java applications that use at least one API with a context-free specification. Our evaluation shows that CFPChecker is able to verify correct usage of the API in clients that use it correctly and produces counterexamples for those that do not. We also compare our method against three relevant baselines and demonstrate that CFPChecker enables verification of safety properties that are beyond the reach of existing tools.<\/jats:p>","DOI":"10.1145\/3434298","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Verifying correct usage of context-free API protocols"],"prefix":"10.1145","volume":"5","author":[{"given":"Kostas","family":"Ferles","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jon","family":"Stephens","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_52"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_2_1_3_1","volume-title":"Laurie J. Hendren, Sascha Kuzins, Ondrej Lhot\u00e1k, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble.","author":"Allan Chris","year":"2005","unstructured":"Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie J. Hendren, Sascha Kuzins, Ondrej Lhot\u00e1k, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. 2005. Adding trace matching with free variables to AspectJ. In OOPSLA."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_1_5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Artho Cyrille","unstructured":"Cyrille Artho and Willem Visser. 2019. Java Pathfinder at SV-COMP 2019 (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Stefen (Eds.). Springer International Publishing, Cham, 224-228."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814228.2814229"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629343"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218063.1217943"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057391"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45139-0_7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.49"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Kevin Bierhof and Jonathan Aldrich. 2007. Modular typestate checking of aliased objects. ACM SIGPLAN Notices 42 10 ( 2007 ) 301-320.","DOI":"10.1145\/1297105.1297050"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_13"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806805"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0183-5"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73208-2_15"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL ( 2017 ), 30","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. 2017. Optimal Dyck reachability for data-dependence and alias analysis. Proceedings of the ACM on Programming Languages 2, POPL ( 2017 ), 30."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586142"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Noam Chomsky. 1959. On certain formal properties of grammars. Information and control 2 2 ( 1959 ) 137-167.","DOI":"10.1016\/S0019-9958(59)90362-6"},{"key":"e_1_2_1_23_1","volume-title":"SMTInterpol: An Interpolating SMT Solver","author":"Christ J\u00fcrgen","unstructured":"J\u00fcrgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In Model Checking Software, Alastair Donaldson and David Parker (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 248-254."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964021"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"e_1_2_1_28_1","unstructured":"John E Hopcroft. 2008. Introduction to automata theory languages and computation. Pearson Education India."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.72"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.39"},{"key":"e_1_2_1_32_1","volume-title":"JayHorn: A Framework for Verifying Java programs","author":"Kahsai Temesghen","unstructured":"Temesghen Kahsai, Philipp R\u00fcmmer, Huascar Sanchez, and Martin Sch\u00e4f. 2016. JayHorn: A Framework for Verifying Java programs. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 352-358."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1966.22"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Patrick Lam Viktor Kuncak and Martin Rinard. 2004. Generalized typestate checking using set interfaces and pluggable analyses. ACM SIGPLAN Notices 39 3 ( 2004 ) 46-55.","DOI":"10.1145\/981009.981016"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386021"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_2_1_37_1","volume-title":"Fundamental Approaches to Software Engineering, Juan de Lara and Andrea Zisman (Eds.)","author":"Long Zhenyue","unstructured":"Zhenyue Long, Georgel Calin, Rupak Majumdar, and Roland Meyer. 2012. Language-Theoretic Abstraction Refinement. In Fundamental Approaches to Software Engineering, Juan de Lara and Andrea Zisman (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 362-376."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814304"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Patrick O'Neil Meredith Dongyun Jin Feng Chen and Grigore Ro\u015fu. 2010. Eficient monitoring of parametric context-free patterns. Automated Software Engineering 17 2 ( 2010 ) 149-180.","DOI":"10.1007\/s10515-010-0063-y"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Tmima Olshansky and Amir Pnueli. 1977. A direct algorithm for checking equivalence of LL (k) grammars. Theoretical Computer Science 4 3 ( 1977 ) 321-349.","DOI":"10.1016\/0304-3975(77)90016-0"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227127"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227127"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250748"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_1_52_1","volume-title":"Typestate: A programming language concept for enhancing software reliability","author":"Strom Robert E","year":"1986","unstructured":"Robert E Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering 1 ( 1986 ), 157-171."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676997"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_27"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_56_1","unstructured":"Salvatore La Torre Margherita Napoli and Gennaro Parlato. 2013. On Multi-stack Visibly Pushdown Languages."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/781995.782008"},{"key":"e_1_2_1_58_1","first-page":"439","volume-title":"Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE '81)","author":"Weiser Mark","year":"1981","unstructured":"Mark Weiser. 1981. Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE '81). IEEE Press, 439-449."},{"key":"e_1_2_1_59_1","volume-title":"European Conference on Object-Oriented Programming. Springer, 98-122","author":"Xu Guoqing","year":"2009","unstructured":"Guoqing Xu, Atanas Rountev, and Manu Sridharan. 2009. Scaling CFL-reachability-based points-to analysis using contextsensitive must-not-alias analysis. In European Conference on Object-Oriented Programming. Springer, 98-122."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180227"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462159"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009848"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434298","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434298","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434298","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:27:16Z","timestamp":1781854036000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434298"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434298"],"URL":"https:\/\/doi.org\/10.1145\/3434298","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}