https://dl.acm.org/doi/10.1145/3652588.3663324 skip to main content ACM Digital Library home ACM Association for Computing Machinery corporate logo * Advanced Search * Browse * About * + Sign in + Register * * Advanced Search * Journals * Magazines * Proceedings * Books * SIGs * Conferences * People * * More * Search ACM Digital Library[ ] SearchSearch Advanced Search 10.1145/3652588.3663324acmconferencesArticle/Chapter ViewAbstract Publication PagespldiConference Proceedingsconference-collections pldi * Conference * Proceedings * Upcoming Events * Authors * Affiliations * Award Winners * More * Home * Conferences * PLDI * Proceedings * SOAP 2024 * Misconceptions about Loops in C research-article Open access [icon-small] Share on * * * * * * Misconceptions about Loops in C Authors: Martin Brain and Mahdi MalkawiAuthors Info & Claims SOAP 2024: Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis June 2024 Pages 60 - 66 https://doi.org/10.1145/3652588.3663324 Published: 20 June 2024 Publication History Related Artifact: [artifact] Misconceptions About Loops in C June 2024 data https://doi.org/10.5281/zenodo.11113582 * 0citation * 11 * Downloads Metrics Total Citations0 Total Downloads11 Last 12 Months11 Last 6 weeks11 Get Citation Alerts New Citation Alert added! This alert has been successfully added and will be sent to: You will be notified whenever a record that you have chosen has been cited. To manage your alert preferences, click on the button below. Manage my Alerts New Citation Alert! Please log in to your account PDFeReader * Contents SOAP 2024: Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis Misconceptions about Loops in C Pages 60 - 66 PREVIOUS ARTICLE Static Analysis for Transitioning to CHERI C/C++ Previous + Abstract + References ACM Digital Library * + Information & Contributors + Bibliometrics & Citations + View Options + References + Media + Tables + Share Abstract Loop analysis is a key component of static analysis tools. Unfortunately, there are several rare edge cases. As a tool moves from academic prototype to production-ready, obscure cases can and do occur. This results in loop analysis being a key source of late-discovered but significant algorithmic bugs. To avoid these, this paper presents a collection of examples and "folklore" challenges in loop analysis. References [1] 2023. Competition on Software Verification (SV-COMP). https:// sv-comp.sosy-lab.org/ Google Scholar [2] Alfred Vaino Aho, Monica Sin-Ling Lam, Ravi Sethi, and Jeffrey David Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley. Google Scholar [3] Frances Elizabeth Allen. 1970. Control Flow Analysis. 5, 7 (1970), issn:0362-1340 https://doi.org/10.1145/390013.808479 Digital Library Google Scholar [4] Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety Verification and Refutation by k-Invariants and k-Induction. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 145-161. isbn:978-3-662-48288-9 Google Scholar [5] Martin Brain and Mahdi Malkawi. 2024. [artifact] Misconceptions About Loops in C. https://doi.org/10.5281/zenodo.11113582 Digital Library Google Scholar [6] Larry Carter, Jeanne Ferrante, and Clark Thomborson. 2003. Folklore Confirmed: Reducible Flow Graphs Are Exponentially Larger. SIGPLAN Not., 38, 1 (2003), jan, 106-114. issn:0362-1340 https://doi.org/ 10.1145/640128.604141 Digital Library Google Scholar [7] Byron Cook, Bjorn Dobel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, and Pawel Wieczorkiewicz. 2020. Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. IEEE, 185-193. https://doi.org/10.34727/2020/ isbn.978-3-85448-042-6_26 Crossref Google Scholar [8] Tom Duff. 1988. Re: Explanation, please!. Usenet. http:// doc.cat-v.org/bell_labs/duffs_device Google Scholar [9] Paul Havlak. 1997. Nesting of Reducible and Irreducible Loops. ACM Trans. Program. Lang. Syst., 19, 4 (1997), jul, 557-567. issn:0164-0925 https://doi.org/10.1145/262004.262005 Digital Library Google Scholar [10] Matthew Sterling Hecht and Jeffrey David Ullman. 1974. Characterizations of Reducible Flow Graphs. J. ACM, 21, 3 (1974), jul, 367-375. issn:0004-5411 https://doi.org/10.1145/321832.321835 Digital Library Google Scholar [11] Brian Wilson Kernighan and Dennis MacAlistair Ritchie. 1978. The C Programming Language. Bell Telephone Laboratories Incorporated. Google Scholar [12] Sambasiva Rao Kosaraju. 1974. Analysis of structured programs. J. Comput. System Sci., 9, 3 (1974), 232-255. issn:0022-0000 https:// doi.org/10.1016/S0022-0000(74)80043-7 Digital Library Google Scholar [13] Chloe Lourseyre. 2021. Duff's device in 2021. https://belaycpp.com/ 2021/11/18/duffs-device-in-2021/ Google Scholar [14] Daniel Neville, Andrew Malton, Martin Brain, and Daniel Kroening. 2016. Towards automated bounded model checking of API implementations. CEUR Workshop Proceedings, 1639, 31-42. Google Scholar [15] Carl D. Offner. 2013. Notes on graph algorithms used in optimizing compilers. University of Massachusetts Boston. https://www.cs.umb.edu /~offner/files/flow_graph.pdf Google Scholar [16] Florian Schanda and Martin Brain. 2012. Using Answer Set Programming in the Development of Verified Software. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12), Agostino Dovier and Vitor Santos Costa (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 17). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 72-85. isbn:978-3-939897-43-9 issn:1868-8969 https://doi.org/10.4230/ LIPIcs.ICLP.2012.72 Crossref Google Scholar [17] Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmuller. 2015. Successful Use of Incremental BMC in the Automotive Industry. In Formal Methods for Industrial Critical Systems, Manuel Nunez and Matthias Gudemann (Eds.). Springer International Publishing, Cham. 62-77. isbn:978-3-319-19458-5 Google Scholar [18] Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmuller. 2017. Incremental Bounded Model Checking for Embedded Software. Form. Asp. Comput., 29, 5 (2017), sep, 911-931. issn:0934-5043 https://doi.org/10.1007/s00165-017-0419-1 Digital Library Google Scholar [19] Kaitlyn Siu and Marcelo Badari. 2022. What's A Loop : A Tree House Adventure. Wayland. isbn:978-1526315717 Google Scholar [20] James Stanier and Des Watson. 2012. A Study of Irreducibility in C Programs. Softw. Pract. Exper., 42, 1 (2012), jan, 117-130. issn:0038-0644 https://doi.org/10.1002/spe.1059 Digital Library Google Scholar [21] Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzman Jimenez, Simon Daniel, Chris Bryan, and Ian Broster. 2017. Functional Requirements-Based Automated Testing for Avionics. In 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS). 170-173. https://doi.org/10.1109/ICECCS.2017.18 Crossref Google Scholar [22] Simon Tatham. 2000. Coroutines in C. https:// www.chiark.greenend.org.uk/~sgtatham/coroutines.html Google Scholar [23] Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, and Yoshiumi Kawamura. 2019. Application of Abstract Interpretation to the Automotive Electronic Control System. In Verification, Model Checking, and Abstract Interpretation, Constantin Enea and Ruzica Piskac (Eds.). Springer International Publishing, Cham. 425-445. isbn:978-3-030-11245-5 Google Scholar Index Terms 1. Misconceptions about Loops in C 1. Software and its engineering 1. Software organization and properties 1. Software functional properties 1. Formal methods 1. Automated static analysis 2. Software verification Recommendations * CLAPP: characterizing loops in Android applications (invited talk) DeMobile 2015: Proceedings of the 3rd International Workshop on Software Development Lifecycle for Mobile When performing program analysis, loops are one of the most important aspects that needs to be taken into account. In the past, many approaches have been proposed to analyze loops to perform different tasks, ranging from compiler optimizations to Worst-... Read More * CLAPP: characterizing loops in Android applications ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering When performing program analysis, loops are one of the most important aspects that needs to be taken into account. In the past, many approaches have been proposed to analyze loops to perform different tasks, ranging from compiler optimizations to Worst-... Read More * Program analysis too loopy? Set the loops aside Among the many obstacles to efficient and sound program analysis, loops may be the most prevalent. In program analyses that traverse paths, loops introduce a variable, possibly infinite and number of paths. This study assesses the potential of a program ... Read More Comments Please enable JavaScript to view thecomments powered by Disqus. Information & Contributors Information Published In cover image ACM Conferences SOAP 2024: Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis June 2024 66 pages ISBN:9798400706219 DOI:10.1145/3652588 * General Chairs: * Raphael Monat Inria, France / University of Lille, France , * Cindy Rubio-Gonzalez University of California at Davis, USA Copyright (c) 2024 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License. Sponsors * SIGPLAN: ACM Special Interest Group on Programming Languages Publisher Association for Computing Machinery New York, NY, United States Publication History Published: 20 June 2024 Permissions Request permissions for this article. Request Permissions Check for updates Badges * [icon-large]Artifacts Available / v1.1 Author Tags 1. Loop Analysis 2. Software Verification 3. Static Analysis Qualifiers * Research-article Conference SOAP '24 Sponsor: * SIGPLAN SOAP '24: 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis June 25, 2024 Copenhagen, Denmark Acceptance Rates Overall Acceptance Rate 11 of 11 submissions, 100% Contributors [loader-7e6] Other Metrics View Article Metrics Bibliometrics & Citations Bibliometrics Article Metrics * 0 Total Citations * 11 Total Downloads * Downloads (Last 12 months)11 * Downloads (Last 6 weeks)11 Other Metrics View Author Metrics Citations View Options View options PDF View or Download as a PDF file. PDF eReader View online with eReader. eReader Get Access Login options Check if you have access through your login credentials or your institution to get full access on this article. Sign in Full Access Get this Publication Media Figures Other Tables Share Share Share this Publication link Copy Link Copied! Copying failed. Share on social media XLinkedinRedditFacebookemail Affiliations Martin Brain City, University of London, London, United Kingdom https://orcid.org/0000-0003-4216-7151 Search about this author Mahdi Malkawi City, University of London, London, United Kingdom https://orcid.org/0009-0005-3045-1472 Search about this author Download PDF Go to Go to Show all references Request permissionsExpand All Collapse Expand Table Authors Info & Affiliations View Table of Contents Export Citations Select Citation format[BibTeX ] * Please download or close your previous search result export first before starting a new bulk export. Preview is not available. By clicking download,a status dialog will open to start the export process. The process may takea few minutes but once it finishes a file will be downloadable from your browser. You may continue to browse the DL while the export process is in progress. Download + Download citation + Copy citation Footer Categories * Journals * Magazines * Books * Proceedings * SIGs * Conferences * Collections * People About * About ACM Digital Library * ACM Digital Library Board * Subscription Information * Author Guidelines * Using ACM Digital Library * All Holdings within the ACM Digital Library * ACM Computing Classification System * Accessibility Statement Join * Join ACM * Join SIGs * Subscribe to Publications * Institutions and Libraries Connect * Contact us via email * ACM on Facebook * ACM DL on X * ACM on Linkedin * Send Feedback * Submit a Bug Report The ACM Digital Library is published by the Association for Computing Machinery. Copyright (c) 2024 ACM, Inc. * Terms of Usage * Privacy Policy * Code of Ethics ACM Digital Library home ACM Association for Computing Machinery corporate logo Your Search Results Download Request We are preparing your search results for download ... We will inform you here when the file is ready. Download now! Your Search Results Download Request Your file of search results citations is now ready. Download now! Your Search Results Download Request Your search export query has expired. Please try again.