{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:03:05Z","timestamp":1742925785095,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_3","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"34-54","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Effective Bug Finding in C Programs with Shape and Effect Abstractions"],"prefix":"10.1007","author":[{"given":"Iago","family":"Abal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus","family":"Brabrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"3_CR1","unstructured":"Abal, I.: Shape-region and effect inference for C(IL). Technical report (2016)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Abal, I., Brabrand, C., Wasowski, A.: 42 variability bugs in the Linux kernel: A qualitative analysis. In: ASE 2014 (2014)","DOI":"10.1145\/2642937.2642990"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001 (2001)","DOI":"10.1145\/378795.378846"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: PASTE 2001 (2001)","DOI":"10.1145\/379605.379690"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: CAV 2001 (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Banning, J.P.: An efficient way to find the side effects of procedure calls and the aliases of variables. In: POPL 1979 (1979)","DOI":"10.1145\/567752.567756"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO 2005 (2005)","DOI":"10.1007\/11804192_6"},{"issue":"5","key":"3_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: POPL 2004 (2004)","DOI":"10.1145\/964001.964020"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Brown, F., N\u00f6tzli, A., Engler, D.: How to build static checking systems using orders of magnitude less code. In: ASPLOS 2016 (2016)","DOI":"10.1145\/2872362.2872364"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Brunel, J., Doligez, D., Hansen, R.R., Lawall, J.L., Muller, G.: A foundation for flow-based program matching: using temporal logic and model checking. In: POPL 2009 (2009)","DOI":"10.1145\/1594834.1480897"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Chen, Y., Wu, F., Yu, K., Zhang, L., Chen, Y., Yang, Y., Mao, J.: Instant bug testing service for Linux kernel. In: HPCC\/EUC 2013 (2013)","DOI":"10.1109\/HPCC.and.EUC.2013.347"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV 2000 (2000)","DOI":"10.1007\/10722167_15"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Cooper, K.D., Kennedy, K.: Efficient computation of flow insensitive interprocedural summary information. In: SIGPLAN 1984 (1984)","DOI":"10.1145\/502874.502898"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Cooper, K.D., Kennedy, K.: Interprocedural side-effect analysis in linear time. In: PLDI 1988 (1988)","DOI":"10.1145\/53990.53996"},{"issue":"3","key":"3_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does Astr\u00e9e scale up? Form. Methods Syst. Des. 35(3), 229\u2013264 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL 1982 (1982)","DOI":"10.1145\/582153.582176"},{"key":"3_CR19","volume-title":"Checking C Programs with Lint","author":"IF Darwin","year":"1986","unstructured":"Darwin, I.F.: Checking C Programs with Lint. O\u2019Reilly, Sebastopol (1986)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Das, M.: Unification-based pointer analysis with directional assignments. In: PLDI 2000 (2000)","DOI":"10.1145\/349299.349309"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: OSDI 2000 (2000)","DOI":"10.21236\/ADA419626"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-45099-3_10","volume-title":"Static Analysis","author":"JS Foster","year":"2000","unstructured":"Foster, J.S., F\u00e4hndrich, M., Aiken, A.: Polymorphic versus monomorphic flow-insensitive points-to analysis for C. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 175\u2013198. Springer, Heidelberg (2000). doi:\n                    10.1007\/978-3-540-45099-3_10"},{"issue":"6","key":"3_CR23","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1145\/1186632.1186635","volume":"28","author":"JS Foster","year":"2006","unstructured":"Foster, J.S., Johnson, R., Kodumal, J., Aiken, A.: Flow-insensitive type qualifiers. ACM Trans. Program. Lang. Syst. 28(6), 1035\u20131087 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: PLDI 2002 (2002)","DOI":"10.1145\/512530.512531"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: PLDI 2002. ACM (2002)","DOI":"10.1145\/512537.512539"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: Haven\u2019t we solved this problem yet? In: PASTE 2001 (2001)","DOI":"10.1145\/379605.379665"},{"key":"3_CR27","unstructured":"Johnson, R., Wagner, D.: Finding user\/kernel pointer bugs with type inference. In: Proceedings of the 13th Conference on USENIX Security Symposium, vol. 13, SSYM 2004, pp. 9\u20139, Berkeley, CA, USA, 2004. USENIX Association (2004)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Jouvelot, P., Gifford, D.: Algebraic reconstruction of types and effects. POPL 1991 (1991)","DOI":"10.1145\/99583.99623"},{"key":"3_CR29","unstructured":"Jouvelot, P., Talpin, J.-P.: The type and effect discipline (1993)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Shan, C.-C.: Lightweight monadic regions. Haskell (2008)","DOI":"10.1145\/1411286.1411288"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Lawall, J., Laurie, B., Hansen, R.R., Palix, N., Muller, G.: Finding error handling bugs in openssl using coccinelle. In: EDCC 2010 (2010)","DOI":"10.1109\/EDCC.2010.31"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Koka: programming with Row polymorphic Effect Types. In: MSFP 2014 (2014)","DOI":"10.4204\/EPTCS.153.8"},{"issue":"2","key":"3_CR33","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/2644805","volume":"58","author":"B Livshits","year":"2015","unstructured":"Livshits, B., Sridharan, M., Smaragdakis, Y., Lhot\u00e1k, O., Amaral, J.N., Chang, B.-Y.E., Guyer, S.Z., Khedker, U.P., M\u00f8ller, A., Vardoulakis, D.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44\u201346 (2015)","journal-title":"Commun. ACM"},{"key":"3_CR34","unstructured":"Lucassen, J.M., Types, E.: Towards the integration of functional and imperative programming. Ph.D. thesis (1987)"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL 1988 (1988)","DOI":"10.1145\/73560.73564"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: CC 2002 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48092-7_6","volume-title":"Correct System Design","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 114\u2013136. Springer, Heidelberg (1999). doi:\n                    10.1007\/3-540-48092-7_6"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Padioleau, Y., Lawall, J.L., Muller, G.: Understanding collateral evolution in Linux device drivers. In: EuroSys 2006 (2006)","DOI":"10.1145\/1217935.1217942"},{"key":"3_CR39","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2619090","volume":"32","author":"N Palix","year":"2014","unstructured":"Palix, N., Thomas, G., Saha, S., Calv\u00e8s, C., Muller, G., Lawall, J.: Faults in Linux 2.6. ACM Trans. Comput. Syst. 32, 4:1\u20134:40 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: Locksmith: context-sensitive correlation analysis for race detection. In: PLDI 2006 (2006)","DOI":"10.1145\/1133981.1134019"},{"key":"3_CR41","unstructured":"Remy, D.: Type inference for records in a natural extension of ML. In: Theoretical Aspects Of Object-Oriented Programming. MIT Press (1993)"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995 (1995)","DOI":"10.1145\/199448.199462"},{"issue":"1","key":"3_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000014","volume":"2","author":"Y Smaragdakis","year":"2015","unstructured":"Smaragdakis, Y., Balatsouras, G.: Pointer analysis. Found. Trends Program. Lang. 2(1), 1\u201369 (2015)","journal-title":"Found. Trends Program. Lang."},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis by type inference of programs with structures and unions. In: CC 1996 (1996)","DOI":"10.1007\/3-540-61053-7_58"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: POPL 1996 (1996)","DOI":"10.1145\/237721.237727"},{"issue":"1","key":"3_CR46","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"2","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 2(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR47","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1017\/S0956796800000393","volume":"2","author":"J-P Talpin","year":"1992","unstructured":"Talpin, J.-P., Jouvelot, P.: Polymorphic type, region and effect inference. J. Funct. Program. 2, 7 (1992)","journal-title":"J. Funct. Program."},{"issue":"1","key":"3_CR48","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M Tofte","year":"1990","unstructured":"Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1\u201334 (1990)","journal-title":"Inf. Comput."},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value \n                    \n                      \n                    \n                    $$\\lambda $$\n                  -calculus using a stack of regions. In: POPL 1994 (1994)","DOI":"10.1145\/174675.177855"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Wright, D.A.: A new technique for strictness analysis. In: TAPSOFT 1991 (1991)","DOI":"10.1007\/3540539816_70"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: POPL 2005 (2005)","DOI":"10.1145\/1040305.1040334"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Yong, S.H., Horwitz, S., Reps, T.: Pointer analysis for programs with structures and casting. In: PLDI 1999 (1999)","DOI":"10.1145\/301618.301647"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:11:37Z","timestamp":1558318297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.researchr.org\/home\/VMCAI-2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}