Applied Implicit Computational Complexity

APPLIED IMPLICIT COMPUTATIONAL COMPLEXITY Neea Rusch Submitted to the Faculty of The Graduate School of Augusta University in partial fulfillment of the Requirements of the Degree of Doctor of Philosophy September 2025 Dissertation defended on Friday, 15 August 2025, in Augusta, Georgia before the dissertation committee composed of: Dr. Clément Aubert, major advisor . . . . . . . . . . Augusta University, United States Dr. Martin Avanzini . . . . . . . . . . . . Centre Inria d’Université Côte d’Azur, France Dr. Yuyan Bao . . . . . . . . . . . . . . . . . . . . . . . . . . . . Augusta University, United States Dr. Bogdan Chlebus . . . . . . . . . . . . . . . . . . . . . . . Augusta University, United States Dr. Harley Eades III . . . . . . . . . . . . . . . . . . . . . . . Augusta University, United States © 2025 by Neea Rusch CC Attribution 4.0 International Acknowledgements Multiple individuals deserve repeated recognitions for their impact in my doctoral journey. However, in interest of brevity, I have adopted a principle from linear types: mentioning each name exactly once.1Let that principle not diminish the significance of anyone’s role. R Family. Kiitos, Eila ja Lefa. Oli kiva nähdä ja toivottavasti tavataan taas. I am thankful to my children, Ileana and Tommy. They both influenced my doctoral studies in their own ways. I am incredibly proud of both of you. Tank, my fondest companion and best buddy, was with me every year I spent at Augusta University, 2011–2025. Academic thanks. My history at Augusta University is extensive. It involves three institutional names,2various roles, learning moments, and interactions with many exceptional individuals. My current achievements are thanks to the last one. In these acknowledgements, I aim to capture everyone who contributed overall positively to this outcome.3 From my undergraduate years, 2011–2014, I appreciate every professor who was teaching computer science at the time: Joanne Sexton, Mike Dowell, Onyeka Ezenwoye, and Paul York. From them, I learned the foundations of my discipline. My undergraduate experience was encouraging, nurturing, and provided the skills that helped me succeed later, at Georgia Institute of Technology and various companies. I am thankful to Joseph Hauger, 1Except Clément, because his actions and influence require multiple mentions. 2Augusta State University, Georgia Regents University, and Augusta University. 3Though, I suspect I still end with a sound under-approximation. Tom Colbert, and Sam Robinson (Professor Emeritus), from the College of Science and Mathematics, for supporting me financially during those years through the Savannah River Scholar’s Program. I am also thankful for the instruction of Predrag Punoševac as I understood the value of his teachings only years later. Finally, I appreciate Jurgen Brauer (Professor Emeritus) and Walter Evans (Professor Emeritus), for creating me opportunities to develop my software engineering skills before I even graduated. After an enriching hiatus, I returned to Augusta University in 2019. First as an instructor and soon as a doctoral student.4This return was prompted in response to the many invitations and encouragement I received (again) from my undergraduate professors. I recognize and thank Steve Weldon for his role in supporting this re-entry. I appreciate my fellow pioneering students, James O’Meara and William Cocke, who were present with me in those early days of the computer science doctoral program, in the spring of 2021. The years of my doctoral study were made pleasant and memorable thanks to the many friends and colleagues I met at the Palazzo5in Summerville. I thank Peter Hanukaev for his friendship, and leadership of ΔΛΔ, and organizing with me the programming languages reading group. I thank Deivid Vale, Gabriele Cecilia, Jason Weeks, Mahady Hassan, Mark Holcomb, and Vignesh Sivakumar for the shared experiences of the reading group and many social events. A special recognition to my fellow Palazzo ladies and friends. Zain Halloush, I will always remember the “escape mission” before the movie Millennium Actress. Nour Alhussien, my special friend, thank you for everything – including the many delicious Arabic foods I got to sample. I am thankful for the many magical moments we all shared as students. I am excited for all our futures and learning what happens in the next chapters. Being in the first cohort in a doctoral program was minimally a character-building experience. It required much resilience and tenacity, since various policies were not in place, or 4In 2020 or 2021, depending on where we set the official start. 5The name was inspired by Konstantin Britikov and Rodrigo Otoni; and validated by Simone Gazza. were not yet fitted for computer science. I accumulated many “firsts” and uncovered several edge cases in the program logistics, which I hope will be resolved over time. I appreciate Gagan Agrawal, for his commitment to student success in the early days of the program, and his direct support to me at various stages of my doctoral study. As a testament to Gagan’s momentous influence—although he left Augusta University two years ago, just two years after the launch of the program—he had a direct impact on the successes of three students that were first to defend their dissertations. During these turbulent times, I also greatly appreciate the stability, peace, and support I found at The Graduate School (TGS). I particularly recognize the strong leadership, commitment, and consistency in action of the TGS Dean, Jennifer Sullivan. I appreciate Patricia Cameron, for her responsiveness and support, especially during the Three Minute Thesis competition. Finally, I want to thank Emily Crider, for the many prompt responses and overall support of the graduate students. Also thanks to The Graduate School for hosting the many wonderful events that fueled and nourished the students of the Palazzo. Across other departments, I am thankful for the supportive and positive staff at the Center of Writing Excellence, where I worked with Brilynn Janckila, Candis Bond, Hannah Soblo, Makayla Mathews, and Romana Hinton. I also appreciate the staff at the Reese Library, which is my special retreat in Summerville. I am thankful for all the times I had the privilege of attending lectures of John Hayes of Pamplin College of Arts. Finally, I greatly appreciated the numerous performance I experienced at the Maxwell Performing Arts Theatre, especially the many organized by Matthew Buzzell. But, beyond friends and events, doctoral study is foremost a phase of individual growth. Easily the most influential person in my journey was my advisor and scientific mentor, Clément Aubert. I started my doctoral study without research experience, but through his guidance developed an appreciation for the elegance and beauty of theoretical computer science. Through years of mentoring and countless conversations, he helped me grow and instilled the research skills that will carry me in the future. It saddens me greatly that our interactions are inevitably ending, and that I am completely incapable of adequately expressing my gratitude for the past. The Augusta University community is infinitely enriched by your presence and mentorship. I hope many more students get to experience it. In research, I am thankful for my collaborators, Thomas Rubiano and Thomas Seiller, for the many projects we completed together. In my mind, our projects represent the ideal model of scientific collaboration, and I am happy to have experienced that model early. I am also thankful to the members of my doctoral committee. Bogdan Chlebus, for his impact in those early days of the doctoral program, and for the guidance that led me to finding the best advisor. Harley Eades III, for instituting programming languages research in Augusta and for introducing me to functional reactive programming. Martin Avanzini, for graciously hosting me in Sofia Antipolis, and for the many fascinating conversations about the flow calculus. Yuyan Bao, for the many thoughtful conversations, reading group experiences, and our many shared experiences. I am also immensely thankful to Neil Jones and Lars Kristiansen, for creating the flow calculus of mwp-bounds. The calculus has been a source of much inspiration and wonder throughout my doctoral study, and expectedly will be also in the future. Outside Augusta, my doctoral journey was greatly elevated by the many fascinating people I met on my travels. Besides the names already mentioned, I appreciate the following individuals – for the conversations, guidance, inspiration, memories, shared adventures, and friendship – that shaped my doctoral experience. Ahmed K. Zaher, Alaia Solko-Breslin, Alan Jeffrey, Alfons Laarman, Amirali Ebrahimzadeh, Anssi Yli-Jyrä (for the reissumies), Arjun Ramesh, Ármin Zavada, Arthur Correnson, Brigitte Pientka, Bryan Richlinski, Caleb Stanford, Chengsong Tan, Chris Brzuska, Christine Rizkallah, Delphine Demange, Dhanushka Jayasuriya, Dionysios Spiliopoulos, Elliot Bobrow, Eric Cornelissen, Ewen Denney, Fabian Muehlboeck (for the dissertation format choice), Haoyi Zeng, Ignacio Ballesteros, Jared Pincus (for Computer Junkyard), Jonathan Aldrich, João C. Pereira, Judith Perera, Julian Loss, Jérémy Thibault, Krystal Maughan, Laura Kovacs, Leona Odole, Linard Arquint, Lisa Oakley, Long Pham, Luca Maio, Mandana Farhang Ghahfarokhi, Marsha Chechik, Mihai Nicola, Mishel Carelli, Mohammed Foughali, Natarajan Shankar, Norine Coenen, Onur Şahin, Pamela Zave, Paul Patault, Rémi Desmartin, Romain Péchoux, Ross Horne, Rustan Leino, Santiago Bautista, Shengyu Huang, Shriram Krishnamurthi, Sumit Gulwani, Thomas Lamiaux, Tim Nelson, Tobias Nießen, Tomáš Dacík, Wilf Offord, Yannick Forster, and Zahra Moezkarimi. I hope we meet again, sometime, somewhere! Recognitions of support in creation of this dissertation. This dissertation benefits from many open source software projects, developed benevolently by contributors around the world. I thank the development teams of the many excellent scientific programming tools— like the Rocq Prover, Dafny, and Python—that I regularly use in my research. I thank Clément Aubert for the initiative and action of preparing the general L A T EX template for doctoral dissertations, and making it open source. Now it benefits all students of The Graduate School at Augusta University. Several aspects and styling of this dissertation were inspired by other researchers, through their work. I appreciate Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti, for their artistry in styling code blocks in (Giallorenzo, Montesi, & Peressotti, 2024), and for sharing those sources on arXiv. The same style is used throughout this dissertation. I was greatly impressed by the work of Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton in (Dash, Kaddar, Paquet, & Staton, 2023); and its companion artifact, the Haskell library LazyPPL (Dash, Kaddar, Paquet, & Staton, 2024). The presentation influenced the preparation of the pymwp tool user guide that appears in §2.1.7. Finally, I am thankful to Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg for their work in “Linearly qualified types,” (Spiwack, Kiss, Bernardy, Wu, & Eisenberg, 2022). From the manuscript, I learned many neat techniques for formatting type systems and working with unicode. Viimeisenä ISO kiitos Tonille ja Sipelle musiikista joka säesti monia väitöskirjan kirjoitushetkiä. Nyt ei pitäisi olla puutteita koodissa! Acknowledgements of financial research support. The primary funding agency behind this work is me. During the doctoral study, my scientific development was also greatly enhanced by numerous research visits and professional events. Participating in these events was made possible thanks to the financial support I received from many generous agencies (in alphabetic order). The list includes all agencies that impacted or supported the dissertation research in any meaningful way, and is complete up to the date of writing these acknowledgements. The ACM Special Interest Group on Programming Languages (SIGPLAN), AFCEA Educational Foundation, Association Internationale pour les Technologies Objets (AITO) e.V., Booz Allen Hamilton, Computing with Infinite Data (CID) programme of the European Commission, Department of Informatics at the Technische Universität München, ETAPS e.V., Graduate Student Government Association (GSGA) at Augusta University, Institute of Electrical and Electronics Engineers (IEEE), NATO Science for Peace and Security Program, National Science Foundation (NSF), Office of the Provost at Augusta University, the Programming Methodology Group at ETH Zürich, SRI International, The Graduate School (TGS) at Augusta University, Udo Keller Stiftung, fortiss GmbH, organizers and sponsors of the mentoring workshop at the International Conference on Computer Aided Verification (CAV) 2023, organizers and sponsors of the European Conference on Object-Oriented Programming (ECOOP) 2025, organizers and sponsors of the European joint conferences on Theory and Practice of Software (ETAPS) 2024, organizers and sponsors of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2022, organizers and sponsors of the International Programming Language Implementation Summer School (PLISS) 2025, the Japan Society for the Promotion of Science (JSPS) Coreto-Core Program, the Transatlantic Research Partnership, and the Translational Research Program of the Department of Medicine at the Medical College of Georgia. Abstract NEEA RUSCH Applied Implicit Computational Complexity (Under the direction of DR. CLÉMENT AUBERT) Implicit computational complexity (ICC) complements classic complexity theory by developing machine-independent characterizations of complexity classes. The idea is to introduce a restriction, at the level of a programming language, that guarantees every program satisfying the restriction belongs to a particular complexity class. There are several strong motivations for this approach, including that ICC systems drive better understanding of complexity classes, yield natural definitions and proofs, and produce techniques for automatable program analysis for free. However, despite the numerous advantages, ICC remains largely a theoretical novelty. This means the practical power, limitations, and advantages of ICCbased program analyses are not well-understood. The dissertation research “puts ICC theories to test” by investigating their capabilities outside the theoretical domain. A guiding intuition is that, if applied, implicit computational complexity could provide us new techniques for program analysis and verification. Over a series of projects, the dissertation work yields three main findings. The first shows that ICC offers complementary techniques for analyzing resource usage. In other words, it allows to produce quantitative reports about programs execution behaviors in cases that are overlooked by other techniques. Second, it is possible to adjust the analyses to track other program properties. This suggests that unrealized potential is available in ICC systems, and we should learn to leverage it. The third finding is reflective and visionary. An essential 30 Published and archived artifacts . . . . . . . . . . . . . . . . . . . . . . . 386 List of Figures 1 Dissertation manuscripts and their associations . . . . . . . . . . . . . . . 9 2 Implicit complexity in a nutshell . . . . . . . . . . . . . . . . . . . . . . . 23 3 Program analysis as an approximation . . . . . . . . . . . . . . . . . . . . 31 4 Sound and incomplete bug detector vs. verifier . . . . . . . . . . . . . . . 32 5 The pymwp static analyzer workflow . . . . . . . . . . . . . . . . . . . . . 49 6 Variable labels of an mwp-matrix . . . . . . . . . . . . . . . . . . . . . . . 53 7 The inference rules of the original mwp-calculus . . . . . . . . . . . . . . 55 8 Visualizing loop transformations . . . . . . . . . . . . . . . . . . . . . . . 75 9 The fork-join programming model . . . . . . . . . . . . . . . . . . . . . . 83 10 Parallel worksharing in loop executions . . . . . . . . . . . . . . . . . . . 86 11 Loop fission transformation . . . . . . . . . . . . . . . . . . . . . . . . . . 91 12 Document classification scheme . . . . . . . . . . . . . . . . . . . . . . . 94 13 Grammar of the non-interference security type system . . . . . . . . . . . . 105 14 Non-interference security type system . . . . . . . . . . . . . . . . . . . . 105 15 Formal verification approaches . . . . . . . . . . . . . . . . . . . . . . . . 118 16 Development view of the simple Rocq proof . . . . . . . . . . . . . . . . . 123 17 Overview of Dafny implementation and verification workflow . . . . . . . 126 18 Automation degree chart . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 19 Dafny running in Visual Studio Code . . . . . . . . . . . . . . . . . . . . . 128 20 Simple imperative while language . . . . . . . . . . . . . . . . . . . . . . 184 21 Statement examples, sets, and representations of their dependencies . . . . 187 22 Data-Flow Graph of composition . . . . . . . . . . . . . . . . . . . . . . . 188 23 Distributing a more complex while loop . . . . . . . . . . . . . . . . . . . 192 24 Code transformation example . . . . . . . . . . . . . . . . . . . . . . . . . 196 25 Speedup of selected benchmarks . . . . . . . . . . . . . . . . . . . . . . . 198 26 Simple imperative programs and their corresponding data flow graphs . . . 213 27 The mwp-analysis workflow . . . . . . . . . . . . . . . . . . . . . . . . . 216 28 A selection of flow calculus rules for assigning vectors to expressions. . . . 218 29 A data-flow graph of LucidLoop . . . . . . . . . . . . . . . . . . . . . . . 222 30 Flow calculus inference rules for while and loop ..............229 31 A demonstration of improved derivation failure handling . . . . . . . . . . 231 32 Loop cases for analyzer comparison . . . . . . . . . . . . . . . . . . . . . 241 33 Postcondition analysis scopes . . . . . . . . . . . . . . . . . . . . . . . . . 254 34 A simple imperative while language.....................265 35 Security-Flow Matrix of compositions . . . . . . . . . . . . . . . . . . . . 270 36 Primary research findings . . . . . . . . . . . . . . . . . . . . . . . . . . . 321 37 Original non-deterministic flow analysis rules . . . . . . . . . . . . . . . . 366 38 Deterministic improved flow analysis rules . . . . . . . . . . . . . . . . . . 368 List of Listings 1 Equivalentprograms ............................. 3 2 Acostequationsystem ............................ 35 3 Derivableprogram .............................. 58 4 Loop that always fails the derivation . . . . . . . . . . . . . . . . . . . . . 59 5 Loop that fails for some derivation paths . . . . . . . . . . . . . . . . . . . 59 6 Program with a single assignment . . . . . . . . . . . . . . . . . . . . . . 60 7 Program with exponential variable value growth . . . . . . . . . . . . . . . 61 8 Program with a while loop.......................... 63 9 “Infinite”program............................... 65 10 Challenge program whose derivability is unknown . . . . . . . . . . . . . . 66 11 Program with control flow . . . . . . . . . . . . . . . . . . . . . . . . . . 68 12 Transformed program with arithmetic . . . . . . . . . . . . . . . . . . . . 69 13 Loopofinsertionsort............................. 71 14 Canonicalloopform ............................. 72 15 Loop fusion transformation . . . . . . . . . . . . . . . . . . . . . . . . . . 74 16 Loop fission transformation . . . . . . . . . . . . . . . . . . . . . . . . . . 74 17 Loop splitting transformation . . . . . . . . . . . . . . . . . . . . . . . . . 75 18 Loop tiling transformation . . . . . . . . . . . . . . . . . . . . . . . . . . 75 19 Loop peeling transformation . . . . . . . . . . . . . . . . . . . . . . . . . 75 20 Loop unrolling transformation . . . . . . . . . . . . . . . . . . . . . . . . 75 21 Beforeinterchange .............................. 75 22 Afterinterchange ............................... 75 23 Truedependence ............................... 77 24 Antidependence................................ 77 25 Outputdependence .............................. 78 26 Controldependence.............................. 78 27 Loop-carried dependence . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 28 The OpenMP parallel construct...................... 85 29 Serialexecution................................ 86 30 Parallelexecution............................... 86 31 Parallelworksharing ............................. 86 32 Sequentialversion............................... 88 33 Parallelversion ................................ 88 34 Applyingfullunroll.............................. 89 35 Fully transformed loop . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 36 Applying partial unroll . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 37 Partially transformed loop . . . . . . . . . . . . . . . . . . . . . . . . . . 90 38 Secure and insecure Boolean operations . . . . . . . . . . . . . . . . . . . 97 39 Implicit information flow leak in an array . . . . . . . . . . . . . . . . . . 97 40 High conditional incremental leak . . . . . . . . . . . . . . . . . . . . . . 97 41 Uncovering loop invariants . . . . . . . . . . . . . . . . . . . . . . . . . . 116 42 AsimpleproofinRocq............................122 43 A Rocq proof of program equivalence . . . . . . . . . . . . . . . . . . . . 130 44 Proof of program equivalence in Dafny . . . . . . . . . . . . . . . . . . . . 132 45 Leftpadinaction ...............................133 46 LeftpadinRocq(1)..............................135 47 LeftpadinRocq(2)..............................136 48 Leftpad in SSReflect proof language . . . . . . . . . . . . . . . . . . . . . 137 49 Formally verified Leftpad in Dafny . . . . . . . . . . . . . . . . . . . . . . 138 50 Moscow messaging functions . . . . . . . . . . . . . . . . . . . . . . . . . 142 51 Receiver knows sender . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 52 Person A cannot recover the allocation . . . . . . . . . . . . . . . . . . . . 143 53 Running a certified message exchange . . . . . . . . . . . . . . . . . . . . 144 54 An imperative program that manipulates variables . . . . . . . . . . . . . . 165 55 Program assign_expression . . . . . . . . . . . . . . . . . . . . . . . . . . 169 56 Programexponent_2 .............................171 57 Programnotinfinite_3.............................172 58 Programinfinite_3 ..............................174 59 Challenge program dense_loop . . . . . . . . . . . . . . . . . . . . . . . . 175 60 Precisecontext ................................208 61 Imprecisecontext...............................208 62 Benchmark: LucidLoop . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241 63 Benchmark: Function condition . . . . . . . . . . . . . . . . . . . . . . . 241 64 Benchmark: Finite iteration . . . . . . . . . . . . . . . . . . . . . . . . . . 241 65 LucidLoop verified in Dafny . . . . . . . . . . . . . . . . . . . . . . . . . 249 66 Running pymwp in loop analysis mode . . . . . . . . . . . . . . . . . . . . 250 67 Program analysis with Duet . . . . . . . . . . . . . . . . . . . . . . . . . . 251 68 Creating a trace with Daikon . . . . . . . . . . . . . . . . . . . . . . . . . 252 69 Infer invariants using Daikon . . . . . . . . . . . . . . . . . . . . . . . . . 252 70 Displaying invariants inferred by Daikon . . . . . . . . . . . . . . . . . . . 252 71 Benchmark: mwp/example 3.4 . . . . . . . . . . . . . . . . . . . . . . . . 253 72 Benchmark: mwp/not infinite #4.......................253 73 Benchmark: Linear #02............................253 74 Expositoryprogram..............................263 75 AssignmentCase ...............................290 76 LoopCase...................................290 77 BranchingCase................................290 List of Algorithms 1 Program analysis with flow calculus of mwp-bounds . . . . . . . . . . . . . 57 2 Command analysis with flow calculus of mwp-bounds . . . . . . . . . . . . 57 3 A loop fission algorithm for parallelizing loops . . . . . . . . . . . . . . . 191 4 mwp-matrix evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 1 Introduction 1 1.1 Problem Statement and Specific Aims A programmable computer is a gadget without precedent that can be appreciated from many perspectives. For example, it can be viewed as an engineering marvel of ever-increasing capacity, as a medium for new flashy applications, or as the machine-independent scientific discipline that forms its foundations (Dijkstra, 1979a; Hoare, 2006). This dissertation focuses on the intellectual challenge of programming these gadgets. This challenge seems unique in the combination of the possibility for unmastered complexity – programs are among the most complex things ever conceived – and the ultimate, but misleading, simplicity of a world of zeros and ones alone (Dijkstra, 1979a). Programming languages provide us a convenient interface for crafting programs. A programming language is an abstraction layer, because it relieves us from working with 0s and 1s directly. We can write programs in a human-intelligence form, and then “translate” (compile) it to 0s and 1s for processing by computers. However, the abstraction provided by programming languages does nothing to reduce the intellectual challenge involved in programming (Dijkstra, 1979b). If we write a syntactically legal but faulty program, we are at the mercy of our faulty creation when the program executes. Equivalence. A fascinating feature about programs is that we can write multiple distinct programs that compute the same result for the same input. Two programs J𝑝1Kand J𝑝2Kare functionally equivalent, i.e., J𝑝1K≡J𝑝2K, iff for every possible input 𝑖,J𝑝1K(𝑖)=J𝑝2K(𝑖). In other words, the criteria is to maintain the input/output behavior, but we are allowed to change how the result is computed. A scientifically inclined reader will recognize functional equivalence as multiple algorithms computing the same function. A software engineer will recognize it as the art of refactoring. 2 Concept Prior foundational work Dissertation work ∗Preprint Implicit Computational Complexity “A Flow Calculus of mwp-Bounds for Complexity Analysis” Jones & Kristiansen (2009) “Loop Quasi-Invariant Chunk Detection” Moyen, Rubiano & Seiller (2017) “mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity” Aubert, Rubiano, Rusch & Seiller (2022) CODE “Distributing and Parallelizing Non-canonical Loops” Aubert, Rubiano, Rusch & Seiller (2023) Wave-Square “pymwp: A Static Analyzer Determining Polynomial Growth Bounds” Aubert, Rubiano, Rusch & Seiller (2023) CODE “A Logic for Anytime Non-Interference∗” Aubert & Rusch SHIELD-ALT “Polynomial Postconditions via mwp-Bounds∗” Rusch Check “Certifying Complexity Analysis∗” Aubert, Rubiano, Rusch & Seiller (2023) Rusch (2023 – ?) Check Related Topics CODEStatic Program Analysis Wave-SquareProgram Optimization CheckFormal Methods SHIELD-ALTSecurity Figure 1: Dissertation manuscripts and their dependency associations. 9 1.1.4.1 Automatic Resource Analysis In the first direction, we focus on the flow calculus of mwp-bounds, introduced by Jones and Kristiansen (2009). It is a canonical example of an ICC system for analyzing variable value growth (data size) in imperative programs. The flow calculus is introduced in detail in §1.2.3. Building on the flow calculus, we define three research questions. RQ1 Can we develop an automatic program analysis based on the flow calculus? RQ2 Given its paper proofs, is the theory correct? I.e., can we prove formally the soundness of the flow calculus? RQ3 Assuming the theory can be automated, what are its use cases? The manuscripts building on the flow calculus demonstrate its uses in static program analysis and in formal verification for specification inference. The manuscripts support all dissertation goals. The manuscripts concerned with the implementation of the flow calculus (RQ1) support Goals 1–3. A formally verified soundness proof (RQ2), and an application to formal verification (RQ3) support Goal 4. One manuscript, “mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity” is in the Appendix (§7) due to an Augusta University policy. The placement should not distract from the significance of the work, as several other manuscripts follow from it. The results of the research questions are discussed in §4.1.1. 10 1.1.4.2 Analyzing Extended Non-Functional Properties The second direction starts with complexity-theoretic techniques but repurposes them toward analysis of other non-functional properties. The technical foundation is inspired by “Loop Quasi-Invariant Chunk Detection” by Moyen, Rubiano, and Seiller (2017a). In the original formulation, the idea is to identify fragments of loops (called “blocks”), whose variables become invariant after a finite number of iterations. Such loop quasi-invariant code blocks can then be lifted from the loop. The program transformation improves the loop’s complexity profile if the lifted block is a nested loop. For convenience, we refer to this technique as the QI framework, after quasi-invariants. This original QI framework is not presented in this dissertation. This is because each refinement changes the behavior of the system and requires fully redefining the system each time. The manuscripts in §2.2 and §3.2 thus provide the technical details. We define two research questions relating to the QI framework. RQ4 How to develop a program transformation to increase parallelization potential? RQ5 How to use it to analyze security properties, specifically non-interference? The research questions thus change the motivation from complexity theory to other application domains. Critically, the original complexity result may be lost, but some other guarantee is gained. On the surface, the research questions appear to be about properties, but more deeply they are about understanding better the underlying theory and its flexibility. Both goals are practically motivated. The expected deliverables support Goals 1 and 2. Moreover, they are strongly aligned to support Goal 4. The results of the research questions are discussed in §4.1.2. 11 1.1.5 Manuscript Overview The dissertation manuscripts connect implicit computational complexity with related research topics. Each manuscript is decorated with an icon that denotes the secondary topic. The topics include: static program analysis IJ, security ȷ, program optimization Д, and formal methods n. Author contributions. The authors are always listed in alphabetical order. The manuscripts in Chapters §2–§3 are “first author” works. The manuscripts in Chapter §7 are “non-first author” works. The co-authors contributions are detailed in Chapter §9. Peer review. The entire Chapters §2, §3, §5, and §7 have been peer reviewed. In other words, the only new content is Chapters §1 and §4, i.e., Introduction and Discussion. • The published works in Chapters §2 and §7, were inspected by 7–10 reviewers before acceptance. • The unpublished works, in Chapter §3, have been reviewed by at least 4 reviewers thus far. Preliminary versions have been accepted and presented at respectable workshops. Be advised that the unpublished works must be viewed with caution, as they are works in progress. All works have some limitations that prevent their inclusion among the published manuscripts. • Chapter §5 is an extended abstract. It describes about the full-length dissertation in a standalone manner. It has been peer-reviewed and presented at the Doctoral Symposium of the European Conference on Object-Oriented Programming 2025. 12 1.1.6 Important Tips to the Reader This dissertation contains three varying-length versions of its content. This allows accessing the presentation at different levels of detail, by need. Content organization. 1. The abstract contains the highlights only. 2. Chapters §1–§4 and §7 form the full-length presentation. 3. Chapter §5 is a standalone extended summary of the full presentation. 1.1.6.1 Software Artifacts and Data Availability All software developed as part of this dissertation is publicly available. Each published manuscript in the dissertation has an associated software artifact. The artifacts are archived, according to the policies of the Association for Computing Machinery (ACM, 2020), for long-term retention. The artifacts are archived even if the publication venue did not provide an official artifact evaluation round. Therefore, each manuscript consists of more than just the text pages of the dissertation. How to locate the artifacts is explained in Chapter §8. Dissertation source code. The source code of the dissertation (Rusch, 2025d) is publicly available at the following repository. https://github.com/nkrusch/dissertation www 13 Dissertation artifact. The dissertation has a companion artifact. The artifact is preloaded with all required software and enables reproducing all executable examples that appear in the dissertation. For example, §2.1.7 can be followed interactively with the artifact. The URL of the artifact is: https://doi.org/10.5281/zenodo.17148077 www 1.1.6.2 Notational Conventions Programming languages, syntax, and code blocks. Syntactic constructs (variables, expressions, commands, etc.) that are embedded in text are typeset in teletype. Larger or more significant code blocks are displayed as dedicated code listings. The listings will display, in the bottom right corner, the associated programming language or context, according to Table 1. In the table, version is the language release version assumed in the listings, when applicable (pseudo-languages do not have a version). Plain text listings, that describe command outputs, are labelled “output.” Internet addresses are marked by “www.” The Rocq Prover is undergoing a name change from its former name Coq. We will use the new name whenever possible. Line numbers. References to a line of source code (or an algorithm) begin with an L, for line. The L is followed by a number (or a numeric range) that specifies the row(s) of interest. For example, L3 means line number 3, and L10–12 means lines 10 to 12. Distinguishing variable states. We will often want to refer to the same variable in different states of computation. In the style of Z specification language (Spivey & Abrial, 1992), we use notation that identifies the new (post) states. A plain variable refers to a state where 14 Language Description Version C the C programming language C99 C* imperative C-like pseudo-language – CES cost equation system – cmd executable shell/terminal command – Dafny the Dafny programming language 4.10.0 Imp imperative language of mwp-calculus – Java the Java programming language SE 24 OMP C code that includes OpenMP directives 6.0 Rocq the Rocq interactive theorem prover 8.20.1 SSReflect the SSReflect proof language 2.4.0 While simple imperative while language – Table 1: The programming languages used in code listings. the variable holds its initial value. A variable with a postfix decoration 'refers to a state where the variable holds its final value. For example, Xrefers to the initial value and X' refers to the final value. 1.1.6.3 Lookup Indices The dissertation includes three indices for terms, acronyms, and symbols. The Term Index (§12) lists technical terms and their uses. Acronyms are generally defined at first use and the Index of Acronyms (§10) lists the long form. The Symbol Index (§11) lists definitions of symbolic notations. 15 1.1.6.4 Dynamic Bibliographic Entries Some bibliography entries refer to dynamic resources like software, web pages, or lecture notes (without DOIs). References to such documents may become unreliable over time. To improve the long-term availability and recoverability, they are pre-emptively preserved in suitable online archives, on Software Heritage and the Internet Archive. Software repositories. Version-controlled third-party software repositories are archived at Software Heritage. For a repository hosted at <URL>, the recovery address pattern is: https://archive.softwareheritage.org/browse/origin/directory/ ?origin_url=<URL> www Example 1 (Recovering a software repository).The dissertation source code archival recovery address is: https://archive.softwareheritage.org/browse/origin/directory/?origin_u rl=https://github.com/nkrusch/dissertation www □ Written documents. Web pages and PDF files are archived in the Wayback Machine of the Internet Archive. Use the following pattern to recover a document from the Internet Archive – substitute <URL> by the document’s URL: https://web.archive.org/web/<URL> www 16 A few cited documents could not be archived by the Internet Archive; for example because the hosting server was blocking automatic clients. These documents are denoted in the bibliography with the symbol †. Example 2 (Recovering archived documents).The following URL is fragile and it may disappear in the future. https://types22.inria.fr/files/2022/06/TYPES_2022_paper_14.pdf www As a backup, the following Internet Archive address produces the same document. https://web.archive.org/web/https: //types22.inria.fr/files/2022/06/TYPES_2022_paper_14.pdf www □ 17 1.2 Literature Review For research papers, it is often optimal to arrive to new findings as soon as possible. This need is motivated by a page limit, but also the need to keep readers interested. Thus, it is natural to make certain assumptions about the readers’ prior knowledge and sacrifice extensive explanations of the basics. This description also applies to the manuscripts bundled in this dissertation. However, the dissertation does not have the same constraints as a research paper. There is neither a page limit nor a compelling reason to omit technical foundations. Since it took several years to internalize and complete the work presented in this dissertation, it seems unlikely every reader is familiar with the same foundations. Therefore, this section presents the technical background needed to enjoy to full extent the manuscripts that will follow. Manuscript Title Section Background mwp-Analysis Improvement and Implementation… 7.1 1.2.1, 1.2.2, 1.2.3 pymwp: A Static Analyzer Determining Polynomial… 2.1 1.2.1, 1.2.2, 1.2.3 Distributing and Parallelizing Non-canonical Loops 2.2 1.2.4 Polynomial Postconditions via mwp-Bounds 3.1 1.2.3, 1.2.6 A Logic for Anytime Non-Interference 3.2 1.2.5 Certifying Complexity Analysis 3.3 1.2.3, 1.2.6 Table 2: Manuscript background dependency associations. The background is organized thematically. The subsections are (mostly) self-contained introductions to the specified topic. It is advisable to read first §1.2.1, but the other sections can follow in any order. It is also possible to initially skip the background and return to this section when a manuscript creates a need to understand its foundations. Refer to Table 2 for guidance on how to connect the dissertation manuscripts with the background topics. 18 𝑦as 𝑓( 𝑥; 𝑦), where the semicolon separates the normal from the safe. This way, the usual scheme of primitive recursion can be restricted as follows: 𝑓(0, 𝑥; 𝑦)=ℎ( 𝑥; 𝑦); 𝑓(𝑛+1, 𝑥; 𝑦)=𝑔(𝑛, 𝑥; 𝑦,𝑓(𝑛, 𝑥; 𝑦)). The way we define 𝑓from 𝑔and ℎis morphologically identical to what happens in the usual primitive recursive scheme. That it is a restriction is a consequence of the distinction between normal and safe arguments: the recursive call 𝑓(𝑛, 𝑥; 𝑦)is required to be forwarded to one of g’s safe argument, while the first parameter of 𝑓must be normal. This makes exp not expressible anymore, giving rise to new function algebra called safe recursion, discovered by Bellantoni and Cook (Bellantoni & Cook, 1992a) (BC in the following). Theorem 1. The class BC equals the class FP of polynomial time computable functions. □ The Bellantoni and Cook result extends an earlier result by Cobham (Cobham, 1965). The Cobham-Edmonds Thesis asserts that being feasible is the same as being computable in polynomial time (Cobham, 1965; Edmonds, 1965). Although the Cobham characterization is independent of any particular execution model, it is not fully syntactic. The limitations are that a size bound has to be proved on the semantics of recursion, and the proof uses a particular model of Turing Machine. This prevents constructing an automatic procedure to check whether a program satisfies Cobham’s criteria (Heraud & Nowak, 2011). In contrast, the Bellantoni and Cook characterization is a fully syntactic and membership in BC can be checked automatically. Note that Safe recursion aims to guarantee that there exists a polynomial bounding the execution time; however, it does not provide the actual value of the polynomial (i.e., the complexity bound are implicit) Heraud and Nowak (2011). The 25 Bellantoni and Cook result was proved formally (Heraud & Nowak, 2018) by Heraud and Nowak (2011). 1.2.1.4 A Snapshot of Theoretical Results The breakthrough result of safe recursion is regarded as the first implicit characterization of a complexity class (Dal Lago, 2011; Kristiansen, 2017; Rubiano, 2017). However, the same result was independently discovered by Leivant (1993) in a slightly different setting of stratified recurrence (Dal Lago, 2022, p. 762). Table 3 shows a very small collection of additional impactful theoretical results. The inclusion criteria is varied and based on representing the rich variety of underlying techniques or complexity classes; or for presenting foundational techniques that have been extended later; or for reflecting shifts in theoretical developments and interests over time. The table also marks with hyperlinks works that are discussed elsewhere in this dissertation. These theoretical results provide a conceptual “toolbox” of techniques that form the foundation for the rest of this dissertation. Symbols. Ʌlogics Ǧtype system ƒdata flow syntactic Ļalgebras ȕrecursion Year Venue Description Classes 1992∗Comput safe recursion – §1.2.1.3 P Complex. Bellantoni and Cook (1992a) 1993∗ȕPOPL stratified recurrence P Leivant (1993) 1995 ĻCSL tiering a.k.a. ramification PSPACE Leivant and Marion (1995) Table 3: (Cont.) 26 Symbols. Ʌlogics Ǧtype system ƒdata flow syntactic Ļalgebras ȕrecursion Year Venue Description Classes 1999 ǦLICS non-size-increasing program P Hofmann (1999) 2000 ȕLPAR quasi-interpretations P Marion and Moyen (2000) 2001 J. Funct. CONS-free programs P, EXP Program. Jones (2001) 2001 ƒPOPL size-change termination principle – §1.2.2.3 PSPACE Lee, Jones, and Ben-Amram (2001) 2005 ĻComput. LOOP−and CLIP programs L, LINSPACE Complex. Kristiansen (2005) 2009 ɅTOCL flow calculus of mwp-bounds – §1.2.3 P Jones and Kristiansen (2009) 2010 ɅTheor. quantum implicit computational complexity EQP, BQP, ZQP Comput. Sci. Dal Lago, Masini, and Zorzi (2010) 2011 ǦLICS SAFE programs – §1.2.5.6 P Marion (2011) 2013 ǦICALP ramified programs – §1.2.5.6 P, L Leivant and Marion (2013) 2013 ǦFoSSaCS SAFE processes – §1.2.5.6 P Hainry, Marion, and Péchoux (2013) Table 3: (Cont.) 27 Symbols. Ʌlogics Ǧtype system ƒdata flow syntactic Ļalgebras ȕrecursion Year Venue Description Classes 2015 ǦLPAR dℓT programs𝑎– §1.2.5.6 P Baillot, Barthe, and Dal Lago (2015) 2016 ɅInf. Comput. Complexity with pointer machines L Aubert and Seiller (2016) 2016 ȕInf. Comput. Complexity of uniform Boolean circuits NC Bonfante, Kahle, Marion, and Oitavem (2016) 2018 ǦInf. Comput. object oriented SAFE programs – §1.2.5.6 P Hainry and Péchoux (2018) 2021 ĻMFCS Probabilistic characterization STPP PP Dal Lago, Kahle, and Oitavem (2021) 2023 ǦPOPL stratified programs (STR) – §1.2.5.6 P Hainry and Péchoux (2023) 2024 ǦPOPL quantitative type theory with dependent types P, NP, BPP Atkey (2024) 2024 ǦLICS aperiodic programs – §1.2.5.6 P Hainry, Kapron, Marion, and Péchoux (2024) 𝑎The system can handle sub-computations not in P. Table 3: A list of theoretical implicit computational complexity systems and results. The historically first publications are marked with the symbol ∗. The graphical icons describe the primary restriction technique used to enforce complexity bounds. 28 1.2.2 Static Resource Analysis Asymptotic analysis, that classifies programs based on resource requirements, is the natural dual to the study of complexity classes. Since implicit computational complexity focuses on language-based characterizations, it produces analysis techniques for free. It is a foundational hypothesis of this dissertation that theoretical ICC systems—with sufficient expressive power and an efficient evaluation strategy—enable concrete program analysis. An analysis that evaluates a program’s resource usage is called resource analysis. Resource analysis is a subfield of static program analysis. 1.2.2.1 Foundations of Static Program Analysis Static program analysis aims to answer questions about the runtime behaviors of programs. The term static means the analysis is conducted at compile-time on the program syntax and without execution. The main motivations is to improve the performance characteristics of the generated executable (Kennedy & Allen, 2001; Nielson, Nielson, & Hankin, 2010). Such improvements include detecting logical issues in the specification of the input program. Foundational techniques include, e.g., type and effect systems; control and data flow analysis; abstract interpretation (AI) (Cousot, 2021); constraint-based, pointer, and inter-procedural analysis; and fixed point algorithms (Møller & Schwartzbach, 2024; Nielson, Nielson, & Hankin, 2010). Static program analysis is strongly practice-oriented and frequently materialized in automatic analyzers. Real-world software development tools— like compilers, interactive development environments, and verifiers—rely on static analyses (Livshits et al., 2015). A central challenges of static analysis concerns the precision and scalability of the techniques. These topics are actively explored in research (Arzt et al., 2014; Dudina & Stark, 2025; Schiebel, Sattler, Schubert, Apel, & Bodden, 2024). 29 As a consequence of Rice’s Theorem (Rice, 1953),10 it is impossible to construct a perfect program analyzer for a Turing-complete language. All approaches must sacrifice something among soundness, completeness and termination (Møller, 2024). Although seemingly discouraging, Rice’s Theorem should be viewed with optimism. Since static program analysis is inherently undecidable, there is infinite opportunity in building increasingly precise approximations.11 The challenge is then to design analysis techniques that produce useful answers efficiently and often enough. This challenge is colloquially called the “full employment theorem for static program analysis designers” (Møller & Schwartzbach, 2024, p. 4). Static analyzers are designed to evaluate programs against semantic properties.12 More specifically, the focus is on safety properties (Møller & Schwartzbach, 2024, p. 6), which assert that something bad will not happen (Lamport, 1977). Examples of safety properties are memory safety, absence of overflows, termination, and secure information flow (cf. §1.2.5.2). Safety properties have many applications, for example, in bug finding (Popeea & Chin, 2010), program optimization (Rinard & Diniz, 1996), and verification (Falcone, Fernandez, & Mounier, 2009). 1.2.2.2 The Challenge of Approximation There are two broad categories of static analyzers (Jourdan, Laporte, Blazy, Leroy, & Pichardie, 2015). • A bug finder must discover potential errors that are hard to find by testing. The analysis must be precise because excessive false alarms make the tool unusable. The 10Informally, Rice’s Theorem asserts that all interesting questions about the input/output behavior of programs written in a Turing-complete language are undecidable. 11For inspiration see, e.g., Ding and Zhang (2023). 12Properties are discussed in §1.2.6.1, but previewed here briefly. 30 precision of an analysis is the degree to which it avoids erroneous results (Livshits et al., 2015). However, a bug finder offers no guarantee that all bugs will be found. • A program verifier must establish that a given safety property holds with high confidence. Critically, the analyzer must account for all execution paths. If the analyzer reports no alarms, then it must be the case that the program is free of the errors tracked by the analyzer. Obtaining the intended behavior depends on design choices, particularly on how the analysis approaches soundness and completeness. a b Universe of programs Safe over-approximation Exact Unsafe Safe under-approximation Figure 3: Program analysis as an approximation – an illustration inspired by Steffen (2020). The EXACT class of programs satisfying the analyzed property 𝜙is undecidable. The program 𝑎satisfies 𝜙, but the program 𝑏does not. For an analyzer making a SAFE UNDER-APPROXIMATION, every accepted program truly satisfies 𝜙, but would give an erroneous result on 𝑎. An analyzer making a SAFE OVER-APPROXIMATION would accept 𝑎and 𝑏, even though 𝑏does not satisfy 𝜙. However, an over-approximating analyzer never misses programs that satisfy 𝜙. Although an UNSAFE analysis can be justifiable in some cases, interpreting its results is problematic because errors are not conservative. Soundness and completeness. A terminating static analyzer can either be sound or complete, but not both. Soundness and completeness are terms from logic and not exclusive to static program analysis. In logic, they carry the following meaning. 31 “there is definitely an error in the program” Bug Finder “there may be errors in the program” Verifier “there are definitely no errors in the program” Figure 4: Behavior of sound and incomplete static analyzers: bug detector vs. verifier (Møller, 2024). An “error” is some property tracked by the analyzer. • A sound system guarantees that everything that is provable is true. • A complete system guarantees that everything that is true has a proof. In the context of program analysis, if a provably sound system reports that some property holds, then it must be true for the analyzed program. A sound analyzer never misses a violation—i.e., when a property does not hold—but it may report an erroneous result for a satisfactory program (Torlak, 2015). A complete analyzer detects all satisfactory programs, but also accepts cases where the tracked property does not truly hold. The analysis approximation should be conservative whereby all errors occur on the “safe side” of the application domain (Møller & Schwartzbach, 2024, p. 5). Refer to Figures 3 and 4 for examples. To offer guarantees, a sound analyzer must overestimate the program behaviors. It models all execution paths, including those that do not occur in any execution, like all branches of a conditional statement. Soundness is challenging because it can render the analysis unscalable or imprecise to the point of being useless. To maintain semantics, an optimizing analysis typically requires soundness (Møller & Schwartzbach, 2024, p. 5). A complete analyzer underestimates the program behaviors and thus errs on the other side. Soundiness. While academic literature widely emphasizes sound analyses, according to Livshits et al. (2015), strict soundness is a myth among realistic whole-program analyzers. Practically-orientated static analyzers typically insist on Turing-completeness 32 and termination, but trade between soundness and completeness (Møller & Schwartzbach, 2024; Steffen, 2020). As an compromise, modern analyzers for real programming languages are often soundy. A soundy analysis is as sound as possible, without excessively compromising precision or scalability (Livshits et al., 2015). 1.2.2.3 Techniques of Resource Analysis Resource analysis13—or (static/automatic) complexity analysis (Leivant & Marion, 2013; Rosendahl, 1989)—aims to obtain static information about the runtime execution cost of an analyzed program. Such analysis naturally decomposes into two parts: one concerning the program’s execution time and termination; and the other change in the program’s data size (Jones & Kristiansen, 2009). Numerous techniques can be used to reason about such properties. • Termination analyses tend to focus on values that are copied or decreased. Establishing termination is a critical aspect of correctness of recursive calls and commands. Termination analyses aim to discover conditions—like difference constraints (Sinn, Zuleger, & Veith, 2017), program-dependent well-founded orders on loops (Lee, Jones, & Ben-Amram, 2001), or establishing that recursive reduction sequence are finite14— that guarantee termination. A specific technique for termination analysis, that originates from implicit computational complexity, is the size-change termination principle of Lee, Jones, and Ben-Amram (2001). • Data-size analyses focus on memory consumption, estimating how large various variable values may become (Lommen & Giesl, 2023). Determining data-size bounds requires studying patterns of data-size changes during computation. In imperative 13Also called cost analysis when using an explicit cost measure (Albert, Arenas, Genaim, & Puebla, 2008). 14Showing that every reduction sequence is finite is called the strong normalization property (Bertot & Castéran, 2004, p. 36) 33 programs, interesting data-size behaviors arise from counter increments and resets, particularly in loops (Ben-Amram & Hamilton, 2020; Sinn, Zuleger, & Veith, 2017). This dissertation is mainly concerned with techniques of data-size analysis. Among the well-established techniques are automatic amortized resource analysis (AARA) and cost equation systems (CES). These techniques are briefly introduced next. Automatic amortized resource analysis. Amortized analysis averages the time required to perform a sequence of operations over all the operations performed (Cormen, Leiserson, Rivest, & Stein, 2009, p. 451). Amortization enables to show that the average cost of an operation is small, even if a single operation might be expensive. Automatic amortized resource analysis (AARA) (Hoffmann & Jost, 2022) builds on the same idea: bounding programs by amortization. In AARA, the analysis can account for amortization effects across sequences of operations. Internally, the analysis relies on inference rules and derivation trees provide proofs of the resource bounds. Thus, AARA provides an automatic static technique for deriving arithmetic resource bounds. AARA originated from works in implicit computation complexity, and in particular from the contributions of Martin Hofmann (Hoffmann & Jost, 2022). The initial design was for tracking resource bounds in functional programs (Hoffmann, Aehlig, & Hofmann, 2012). In later works, techniques based on or influenced by AARA have been extended to imperative (Carbonneaux, Hoffmann, Reps, & Shao, 2017; Carbonneaux, Hoffmann, & Shao, 2015), parallel (Hoffmann & Shao, 2015), probabilistic (Avanzini, Moser, & Schaper, 2020; Ngo, Carbonneaux, & Hoffmann, 2018; Wang, Kahn, & Hoffmann, 2020), and concurrent session-typed programs (Das, Balzer, Hoffmann, Pfenning, & Santurkar, 2021; Das, Hoffmann, & Pfenning, 2018). 34 1.2.2.6 Prospects of ICC-Based Program Analysis There are two general strategies for implementing static analyses based on implicit computational complexity. The first involves restricting the program syntax to guarantee all valid programs satisfy a desired property. This is challenging for a software engineer since it may require writing programs in an unnatural way (though not all programs are written by humans). However, if the program can be expressed in the given syntax, then the desired property is obtained for free. The second strategy allows a software engineer to write any program and performs program analysis aposteriori. Instead of requiring every program to be written using the restriction ℛ, we would test the adhesion of the program to the restriction ℛ. While this is more preferable for the program creator, such analysis is necessarily incomplete. Some programs will be decided incorrectly and must be refactored to be acceptable to an analyzer. Nonetheless, this strategy already has produced applications in Moyen and Rubiano (2016) and Moyen, Rubiano, and Seiller (2017a). Those research lines illustrates a shift from the design of ICC programming languages – from pre-bounding all programs – to the design of criteria that may or may not be met by programs written in a Turing-complete programming language. The first observation is crucial, considering that software engineers in general focus on much more tangible functional properties, than complexity classes. The second observation sends a mixed signal. It seems that ICC will lose the originality of its approach by accepting to act as a post-filter on Turing-complete programming languages. Let us not forget that by restricting the programming language itself, ICC offers the possibility of never having to run any analysis. Compelling related examples of systems that provide properties by construction already exist. The safe subset of the programming language Rust guarantees e.g., memory safety and deadlock freedom by design. Strongly normalizing interactive theorem provers require 41 structural fixed point termination (Bertot & Castéran, 2004). In return, every valid programs is known to terminate. Although a software engineer cannot write every program, if they accept the restriction, they receive the termination guarantee for free. Conceivably, implicit computational complexity techniques can provide similar X-by-Construction (ter Beek, Cleophas, Schaefer, & Watson, 2018) guarantees. 1.2.3 The Flow Calculus of mwp-Bounds The flow calculus of mwp-bounds, introduced by Jones and Kristiansen (2009), is a sound and compositional complexity analysis technique for reasoning about variable value growth in imperative programs. It tracks data-size growth in variables between commands. The information about variable value growth is captured and expressed as mwp-bounds. More precisely, for program Cthe analysis aims to discover polynomially bounded data flow relations, between the initial values 𝑥1,…,𝑥𝑛of natural-number variables X1,…,X𝑛 and the final values 𝑥′𝑖of X𝑖(for 𝑖 = 1,…,𝑛), that hold whenever JCK(𝑥𝑖⇝ 𝑥′𝑖). If it is possible to determine that all variable values grow at most polynomially in inputs, the analysis assigns to program Cabound, i.e., a conjunction of mwp-bounds; that characterizes the value growth of all its variables. The conclusion is derived statically and syntactically by applying inference rules to the commands of the program. As a motivating preview, Examples 3 and 4 demonstrate the semantic property the analysis detects. Example 3 (Polynomially bounded program).The variable values of the program X1=X2+X3; X1=X1+X1 42 are bounded by 𝑥′1≤ 2𝑥2+2𝑥3and 𝑥′2≤ 𝑥2and 𝑥′3≤ 𝑥3. Each variable can be bounded by at most a polynomial and the flow calculus accepts the program. The polynomially bounded data flow relation JCK(𝑥1,𝑥2,𝑥3⇝𝑥′1,𝑥′2,𝑥′3)holds for all variables in all program states. □ Example 4 (An always failing program).Consider a program that repeats, for X2times, an arithmetic operation on the variable X1. X1=1; loop X2{X1=X1+X1} The value of X2never changes from its initial value; therefore, the final value of X2is trivially bounded by a polynomial 𝑥′2≤𝑥2. However, variable X1grows at an exponential rate, with final value bounded by 𝑥′1≤2𝑥2. Since variable X1cannot be bounded by a polynomial, the program is rejected by the flow calculus of mwp-bounds. □ 1.2.3.1 Tracking Value Growth With Coefficients As a bookkeeping procedure, the flow calculus of mwp-bounds tracks coefficients (or “flows”) representing how data flows in variables between commands. The name of the calculus comes from these coefficients. In the mwp-calculus, harmless data flows are acceptable. However, computations that are harmful lead to values not bounded by a polynomial in the inputs and the coefficients capture these data flow facts. The coefficients are, in order of lowest to the highest degree of dependency: 0indicating no dependency, 𝑚for maximal of linear, 𝑤for weak polynomial, 𝑝for polynomial, and ∞for failure, when no value growth bound can be established. The 𝑚-flow is harmless. The 𝑤and 𝑝-flows are sometimes harmful and have restrictions on their use. The distinction between 𝑤and 𝑝is that 𝑤is iteration-independent and 𝑝is iteration-dependent (more 43 harmful). The ∞-flow is always harmful. For example, if an exponential dependency exists between two variables, the analysis assigns an ∞-coefficient to the target variable of the data flow. Internally, the coefficients are collected and tracked in mwp-matrices. The mwp-matrices are assigned to program commands by the inference rules of the mwp-calculus. This dissertation will revisit the topic of mwp-matrices several times, presenting them at different levels of detail. For this introduction, it suffices to consider an mwp-matrix as an array of coefficients for simplicity. A sound calculus of value growth. The analysis result is binary and indicates whether all final values can be bounded by polynomials in inputs. When affirmative, we call the analyzed program derivable. For a program Cand an mwp-matrix 𝑀, the syntactic relation ⊢C∶ 𝑀 holds if a program is derivable. In other words, a derivable program can be assigned an mwp-matrix of at most 𝑝-coefficients at each variable. If a command Ccomputes a function growing exponentially, the statement C∶ 𝑀 will be false for all matrices 𝑀. The flow calculus result is sound but incomplete. If a derivable program terminates, the soundness theorem (Jones & Kristiansen, 2009, p. 12) guarantees that the variable value growth is polynomially bounded. Theorem 2 (Soundness of mwp-calculus).⊢C∶𝑀implies ⊨C∶𝑀.□ The soundness theorem connects the syntactic data flow relation to the semantic property ⊨C∶ 𝑀. Informally, derivability guarantees that the variable values of program Cwill grow at most polynomially at runtime. This in turn ensures program Cruns in polynomial time (Kristiansen, 2017). The main result of the work introducing the flow calculus (Jones & Kristiansen, 2009) is precisely a proof of the soundness theorem. Since the analysis omits termination, the flow analysis provides a partial correctness guarantee. 44 The flow calculus offers no guarantee to programs that are not derivable. Then, variable value growth is interpreted as unknown. A program always fails if a variable value grows “too fast”, for example exponentially. A single variable can be the source of whole-program derivation failure. Alternatively, failure may occur from inability to express satisfiable behavior. The latter is a built-in limitation of the flow calculus. To increase expressiveness and capture a larger class of derivable programs, the mwp-calculus includes nondeterminism in its inference rules. Consequently, a single program may admit multiple derivations with distinct matrices, which in turn complicates determining the result of the analysis. However, a program is derivable if there exists a derivation without an ∞-coefficient. The mwp-bounds characterize value growth. The column vectors of an mwp-matrix encode variable value growth bounds. An mwp-bound (denoted 𝑊,𝑉,𝑈,…) characterizes the value growth of a single variable w.r.t. program inputs. An mwp-bound is an expression of form max( 𝑥,poly1( 𝑦))+poly2( 𝑧). Variables characterized by 𝑚-flow are listed in 𝑥; 𝑤-flows in 𝑦, and 𝑝-flows in 𝑧. The notation 𝑊( 𝑥; 𝑦; 𝑧)displays all the variables in an mwpbound 𝑊where 𝑥,𝑦and 𝑧are respectively the 𝑚-, 𝑤and 𝑝-variables of 𝑊. Variables characterized by 0-flow do not occur in the expression and no bound exists if some variable is characterized by ∞. The poly1and poly2are honest polynomials, build up from constants and variables by applying +and ×. Any of the three variable lists might be empty, and poly1and poly2may not be present. When characterizing value growth, an mwp-bound is approximative; it excludes precise constants and degrees of polynomials. We write an mwpbound of variable Xas 𝑥′≤𝑊where 𝑥′is the final value of Xand 𝑊is an mwp-bound. A program bound is a conjunction (∧) of its variables’ mwp-bounds. Example 5 (Interpreting mwp-bounds).For an arbitrary variable, the mwp-bound indicates the final value of the variable is bounded by… 45 0…a constant. X…the initial value of variable X. max(X,Y)…the initial values of Xor Y, the greatest of the two. max(X,0)+Y…the initial values of Xand Y. max(X0,X1+X2)+X3×X4…the maximum of X0or X1+X2, and X3×X4. □ Multiple mwp-bounds of different form can evaluate to the same numerical value. For example, the mwp-bounds 𝑊 ≡ max(0,X1+X2)+0and 𝑉 ≡ max(X1,0)+X2and 𝑈≡max(X2,0)+X1are all numerically equal to X1+X2. As each variable in the mwpbound omits constants. Thus, an mwp-bound is best suited for recognizing the shape of the value growth rather than its explicit numerical value. Furthermore, mwp-bounds can be incomparable. For example, between 𝑊 ≡max(X1,X2)+X3and 𝑉 ≡X1+X2×X4, it is impossible to determine which mwp-bound evaluates to a lower value numerically. This means mwp-bounds cannot be totally ordered. 1.2.3.2 Advancements of the Flow Calculus, Chronologically The incremental technical advancement of the flow calculus of mwp-bounds is an important theme of this dissertation. The developments are a necessary prerequisite for enabling different applications of the flow calculus. It may be challenging to extract the “big picture of developments” by reading the manuscripts alone. Therefore, this section aims discuss the topic in an accessible manner, with a summary in Table 4). The table corresponds to the following four publications. 46 The original flow calculus. The flow calculus of mwp-bounds (Jones & Kristiansen, 2009) was designed to characterize sequential imperative polytime programs, with an underlying ambition to study the boundary of decidability (Kristiansen, 2017). The complexitytheoretic result is obtained by bounding the growth of variable values by polynomials in inputs. In effect, the flow calculus provides a computational method ℳfor deciding a runtime property, ℳ∶programs →{yes,no} such that {𝐶𝑖∣ℳ(𝐶𝑖)=yes}⊂{𝐶𝑖∣𝐶𝑖runs in polynomial time }. The formulation naturally provides the theoretical foundations and a concrete technique for program analysis. The analysis is defined over nondeterministic inference rules and coefficients {0, m, w, p} where multiple matrices can be assigned to one program. A single program has 3𝑘derivations where 𝑘is the count of binary arithmetic operations (the binary operations are the sources of nondeterminism). The analysis proceeds in a “single-shot”, exploring one derivation path until the complete program syntax has been successfully analyzed, or the derivation fails. On derivation failure, the analysis restarts to explore a different deprivation path until all paths have been exhausted. Among the advantage of the original flow calculus is that if a derivation succeeds, the mwpbounds are obtained immediately. Although on success the method produces mwp-bounds straightforwardly, it does not support searching for mwp-bounds of specific form. The mathematical framework is sophisticated and recognizes a larger class of programs than earlier similar systems, e.g., (Niggl & Wunderlich, 2006). However, beyond pen and paper examples, the technique is infeasible for practical implementation, due to the exponential blowup and inefficient handling of derivation failure. 47 The enhanced MWP∞-calculus. In an effort to move the flow calculus toward practical static analysis, in (Aubert, Rubiano, Rusch, & Seiller, 2022a) (§7.1) the calculus was refined to resolve its theoretical inefficiencies. There are several well-founded motivations for this goal: a practical analysis permits stress-testing the technique beyond paper examples, exports ideas from implicit complexity to broader communities, and exposes hidden challenges within the analysis technique. Most notably, the enhanced flow calculus “internalizes” the nondeterminism through deterministic inference rules. A key notion is the introduction of the ∞-coefficient that tracks derivation failure. Instead of multiple matrices, every program is assigned exactly one (complex) mwp-matrix. The complex mwp-matrix captures all derivations at once, in a single data structure, resolving much of the combinatorial inefficiency of the original flow calculus. Program analysis now transforms, from performing multiple derivations, to a question of determining if there exists a derivation without an ∞-coefficient. This splits the program analysis procedure into two phases of mwp-matrix construction and mwp-matrix evaluation. As a consequence, the mwp-bounds are no longer immediately obtained from the mwp-matrix. The enhanced flow calculus is practically efficient as demonstrated by the prototype implementation, pymwp.17 The technique permits efficient construction of complex mwpmatrices, but only a brute force approach for mwp-matrix evaluation. At the time, the analyzer could answer a question of whether all variables could be bounded (yes/no). However, in absence of an efficient evaluation strategy, it could not provide concrete bounds (cf. Table 1 in §7.1). The pymwp static analyzer. After continued development, the pymwp static analyzer (Aubert, Rubiano, Rusch, & Seiller, 2025) was enhanced in two ways (Aubert, 17Pronounced “paI em double-you pē.” 48 pymwp static analyzer </> program input [front-end] pycparser [phase-I] inference [phase-II] evaluation {…} analysis result output source code AST syntax check matrix object Figure 5: Workflow of the pymwp static analyzer. pymwp analyzes a C program and produces a result with information about the program’s variable value growth. If the program is derivable, the result contains mwp-bounds for all variables. Otherwise, the result identifies the variables with problematic data flows that cause derivation failure. Rubiano, Rusch, & Seiller, 2023b). The first introduced an efficient mwp-matrix evaluation strategy. It enabled representing all permissible derivations in a compact form and producing an arbitrary instance of a program bound, if at least one bound exists. The second introduced feedback about source of derivation failure. This is possible because the ∞-coefficient marks the locations of failure, yielding a more informative system than the original flow calculus. With these enhancements, the analysis produces results efficiently, while exceeding the informative capabilities of the original flow calculus. The workflow of pywmp is visualized in Fig. 5. Functionally, pymwp is a command-line tool that enables running mwp-analysis through a terminal. The analyzer takes as input a program written in (a subset) of the C programming language. The analyzer front-end is pycparser (Bendersky, 2024). pycparser converts the program source code into an abstract syntax tree (AST). Before the inference, the AST is checked for consistency with the imperative language. In strict mode, if the syntax is not fully expressible, the analysis terminates.18 pymwp then runs the flow calculus of mwp-bounds on the (compatible) AST. By default, the result of the analysis displays at the screen and is saved to a file. Besides the CLI interface, pymwp can be incorporated into larger software development as an imported library. 18Importantly, the strict mode is sound because it only accepts programs that are fully-expressible in the imperative language of the flow calculus. 49 Postconditions via mwp-bounds. The most recent development applies the flow calculus to specification inference, namely postconditions §3.1. This ia new use-case, shifting the focus form static analysis toward formal verification. Technically it introduces three flow calculus enhancements: projecting the mwp analysis on individual variables, improving the derivation failure handling strategy, an evaluation strategy to obtain optimal mwp-bounds through a query procedure. For example, it permits inferring mwp-bounds of some variables in presence of whole-program derivation failure. Due to focus on verifying numerical loops, the programming language is restricted to a language of loops. The language adjustment is now a prerequisite to obtain the technical enhancements. The loop analysis variant is implemented in pymwp as a special mode called mwpℓ. Open problems for future developments. Throughout the technical progression, the class of programs covered by the analysis has remained similar; with small adjustments. The semantic property of interest, variable value growth w.r.t. inputs, is never lost nor altered. Therefore, the flow calculus input/output behavior has remained the same. All notable changes concern the mechanics of the analysis and how to improve the process by which the analysis arrives to its conclusion. In the original mwp-calculus, the problem of determining program derivability is NP-complete. It is unknown if the efficiency has changed following the technical advancements. Among the remaining open problems are: 1. extending the imperative language to cover a larger class of programs, 2. formally verifying the flow calculus for obtain a rigorous soundness guarantee (cf. §3.3), 3. exploring the extended analysis applications, and 4. enhancing the precision of the flow calculus. Matrix construction is currently the most costly analysis phase. It is possible to design data flows that make program analysis inefficient due to the resulting matrix size. More effort is needed to scale the analysis to such inputs. 50 Input: sequence of commands P Output: mwp-matrix 𝑀or failure 1Take the first command C0in P 2Analyze C0by Algorithm 2 to obtain 𝑀 3(Maybe signal failure) 4for Commands 𝑛=1…𝑚do 5Analyze C𝑛by Algorithm 2 6(Maybe signal failure) 7Compose 𝑀=𝑀∘𝑀𝑛by rule C 8return mwp-matrix 𝑀 ▷⊢P∶𝑀 Algorithm 1: Program analysis with flow calculus of mwp-bounds. Input: command C Output: mwp-matrix 𝑀or failure 1Analyze expressions in Cby rules E1-E4 2Analyze Cby rules A-W, possibly recursively 3(Maybe signal failure) 4return 𝑀 ▷⊢C∶𝑀 Algorithm 2: Command analysis with flow calculus of mwp-bounds. 57 1.2.3.4 Derivations I: Range of Analysis Outcomes Example 6 (Polynomially bounded program is derivable).Recall the program from Ex. 3, X1= X2+ X3; X1= X1+ X1Imp Listing 3: A derivable program. The conclusion about derivability can be reached by 32= 9distinct derivations, one of which is shown below. E1 ⊢X2∶(0 𝑚 0)E1 ⊢X3∶(0 0 𝑚)E4 ⊢X2+X3∶(0 𝑚 𝑝)A ⊢X1=X2+X3∶(0 0 0 𝑚𝑚 0 𝑝 0 𝑚) E1 ⊢X1∶(𝑚 0 0)E1 ⊢X1∶(𝑚 0 0)E4 ⊢X1+X1∶(𝑝 0 0)A ⊢X1=X1+X1∶(𝑝 0 0 0𝑚 0 0 0 𝑚)C ⊢X1=X2+X3; X1=X1+X1∶(0 0 0 𝑝𝑚 0 𝑝0𝑚) The mwp-bounds are obtained column-wise from the concluding mwp-matrix, cf. §1.2.3.1. For X1, the vector (0 𝑝 𝑝)corresponds to 𝑥′1≤max(0)+X2×X3and simplifies to 𝑥′1≤X2× X3. The mwp-bound is not as tight as possible (expression X2+X3would be an improvement), but discovering a better one requires exploring the derivation paths exhaustively. Variables X2and X3obtain the same mwp-bounds in every derivation. For X2, the vector (0 𝑚 0)gives an mwp-bound 𝑥′2≤X2, and for X3, the vector (0 0 𝑚)gives 𝑥′3≤X3. The program bound is a conjunction of the variables’ mwp-bounds, i.e., 𝑥′1≤X2×X3∧𝑥′2≤X2∧𝑥′3≤X3. □ Example 7 (Failing program admits no derivation).Consider the program fragment from Ex. 4, loop X2{X1= X1+ X1}Imp 58 Listing 4: A loop that always fails the derivation. The command X1=X1+X1admits three derivations. E1 ⊢X1∶(𝑚 0)E3 ⊢X1+X1∶(𝑝 0)A ⊢X1=X1+X1∶(𝑝 0 0𝑚) E1 ⊢X1∶(𝑚 0)E4 ⊢X1+X1∶(𝑝 0)A ⊢X1=X1+X1∶(𝑝 0 0𝑚) E2 ⊢X1+X1∶(𝑤 0)A ⊢X1=X1+X1∶(𝑤 0 0 𝑚) The next step in the derivation requires accounting for the enclosing loop by applying the rule L. The application involves computing the closure (fixed point) 𝑀∗of the mwp-matrix assigned to the body command X1=X1+X1. In this instance, the fixed point computation does not change the mwp-matrix coefficients. The L side condition is ∀𝑖,𝑀∗ 𝑖𝑖 =𝑚. That is, it requires 𝑚-coefficients on the diagonal of 𝑀∗. None of the derivations satisfy the side condition, therefore the program is not derivable. Although the analysis focused only on a program fragment, the complete program fails because it contains a command that is not derivable. □ Example 8 (Derivability in presence of partial derivation failure).Consider the following program, that is a slightly modified version of Ex. 7, loop X3{X2= X1+ X2}Imp Listing 5: A loop that fails for some derivation paths. The body of the loop command admits three different derivations, obtained by applying the tule A to one of the three derivation of the expression X1+X2, that we name 𝜋0,𝜋1and 𝜋2: E1 ⊢X1∶(𝑚 0 0)E1 ⊢X2∶(0 𝑚 0)E3 ⊢X1+X2∶(𝑝 𝑚 0) E1 ⊢X1∶(𝑚 0 0)E1 ⊢X2∶(0 𝑚 0)E4 ⊢X1+X2∶(𝑚 𝑝 0) E2 ⊢X1+X2∶(𝑤 𝑤 0) From 𝜋0, the derivation of loop X3{X2=X1+X2}can be completed using A and L, but since L requires having only 𝑚coefficients on the diagonal, 𝜋1cannot be used to complete the derivation, because of the 𝑝coefficient in a box below: 59 . . . . .𝜋0 ⊢X1+X2∶(𝑝 𝑚 0)A ⊢X2=X1+X2∶(𝑚 𝑝 0 0𝑚0 0 0 𝑚)L ⊢loop X3{X2=X1+X2}∶(𝑚 𝑝 0 0𝑚0 0 𝑝 𝑚) . . . .𝜋1 ⊢X1+X2∶(𝑚 𝑝 0)A ⊢X2=X1+X2∶(𝑚𝑚 0 0 𝑝 0 0 0 𝑚) Similarly, using A after 𝜋2gives a 𝑤coefficient on the diagonal and makes it impossible to use L, hence only one derivation for this program exists. A single successful derivation is sufficient to make the input program derivable. □ 1.2.3.5 Derivations II: Programs From the Tool User Guide The pymwp tool user guide, in §2.1.7, discusses five cases of program analysis of programs written in C. The tool user guide gives the analyzer input and output and describes the rationale for the obtained result. This section complements the tool user guide by showing the derivations behind those results. To retail fidelity with the C language examples, we show inputs in C, but implicitly convert them to the core imperative language of the flow calculus. The examples omit function declarations since those are irrelevant for the analysis. Example 9 (Binary assignment).The input program in Listing 6 contains a single command. 1int foo(int y1,int y2) { 2y2= y1+ y1; 3}C Listing 6: A program with a single assignment. The program has three derivations and all of them succeed. One derivation instance is shown below. 60 E1 ⊢Y1∶(𝑚 0)E1 ⊢Y1∶(𝑚 0)E3 ⊢Y1+Y1∶(𝑝 0)A ⊢Y2=Y1+Y1∶(0 𝑝 𝑚0) The program bound is a 𝑦′1≤Y1∧𝑦′2≤Y1.□ Example 10 (Exponential Program).The input program is in Listing 7. 1int foo(int base, int exp, int i, int result) { 2while (i < exp) { 3result = result * base; 4i=i+1; 5} 6}C Listing 7: A program with exponential variable value growth. Step 1. Analyze the command result = result * base (simplified to r=r*b in the following). It admits three derivations (𝜋0,𝜋1and 𝜋2). E1 ⊢r∶(0 0 0 𝑚)E1 ⊢b∶(𝑚 0 0 0)E3 ⊢r*b ∶(𝑝 0 0 𝑚)A ⊢r=r*b ∶(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚) E1 ⊢r∶(0 0 0 𝑚)E1 ⊢b∶(𝑚 0 0 0)E4 ⊢r*b ∶(𝑚 0 0 𝑝)A ⊢r=r*b ∶(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑝 ) E2 ⊢r*b ∶(𝑤 0 0 𝑤)A ⊢r=r*b ∶(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑤) Step 2. Analyze command i=i+1. Similarly, it admits three derivations (𝜋3,𝜋4and 𝜋5). E1 ⊢i∶(0 0 𝑚 0)E1 ⊢1∶(0 0 0 0)E3 ⊢i+1∶(0 0 𝑝 0)A ⊢i=i+1∶(𝑚 0 0 0 0 𝑚0 0 0 0 𝑝 0 0 0 0𝑚) E1 ⊢i∶(0 0 𝑚 0)E1 ⊢1∶(0 0 0 0)E4 ⊢i+1∶(0 0 𝑚 0)A ⊢i=i+1∶(𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚) E2 ⊢i+1∶(0 0 𝑤 0)A ⊢i=i+1∶(𝑚 0 0 0 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑚) 61 Step 3. Compose the body commands, r=r*b; i=i+1. There are 9 different combinations, by the derivation choices made in the previous steps. . . . . .𝜋0×𝜋3C ⊢B∶(𝑚 0 0 𝑝 0 𝑚0 0 0 0 𝑝 0 0 0 0𝑚) . . . . .𝜋0×𝜋4C ⊢B∶(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚) . . . . .𝜋0×𝜋5C ⊢B∶(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑚) . . . . .𝜋1×𝜋3C ⊢B∶(𝑚 0 0𝑚 0 𝑚0 0 0 0 𝑝 0 0 0 0 𝑝 ) . . . . .𝜋1×𝜋4C ⊢B∶(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑝 ) . . . . .𝜋1×𝜋5C ⊢B∶(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑝 ) . . . . .𝜋2×𝜋3C ⊢B∶(𝑚 0 0𝑤 0 𝑚0 0 0 0 𝑝 0 0 0 0𝑤) . . . . .𝜋2×𝜋4C ⊢B∶(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑤) . . . . .𝜋2×𝜋5C ⊢B∶(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑤) Step 4. Apply rule W to account for the enclosing while loop. It requires first computing mwp-matrix closure 𝑀∗for the body command. The side conditions is ∀𝑖,𝑀∗ 𝑖𝑖 =𝑚and ∀𝑖,𝑗,𝑀∗ 𝑖𝑗 ≠𝑝. That is, the rule can be applied when only 𝑚-coefficients appear on the diagonal and no 𝑝-coefficients occur anywhere in the mwp-matrix . In every derivation, the mwp-matrix violates the side condition by the boxed coefficients. . . . . .𝜋0×𝜋3 𝑀∗=(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑝 0 0 0 0 𝑚) . . . . .𝜋0×𝜋4 𝑀∗=(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚) . . . . .𝜋0×𝜋5 𝑀∗=(𝑚 0 0 𝑝 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑚) . . . . .𝜋1×𝜋3 𝑀∗=(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑝 0 0 0 0 𝑝 ) . . . . .𝜋1×𝜋4 𝑀∗=(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑝 ) . . . . .𝜋1×𝜋5 𝑀∗=(𝑚 0 0 𝑚 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑝 ) 62 . . . . .𝜋2×𝜋3 𝑀∗=(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑝 0 0 0 0 𝑤 ) . . . . .𝜋2×𝜋4 𝑀∗=(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑚 0 0 0 0 𝑤 ) . . . . .𝜋2×𝜋5 𝑀∗=(𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑤 0 0 0 0 𝑤 ) Step 5. We conclude the input program is not derivable. □ Example 11 (While analysis).The input program, that we will refer to as 𝑃, is 1int foo(int X0,int X1,int X2,int X3) { 2if (X1== 1) { 3X1= X2+ X1; 4X2= X3+ X2; 5} 6while (X0<10) { 7X0= X1+ X2; 8} 9}C Listing 8: A program with a while loop. The tool user guide reveals that the program is derivable. Compared to derivation failure that requires exploring all derivation choices, a derivable program simply requires showing one successful derivation. For presentation reasons, we show the two branches of the derivation tree individually. Step 1. The derivation of the if command (𝜋0) is straightforward. Observe that the control expression of the if statement has no impact on the constructed mwp-matrix. 63 E1 ⊢X1∶(0 𝑚 0 0)E1 ⊢X2∶(0 0 𝑚 0)E4 ⊢X2+X1∶(0 𝑚 𝑝 0)A ⊢X1=X2+X1∶(𝑚 0 0 0 0 𝑚 0 0 0 𝑝 𝑚 0 0 0 0 𝑚) E1 ⊢X3∶(0 0 0 𝑚)E1 ⊢X2∶(0 0 𝑚 0)E4 ⊢X3+X2∶(0 0 𝑚 𝑝)A ⊢X2=X3+X2∶(𝑚 0 0 0 0 𝑚 0 0 0 0 𝑚 0 0 0 𝑝 𝑚)I ⊢if(X1==1) { X1=X2+X1; X2=X3+X2}∶(𝑚 0 0 0 0 𝑚 0 0 0 𝑝 𝑚 0 0 0 𝑝 𝑚) Step 2. The derivation of the while loop (𝜋1) is now permitted, because the rule W side condition is not violated by any coefficient. E1 ⊢X1∶(0 𝑤 0 0)E1 ⊢X2∶(0 0 𝑤 0)E4 ⊢X1+X2∶(0 𝑤 𝑤 0)A ⊢X0=X1+X2∶(0 0 0 0 𝑤𝑚 0 0 𝑤0𝑚0 0 0 0 𝑚)W ⊢while(X0<10) X0=X1+X2∶(𝑚 0 0 0 𝑤 𝑚 0 0 𝑤 0 𝑚 0 0 0 0 𝑚) Step 3. Composing the mwp-matrices of the two commands gives an mwp-matrix for the complete input program 𝑃. We conclude the syntactic data-flow relation ⊢𝑃∶𝑀holds. . . . . .𝜋0×𝜋1C ⊢𝑃∶(𝑚 0 0 0 𝑤 𝑚 0 0 𝑝 𝑝 𝑚 0 𝑝 0 𝑝 𝑚) If the program terminates for the input values of the variables (it does not terminate for all inputs), the variable value growth is polynomially bounded. The mwp-bounds of the variables are 𝑥′0≤max(X0,X1)+X2×X3and 𝑥′1≤max(X1)+X2and 𝑥′2≤max(X2)+X3 and 𝑥′3≤max(X3). This program bound matches the result of the tool user guide. □ 64 Example 12 (Infinite program).The input program is 1int foo(int X1,int X2,int X3) { 2if (X1== 1) { 3X1= X2+ X1; 4X2= X3+ X2; 5} 6while (X1<10) { 7X1= X2+ X1; 8} 9}C Listing 9: An “infinite” program. This program is similar to Ex. 11, with only a small change to the while loop. From the previous example, the if statement is derivable as before by 𝜋0. Letting C2represent the while command, the mwp-matrix closures 𝑀∗of C2are shown below. . . . .E3 𝑀∗=(𝑚 0 0 0 0 𝑝 0 0 0 𝑚𝑚 0 0 0 0 𝑚) . . . .E4 𝑀∗=(𝑚 0 0 0 0 𝑚 0 0 0 𝑝 𝑚 0 0 0 0 𝑚) . . . .E2 𝑀∗=(𝑚 0 0 0 0 𝑤 0 0 0 𝑤 𝑚 0 0 0 0 𝑚) Every 𝑀∗violates the side condition of rule W. The problematic coefficient is boxed for emphasis. The program is not derivable. □ Example 13 (Challenge example).The input program has four top-level commands, identified by the circled annotations. 65 1int foo(int X0,int X1,int X2) { 2if (X0) { 3X2= X0+ X1; 4}else { 5X2= X2+ X1; 6} 7X0= X2+ X1; 8X1= X0+ X2; 9while (X2) { X2= X1+ X0; } 10 }C Listing 10: A challenge program whose derivability is unknown. We will refer to these commands as C0–C3and their derivations as 𝜋0–𝜋3, respectively. The program analysis proceeds in corresponding steps. To ease presentation, we will analyze command composition after each individual command. Step 1. Analyze command C0i.e., the if-else statement. E1 ⊢X0∶(𝑚 0 0)E1 ⊢X1∶(0 𝑚 0)E4 ⊢X0+X1∶(𝑚 𝑝 0)A ⊢X2=X0+X1∶(𝑚0𝑚 0 𝑚 𝑝 0 0 0 ) E1 ⊢X2∶(0 0 𝑚)E1 ⊢X1∶(0 𝑚 0)E4 ⊢X2+X1∶(0 𝑝 𝑚)A ⊢X2=X2+X1∶(𝑚 0 0 0 𝑚 𝑝 0 0 𝑚)I ⊢if(X0) X2=X0+X1; else X2=X2+X1∶(𝑚0𝑚 0 𝑚 𝑝 0 0 𝑚) Steps 2–3. Analyze commands C1and C2, i.e., X0=X2+X1and X1=X0+X2. 66 A note on loop representations. This representation is simplified, at least in two ways, for accessibility. Real compile-time code optimizations are performed on an intermediate representation (IR) of the source program. Intermediate representations, which are compilerspecific, differ from the high-level syntactic view described previously. Further, to facilitate various analyses, it is possible to detach programs from language-based representations altogether, via control-flow (and other) graphs. A control-flow graph (CFG) (Allen, 1970) is a directed graph for representing program’s execution paths. In a CFG, the nodes are basic blocks and the edges are control flow paths. A basic block is a linear sequence of program instructions with one entry and one exit point. Control-flow graphs are a common approach for compile-time program analyses and transformations (Moyen, 2017, p. 48) and are adopted, e.g., in the LLVM compiler (LLVM project contributors, 2025). Although making this note is important, the level of detail is unnecessary for this topic overview. 1.2.4.2 Sequential Loop Transformations Compile-time loop optimization is motivated by the idea that a loop transformation yields— by some quantifiable metric like data access pattern—a more optimal loop form than the original source program (Aho, Lam, Sethi, & Ullman, 2007). A loop transformation replaces the original loop(s) with one or more semantically equivalent generated loops. We consider next a few common loop transformations to demonstrate the idea. Assuming a sequential source program, these transformations are straightforward for a compiler to apply automatically (Bertolacci, Strout, de Supinski, Scogland, Davis, & Olschanowsky, 2018). Distributing and combining loops. Loop fusion, in Listing 15, merges multiple loops by replacing them with a single loop. In each iteration, the generated loop executes an iteration of each original loop. Loop fission, in Listing 16, operates in the reverse direction. It breaks the original loop into multiple loops, with each generated iteration taking only a part of 73 the original loop’s body (Zhao et al., 2018). In both transformations, the loop header and iteration space remain unchanged. 1for(int i=0; i<N; i++) { 2A[i] = B[i]; 3C[i] = rand(); 4}C* Listing 15: Loop fusion. 1for(int i=0; i<N; i++) 2A[i] = B[i]; 3for(int i=0; i<N; i++) 4C[i] = rand(); C* Listing 16: Loop fission. Other loop transformations. Although the main focus of the dissertation work is loop fission (in §2.2), there are several other loop transformations. The transformations are summarized visually in Fig. 8. When considering the overall compilation strategy, the combination of applied transformations is important. Iteration range-based transformations. • The split transformation, in Listing 17, breaks the original loop into multiple generated loops. Each generated loop has the same body as the original, but iterates over a different contiguous subset of the original range. • Loop tiling breaks a loop into contiguous chunks of fixed tile size. In Listing 18, the tile size is 8. Tiling improves cache behavior by reducing data reuse distance (Bertolacci, Strout, de Supinski, Scogland, Davis, & Olschanowsky, 2018). • Loop reversal executes loop iterations in the reverse order. For example, if 0,1,…,𝑛−2,𝑛−1are the logical iteration numbers of a loop, after transformation, the iterations occur in order 𝑛−1,𝑛−2,…,1,0(OpenMP Architecture Review Board, 2024). 74 1for(int i=0; i<N/2; i++) { 2A[i] = B[i]; 3C[i] = rand(); 4} 5for(int i=N/2; i<N; i++) { 6A[i] = B[i]; 7C[i] = rand(); 8}C* Listing 17: Loop splitting. 1for(int j=0; j<N; j+=8) { 2for(int i=j; i<j+8; i++) { 3A[i] = B[i]; 4C[i] = rand(); 5} 6}C* Listing 18: Loop tiling. 1A[0] = B[0]; C[0] = rand(); 2A[1] = B[1]; C[1] = rand(); 3for(int i=2; i<N; i++) { 4A[i] = B[i]; 5C[i] = rand(); 6}C* Listing 19: Loop peeling. 1for(int i=0; i<N; i+=2) { 2A[i] = B[i]; 3C[i] = rand(); 4A[i+1] = B[i+1]; 5C[i+1] = rand(); 6}C* Listing 20: Loop unrolling. 1for(int j=0; j<M; j++) 2for(int i=0; i<N; i++) { 3A[i][j] = B[i][j]; 4C[i][j] = rand(); 5}C* Listing 21: Pre-interchange. 1for(int i=0; i<N; i++) 2for(int j=0; j<M; j++) { 3A[i][j] = B[i][j]; 4C[i][j] = rand(); 5}C* Listing 22: Post-interchange. Figure 8: Visualizing loop transformations. 75 • Finally, loop peeling, in Listing 19, is a special case of loop splitting. It removes the first few or last iterations from the body and performs them outside the loop. The loop iteration space is adjusted accordingly. Modifications of the loop body. Loop unrolling expands and duplicates the body commands into similar independent commands. The update condition is adjusted by an unroll factor. In Listing 20 the loop body is unrolled twice, therefore the unroll factor is 2.25 Unrolling aims to reduce or eliminate evaluations of the loop condition. Transforming nested iterations. Loop interchange is a transformation on a nested loop. It changes the loop nesting order by exchanging two iteration variables referenced by a nested loop, as shown in Listings 21 and 22. 1.2.4.3 Dependence in Transformations A transformation is permissible if the transformation preserves the semantics of the source program. Thus, the application of a transformation depend crucially on the execution relationships between program statements.26 The source program specifies, via a series of statements and an ordering of those statements, a set of execution constraints. However, the constraints may be imprecise since not all constraints are needed to preserve the effect of the computation. For example, in the program fragment X=42; Y=5;it is safe to reorder the two statements. A fundamental challenge in compiler theory concerns determining whether an execution order, that differs from the one specified by the source program, always computes the same result as the source program. Dependence is the primary mechanism for determining if code transformation is safe. 25The simplified example assumes the transformation does not exceed the array bounds. 26Compiler literature refers to statements, rather than commands and expressions. 76 Adependence is a relation on statements that must be preserved by a transformation (Kennedy & Allen, 2001, p. 47). Informally, for any two statements S1and S2, if S1 must be executed before S2then S2depends on S1. Dependence arises primarily from data access patterns – if S2refers to a value computed by S1– and from conditional branching, when the execution of S1decides whether S2will execute. Further, by parametrizing computation over iterations, loops introduce additional special cases of dependence. A reordering transformation is any transformation that changes the code execution order, but does not add or delete statements. By the fundamental theorem of dependence, a reordering transformation that preserves every dependence in a program preserves the meaning of that program (Kennedy & Allen, 2001, p. 66). Data and control dependence. How data is accessed during computations creates dependencies in terms of order of shared memory operations. There is a data dependence from statement S1to S2if and only if both statements access the same memory location, at least one statement writes to the location, and there is a runtime execution path from S1to S2 (Kennedy & Allen, 2001, p. 59–60). Dependence is further complicated by the program’s control flow. Conditional branching creates a control dependence between the control statement and the statements whose execution depends on the control statement (Kennedy & Allen, 2001, p. 374). Four common cases of data and control dependence are demonstrated in Listings 23–26. The interesting variables, that reference a memory location of interest, are emphasized. X=42;S1 Y=X;S2 C* Listing 23: True dependence. Y=X;S1 X=42;S2 C* Listing 24: Antidependence. 77 X=1;S1 X=2;S2 Y=5*X;S3 C* Listing 25: Output dependence. if (Y==1)S1 X=42;S2 C* Listing 26: Control dependence. • A true dependence occurs when a write (S1) executes before a read (S2) at the same memory location (X). True dependence ensures the read observes the value of the write. • An antidependence reverses the order, with a read (S1) executing before a write (S2) at the same memory location (X). • An output dependence requires two writes (S1,S2) to the same memory location (X). It forbids reordering the writes to prevent an interchange that would cause a subsequent read (S3) to observe an incorrect value. • In control dependence, the dependent statement (S2) is conditionally executed, based on evaluation of the control statement (S1). Dependence in loops. Data and control dependence are applicable to loops; however, loops introduce additional dependence. Dependence in loops arises from statements being parameterized by iterations in which they execute. Aloop-carried dependence (Kennedy & Allen, 2001, p. 73), in Listing 27, occurs when a statement uses a value computed in a different iteration. More precisely, a statement S2has a loop-carried dependence on statement S1if and only if 1. S1references a location Xon iteration 𝑖, 78 2. S2references the location Xon iteration 𝑗, and 3. the loop iterates at least once between the references of X, i.e., the distance 𝑑between iterations is 𝑑(𝑖,𝑗)>0. 1for(i=0; i<N-1; i++) { 2A[i+1] = B[i]; S1 3B[i+1] = A[i]; S2 4}C* 012 i B A … S2S1 Listing 27: Loop-carried dependence. After the first iteration, in every iteration S2uses a value of array Acomputed in the previous iteration by S1. Similarly, S1uses a value of array B computed in the previous iteration by S2. There is a true dependence from S2to S1and from S1to S2, and both dependencies are carried by the loop. If we select any individual iteration and execute it alone, no dependence exists. If loop statements depend only on statements in the same iteration, then there exists a loopindependent dependence. A loop-independent dependence (Kennedy & Allen, 2001, p. 76) occurs when S1references a location Xon iteration 𝑖,S2references Xon iteration 𝑖, and there is a control flow path from S1to S2. Comparing the two loop dependencies, a loop-carried dependence determines the iteration order and whether that order can be transformed safely. A loop-independent dependence determines the statement execution order within a nest of loops. Dependence analysis. Dependence analysis (or a dependence test) is a technique for identifying or characterizing program dependencies and dependence-preserving reorderings; which may then permit transformation or parallel execution. Among the well-established techniques of dependence analysis are Banerjee test (Banerjee, 1997), GCD test (Zima & Chapman, 1990), Omega test (Pugh, 1991), and commutativity analysis (Rinard & Diniz, 79 1996). Section §2.2 will present a complementary dependence analysis inspired by implicit computational complexity. 1.2.4.4 Incorporating Parallelism If we only focus on sequential code, the notions around dependence are well-established. However, sequential reasoning is insufficient for effective use the parallelism that is available in modern processors. Developing and designing parallel software and algorithms is conceptually challenging. One of the major difficulties is the effort required to ensure that a parallel program is (functionally) correct. In addition to all the errors that arise in sequential programs, parallelism introduces a new class of bugs that includes race conditions. A race condition is devious because the runtime behavior of a program with such a bug is nondeterministic (Chapman, Jost, & Van Der Pas, 2007, p. 32). But in exchange for the challenge, parallelism provides the potential to improve the program’s runtime performance. In practice, exploiting parallelism is necessary for all performance-critical applications (Suomela et al., 2025). There are several good motivations for introducing parallelism in programs and for improving the existing parallelization techniques. High-performance multicore processors are ubiquitous and possess the abilities to execute several operations in a single clock cycle. Due to physics, improvements in hardware design now come from parallel processing capabilities, rather than adjustments in clock cycles. On the software side, a vast majority of legacy applications, and the algorithms that power them, were developed without parallelization in mind. Parallelizing compilers, that automatically translate sequential programs to multicore executables, have made big advances toward improving prevalence of parallelism. But despite the advances, these compilers make conservative choices and miss opportunities to parallelize (Holewinski et al., 2012). Correct and efficient parallel code is thus often hand-crafted in a process that is time-consuming and error-prone. 80 Ultimately, our abilities to parallelize programs relies on the potential parallelism available in the program and the processor; and the degree to which we can extract parallelism from a sequential program and find the best parallel schedule under the processor’s scheduling constraints (Aho, Lam, Sethi, & Ullman, 2007). No parallelization strategy fits all cases and it is important to facilitate the discovery of new strategies and parallel algorithms as complementary to existing techniques. For example, running automatic analysis on a large application can distinguish regions that can be parallelized automatically from those that need manual changes. From dependence to independence. Since dependence determines how program executions may be reordered, it provides a strong foundation for developing techniques to increase the parallelism available in programs. Parallelism inherently requires independence between statements; in other words, we are interested in absence of dependence. Thus, if we can design algorithms, or transform programs in ways that increase prevalence of independent statements, we improve the program’s parallelization potential. One focus area in parallelization concerns loop-level parallelism that aims is to extract parallel tasks from loops. For example, by the Loop Parallelization Theorem, it is permissible to convert a sequential loop to a parallel one if the loop carries no dependence (Kennedy & Allen, 2001, p. 82). The remainder of this section focuses precisely on the terms and techniques of parallelizing loops. Parallel programming models. Multiple sophisticated programming models exist to simplify the task of writing parallel programs. These models raise the abstraction level between the application code and the operating system-level parallelization mechanism of threading. The OpenMP application programming interface is presented in §1.2.4.5. Other approaches include the Parallel Patterns Library (PPL) (Campbell & Miller, 2011; Whitney, Sharkey, Jones, Blome, Hogenson, & Cai, 2021), that parallelizes tasks through built-in 81 algorithms and containerization; and the oneAPI Threading Building Blocks (oneTBB), a runtime-based model for C++ programs (oneTBB Contirbutors, 2025). 1.2.4.5 The OpenMP Programming Model OpenMP, for Open Multi-Processing, is a parallel programming model for developing portable, shared memory parallel applications in C,C++ and Fortran (OpenMP Architecture Review Board, 2024). OpenMP is not a programming language. Rather, it provides directives for sequential programs that translate the programs to parallel execution instructions at compile-time. The OpenMP infrastructure includes compiler directives, library routines, environment variables, and tool support for creating, debugging, and analyzing parallel applications. Program execution in OpenMP follows the fork-join programming model (Chapman, Jost, & Van Der Pas, 2007, p. 24) of Fig. 9. Program execution starts with an primary thread that runs in sequential mode. After encountering a specially-marked parallelizable program region, the primary thread spawns a team of threads in a fork-operation. The team collaborates to complete the tasks of the parallel program region. The execution concludes with a join-operation, where the forked threads terminate. The primary thread continues execution past the parallel program region, running again in sequential mode. 82 line of directives. By the data-sharing attribute clauses, the arrays Aand Bare explicitly shared across the threads and the iteration variable iis privatized. □ 1.2.4.6 Built-In Loop Transformations in OpenMP OpenMP includes built-in directives that perform loop transformations (OpenMP Architecture Review Board, 2024). A loop-transformation replaces the associated loop with a structured block that is another loop or a loop sequence. Unless otherwise specified, all generated loops have canonical form. Loop-iteration variables of generated loops are always private in the innermost enclosing construct. The loop transformations available in OpenMP are: fusion, interchange, reverse, split, stripe (interleaving of loop iterations), tile, and unroll. As an example, we consider the unrolling transformation. Loop unrolling. The unroll clause (OpenMP Architecture Review Board, 2024, p. 381– 382) transforms the associated loop based on the specification provided in the parallelization directive. The unroll clause is followed by either full or partial clause. The effect of full clause is to unroll the associated loop fully. Full unroll requires that the iteration count of the associated loop is a constant. Listing 34 shows the application of the directive and the loop post-transformation form is shown in Listing 35. 1#pragma omp for unroll full 2for(int i=0; i<4; ++i) 3A[i] += B[i] * c; OMP Listing 34: Applying full unroll. 1A[1] += B[1] * c; 2A[2] += B[2] * c; 3A[3] += B[3] * c; 4A[4] += B[4] * c; C Listing 35: Fully transformed loop. 89 The partial clause takes an integer-valued unroll factor. The effect of partial clause is to tile the loop, using the unroll factor as the tile size. Then, the generated tile loop is fully unrolled. If no unroll factor is specified, the unroll behavior depends on the implementation. Partial transformation is illustrated in Listing 36 and Listing 37. 1#pragma omp for unroll \ partial(4) 2for(int i=0; i<n; i+=1) 3A[i] += B[i] * c; OMP Listing 36: Applying partial unroll. 1for(int i=0; i<n; i+=4) { 2A[i] += B[i] * c; 3if(i+1< n) 4A[i+1] += B[i+1] * c; 5if(i+2< n) 6A[i+2] += B[i+2] * c; 7if(i+3< n) 8A[i+3] += B[i+3] * c; 9}C Listing 37: Partially transformed loop. Applying loop transformations requires suitable loop form. For example, the worksharing loop expects loops to be in canonical form. Afterward, a transformation that increases the program’s parallelization potential enables making use of multicore hardware during execution. Thus, an important challenge of parallelizing compilers and program optimizations is to find generalized strategies to increase parallelization potential. 1.2.4.7 ICC for Parallel Loop Transformations Since implicit computational complexity has developed many systems for reasoning about loops, it seems natural that in extended use, it has potential to support loop-based program 90 transformations. Founded on this concept, §2.2 presents an ICC-based technique to increase parallelization potential in imperative programs. The technique uses a static data dependence analysis that detects independent blocks of commands inside loops. Through a loop fission transformation, then independent blocks are then transformed into multiple parallelizable loops, as illustrated in Fig. 11. Sequential loop Parallelizable loops transformation Figure 11: Loop fission of a sequential loop into parallelizable loops. The loop header (the leading block) is replicated across the generated parallellizable loops. In the sequential loop body, the colors denote (disjoint) dependence between command blocks. Each generated parallellizable loop takes a part of the original loop’s body. The technique is interesting because it is applicable even when the loop iteration space is unknown; enabling parallelization of e.g., while loops. Such non-canonical loops are traditionally outside the built-in transformation and parallelization capabilities of parallel programming models like OpenMP. Although the iterations of while loops must be executed under the single construct, the multiple loops generated by the transformation can be parallelized with OpenMP directives. The technique is useful as a preprocessor, before adding parallelization directives; and in conjunction with other loop transformations. The technique is inspired by (Moyen, Rubiano, & Seiller, 2017a), but was adjusted significantly to support the different application. 91 1.2.5 Confidentiality and Non-Interference Computer security is a broad, interdisciplinary field with technical and non-technical challenges. An important subset of the technical aspects can be modeled and studied mathematically (Piessens, 2024). At its core, computer security is concerned with three properties: confidentiality, integrity, and availability (Du, 2017). Although the precise meaning of these terms is situational, they are generally described as follows (Bishop, 2019, p. 4–6). Confidentiality is about concealment of protected assets, like secret information and resources. The goal of confidentiality is to ensure protected assets are viewed by authorized users only. By extension, it includes concealing knowledge about the existence of protected assets. Confidentiality is compromised if secrets are exposed, or “leak|seealsoviolation”, to unauthorized users. Integrity is about trustworthiness of information and resources. It aims to ensure protected assets are modified by authorized users only and that those modifications preserve authenticity of the resource. For example, an update to a date field should yield a legitimate date. Integrity is difficult to guarantee because it concerns assets over mutations, transmissions, and time. Authentication is a critical (though an insufficient) mechanism to enforce integrity. Integrity is often considered the dual of confidentiality (Biba et al., 1977). Availability refers to the ability to access and use authorized system and its assets. Availability is compromised if a computational system is unusable or incapable of supporting its intended use – to include unavailability due to excessive service latency. The challenge of computer security is to find the right balance between the three properties – preventing unauthorized views and modifications, while preserving access and supporting authorized use. Among the strategies are designing techniques to prevent improper use, 92 detect issues, and recover from compromised scenarios. Although all three properties are important, the rest of this presentation focuses on confidentiality. Confidentiality can be enforced with numerous mechanisms, e.g., firewalls, access control, and encryption. A firewall is a network-layer protection, and an operating system implements and maintains access control. Encryption protects secret information until decryption, but its excessive use is problematic for availability. In general, those mechanisms are insufficient to provide end-to-end guarantees through all layers of computation. One problem is that confidentiality is not guaranteed after secret information is released as input to a program (Zdancewic, 2004). Information flow security is concerned with achieving fine-grained confidentiality (and integrity) guarantees by tracking information propagation during program executions (Eggert, 2014; Hedin & Sabelfeld, 2012). 1.2.5.1 Information Flow Security Protected assets may require different levels of confidentiality. Computer systems that protect assets at different security levels need controlled information flow. The capability to process assets at different security levels is called multilevel security (MLS) (Bossi, Macedonio, Piazza, & Rossi, 2005). Illustrated in Fig. 12, the United States federal government document classification scheme (Wikipedia contributors, 2025) is one example of a multilevel security system (Feiertag, Levitt, & Robinson, 1977). The permissions cascade: having access to a specific level grants access to all the levels below it. For example, accessing “secret” documents requires permission at secret or top secret level. The main idea for achieving secure multilevel information flow is to impose constraints on how privileged information is permitted to flow within the system. Secure information flow is a confidentiality guarantee, because it aims to ensure secrets do not leak to unauthorized 93 top secret secret confidential unclassified highest lowest Figure 12: The United States federal government document classification scheme. parties (Piessens, 2024). Implementing secure information flow requires three steps (Eggert, 2014). 1. Identifying security classes (alternatively, domains or user groups). In Fig. 12, the classes are top secret, unclassified, secret, and confidential. 2. Defining a confidentiality policy. The policy specifies how information is permitted to flow between the security classes. In Fig. 12, the the directed arrows define the policy. 3. Instrumenting an control. A control is a mechanism that enforces the behavior permitted by the policy. In Fig. 12, no control is specified. For strong confidentiality guarantees, the information flow approach should also consider and protect against side channels. Side channels are all system characteristics that enable a malicious actor to deduce secrets, indirectly and without assistance from other users (Bishop, 2019, p. 280). In terms of program executions, a few examples of side channels are termination (Stefan, Russo, Buiras, Levy, Mitchell, & Maziéres, 2012), divergence, deadlocking, and execution latency (Lawson, 2009). 94 1.2.5.2 The Elements of Information Flow Information flow is an observable action between two agents27 𝐴and 𝐵(Eggert, 2014). If an action performed by 𝐴is observable to 𝐵, then there exists an information flow from 𝐴to 𝐵. The information flow is explicit if it is directly observable from a single action. The insecure program in Listing 38 shows an example of direct information flow between high and ret. Information flow is implicit when it is not directly observable, but the initial action can be deduced from the sequence of actions that follow. The insecure program in Listing 40 shows an example of an implicit flow. The initial value of variable his deducible from the returned value l, even though there is no direct flow from hto l. Information flow policy (IFP) is a statement of what is, and what is not, permissible between security classes (Bishop, 2019, p. 9). Since the seminal works on information flow (Bell & La Padula, 1976; Biba et al., 1977), it has been a convention to model information flow policies with lattices (Denning, 1976). The most simple case considers two security classes, typically “high” and “low” (ℎ,𝑙)(or trusted and untrusted, secret and public, etc.). In the simple case, the policy condition is that no information should flow from high to low. (Bossi, Macedonio, Piazza, & Rossi, 2005) Then, showing that such a system is secure requires proving that executions that differ only on secrets are indistinguishable (Piessens, 2024). A policy that restricts information flow from a lower security class to a higher security class is called a non-interference policy, presented in §1.2.5.4. Information flow control (IFC) is a mechanism that enforces a policy (Bishop, 2019). Designing adequately expressive and effective controls is an active topic in security research (Bossi, Macedonio, Piazza, & Rossi, 2005; Sabelfeld & Myers, 2003; van 27We use the term agent to emphasize an abstraction. An agent could be a human user, computer system, web request, program variable, etc. 95 der Meyden & Zhang, 2007). Like in static analysis (cf. §1.2.2.1), designing a sound and complete control for arbitrary programs is impossible. A sound IFC guarantees to find all policy violations and a precise IFC avoids raising excessive false alarms. However, an overly restrictive IFC is challenging because it compromises availability. The challenge of information flow control is more nuanced than classic data-flow analysis of functional properties, because an IFC must consider a program w.r.t. policies and multiple executions (Frumin, Krebbers, & Birkedal, 2021). Thus, the same program can have multiple judgments depending on the policy. Declassification refers to controlled release of secret information (Sabelfeld & Sands, 2009). Declassification requires a downgrading operation; a mechanisms that permits an elevated security judgement to be lowered. In other words, information is allowed to flow contrary to the policy (Cecchetti, Myers, & Arden, 2017). Declassification is necessary to support real world security applications. For example, after a failed login attempt, an unauthorized user is able to observe the effect of the failure, although this is an information leak. Declassification is generally not safe (Derakhshan, Balzer, & Yao, 2024), and thus poses a major design challenge to IFCs. In the context of integrity, declassification is also called endorsement (Marion, 2011). Secure and insecure information flows. Figures 38–40 show basic examples of insecure and secure information flows. Variables high,secret, and hare assumed to be secret and their values should not leak from executions. The programs are fragments from the IFSPEC benchmark suite (Hamann, Herda, Mantel, Mohr, Schneider, & Tasch, 2018a) available at (Hamann, Herda, Mantel, Mohr, Schneider, & Tasch, 2018b). The more advanced benchmarks involve, e.g., aliasing, reflection, context sensitivity, and exception handling. 96 1boolean ret; 2ret = (high && true); 3return ret; Java Insecure. 1boolean ret; 2ret = (high || true); 3return ret; Java Secure. Listing 38: Boolean Operations. The programs are parametric on a Boolean variable high. In the insecure version, the value of high is deducible from the value of ret. 1int[] arr = new int[5]; 2arr[0] = secret; 3if (arr[0] == 42) 4println("Found"); Java Insecure. 1int[] arr = new int[5]; 2arr[0] = secret; 3if (arr[0] == 42) 4println("checked"); 5else 6println("checked"); Java Secure. Listing 39: Arrays Implicit Leak. The insecure program’s output reveals if the value of secret is or is not 42. This leak is small, since it corresponds to 1 bit of information. However, the secure version reveals nothing about the value of secret. 1int f(int h, int l) { 2while (h>0) { h--; l++; } 3return l; 4}Java Insecure. 1int f(int h, int l) { 2while (h > 0) { h--; } 3return l; 4}Java Secure. Listing 40: High conditional incremental leak. The insecure version reveals implicitly the value of the secret variable hthrough variable l. The leak reveals every value of hprecisely. In the secure version, value of hcannot be deduced. But even the secure version may be vulnerable over a side channel, if the loop execution time is observable to an attacker. 97 1.2.5.3 Techniques for Information Flow Modeling and Analysis Information flow can be modeled in several distinct ways. One way to categorize these approaches is by how they model systems; e.g., state-based automata, trace-based model, and process algebras (van der Meyden & Zhang, 2007). The presentation in this dissertation is only concerned with approaches based on programming languages. The study of security through programming languages is called language-based security (Sabelfeld & Myers, 2003; Schneider, Morrisett, & Harper, 2001). The goal of language-based security is to use principles of programming languages—semantics, analysis, type systems, rewriting, etc.— to strengthen application security. However, to offer a point of comparison, we introduce briefly trace-based information flow. The language-based and trace-based approaches have very little in common (Eggert, 2014, p. 235). Language-based information flow. Language based security formulates information flow constructs through programming languages. Program logics and security type systems are among the common techniques (Frumin, Krebbers, & Birkedal, 2021). A security type system aims to guarantee the security policy induced by its lattice (Marion, 2011). Each variable is assigned a security type, i.e., a label that indicates its security class. A satisfactorily secure program must pass a compile-time type check of the security labels. Sections 1.2.5.4 and 3.2 discuss the language-based information flow in more detail. Trace-based information flow. The trace-based approach (Eggert, 2014, p. 24) models a system with a state machine. In response to actions, the machine transitions, deterministically or nondeterministically, from state to state. A trace is a sequence of actions of such a machine (Nelson, Bornholt, Krishnamurthy, Torlak, & Wang, 2020). Evaluating secure information flow over traces is about equivalence relations, or indistinguishability. For example, for a policy that requires that secrets should not leak to public, two traces must be 98 𝐶 ∶∶=skip ∣v≔e∣𝐶1;𝐶2∣if e then 𝐶1else 𝐶2∣while e do 𝐶 Figure 13: Grammar of the non-interference security type system. ⊢e∶𝜏 (expression typing) E-HIGH ⊢e∶h E-LOW h∉𝑣𝑎𝑟𝑠(e) ⊢e∶l Γ⊢C(command typing) C-SKIP Γ⊢skip C-ASSIGN1 ⊢v∶h Γ⊢v≔e C-ASSIGN2 ⊢e∶l l⊢v≔e C-SEQ Γ⊢𝐶1Γ⊢𝐶2 Γ⊢𝐶1;𝐶2 C-WHILE ⊢e∶Γ Γ⊢𝐶 Γ⊢while e do 𝐶 C-IF ⊢e∶Γ Γ⊢𝐶1Γ⊢𝐶2 Γ⊢if e then 𝐶1else 𝐶2 C-SUB h⊢𝐶 l⊢𝐶 Figure 14: A non-interference security type system. which reads: If two input states share the same low values, then the behaviors of the program executed on these states are indistinguishable by the attacker. The security typing rules are shown in Fig. 14. For the typing rules, an expression ⊢e∶𝜏 means ehas type 𝜏. The judgement Γ ⊢ Cmeans the program Cis typable in security context Γ. Expression types and security contexts can be either low (𝑙) or high (ℎ). The symbol Γrefers to the current context (low or high). 105 Derivations. Consider the programs in Figures 38–40. Since the programs are written in Java, the constructs are richer than available in the type system grammar. The programs are not fully analyzable. For example, the security type system does not specify how to handle the array in Listing 39. However, we can analyze sub-programs, like the while loops in Listing 40 through a mapping to the grammar. The following examples show basic non-interference derivations. Example 15 (Secure high conditional incremental leak).We will analyze the following program fragment. while (h>0) { h--; } Java We assume his an arbitrarily typed variable—neither low or high—and will analyze both cases. We map the program to the grammar by substituting h > 0with e0and h-- with v:=e1to obtain while(e0) { v:=e1}.30 Case 1: e0,v, and e1are of type high. Since the program is derivable as follows, it is non-interfering. E-HIGH ⊢e0∶hC-ASSIGN1 h⊢v:=e1C-WHILE h⊢while(e0) { v:=e1} Case 2: e0,v, and e1are of type low. The program is also derivable in low context, and again, is non-interfering. 30We will lose detail of the compound assignment, but the loss is acceptable for this example. 106 h∉vars(e0)E-LOW ⊢e0∶l h∉vars(v:=e1)E-LOW ⊢v:=e1∶lC-ASSIGN2 l⊢v:=e1C-WHILE l⊢while(e0) { v:=e1} Intuitively, the program is always non-interfering because it processes only high (secret) values, or low (public) values; never mixing the two security classes. □ Example 16 (Insecure high conditional incremental leak).We analyze the following program. It is labeled insecure in the benchmark suite. while (h>0) { h--; l++; } Java The goal of this example is to reveal the assumptions that make it insecure. Using a similar procedure as in Ex. 15, we express the program in the type system grammar as while(e0) { v1:=e1; v2:=e2} To maintain the original information flow behavior, expressions e0,v1,e1(resp. v2and e2) must be typable in the same security class. We also know from Ex. 15 that without multiple security classes, the program is non-interfering. There are two interesting cases. Case 1: e0,v1,e1are high, and v2,e2are low. The derivation beings as follows. E-HIGH ⊢e0∶h C-ASSIGN1 h⊢v1:=e1X⊢v2:=e2C-SEQ h⊢v1:=e1; v2:=e2C-WHILE h⊢while(e0) { v1:=e1; v2:=e2} Since v2is of type low, there is no way to handle v2:=e2. The derivation gets stuck at point marked Xbecause the program has a non-interference violation. Intuitively, it is because the program operates on a low variable inside a loop with a guard variable that is of type high. This construction is not safe because it leaks information. 107 Case: e0,v1,e1are low and v2,e2are of type high. h∉vars(e0)E-LOW ⊢e0∶l h∉vars(e1)E-LOW ⊢e1∶lC-ASSIGN2 l⊢v1:=e1 C-ASSIGN1 h⊢v2:=e2C-SUB l⊢v2:=e2C-SEQ l⊢v1:=e1;v2:=e2C-WHILE l⊢while(e0) { v1:=e1; v2:=e2} Reversing the security label configuration makes the program typable. A critical rule is CSUB (subsumption) that permits lowering the security class label of a high command. Unlike in the previous case, the loop guard is now low type. It permits manipulating a variable of high type inside the loop body. □ 1.2.5.6 Security Meets Implicit Computational Complexity With a common focus on restrictions, it seems intuitive that techniques from implicit computational complexity would pair elegantly with information flow and applications in languagebased security. The combination can potentially provide two types of correctness guarantees, relating resource analysis and security. Supporting this hypothesis, there are already multiple series of work exploring connections between the two domains. This section gives a brief summary of those results. Complexity via non-interference: SAFE programs. The class of SAFE programs is foundational in demonstrating that non-interference security type systems can support implicit characterizations of complexity classes. The idea was introduced by Jean-Yves Marion in (Marion, 2011). SAFE programs continue to be actively investigated by Marion, Emmanuel Hainry, Romain Péchoux, and others. 108 Starting with the principle of tiering,31 Marion extended the principle to characterize the class of polynomial time computable functions. A critical step in obtaining this result was combining tiering with a type system for secure information flow. Each variable is assigned a type – a tier of either 0 or 1 – representing elements of a complexity lattice. The paper then shows that terminating and well-typed programs are computable in polynomial time. SAFE programs is precisely the class of programs captured by this characterization. Judging by the number of works that followed, the technique was inspirational. The subsequent results have provided extensions mainly along two directions. The first has focused on programming language paradigms, including: concurrent fork-join processes (SAFE processes) (Hainry, Marion, & Péchoux, 2013), dynamic data structure (ramified programs) (Leivant & Marion, 2013), and object-oriented (OO) programs (Hainry & Péchoux, 2015). The OOP result is the first characterization of polynomial time computable functions in the object oriented paradigm. The second directions has focused on redefining the system restrictions, with the goal of improving intensional completeness. For example, the class of stratified programs (Hainry & Péchoux, 2023) characterizes a strictly larger class than SAFE programs, by using a combination of security type system, heap memory restriction, and shape analysis. With the same end-goal, aperiodic programs (AP) (Hainry, Kapron, Marion, & Péchoux, 2024) extends SAFE programs by using declassification; another mechanism adopted from the security domain. In the latter, the main result is a proof that SAFE and terminating aperiodic programs is the class of Basic Feasible Functionals, i.e., JSAFE ∩AP ∩terminating =BFFK(Hainry, Kapron, Marion, & Péchoux, 2024; Hainry, Kapron, Marion, & Péchoux, 2020). 31The intuition behind tiering, a.k.a. ramification, is that program execution time depends on the nature of information flow during executions. The flow can be constrained by imposing a precedence relation that regulates the information flow, e.g., from higher tier to lower tier (Leivant & Marion, 1995, 2013). 109 From complexity to cryptography. A separate series of works applies implicit computation complexity toward applications in cryptography. The application is natural, because the security of cryptographic schemes is formulated as a mathematical problem, where the goal is to show the scheme is not to be solvable by a feasible adversary. The term feasible refers to computable in polynomial time (Férée, Hym, Mayero, Moyen, & Nowak, 2018). This application is naturally, because in showing that a cryptographic scheme is secure, adversarial capabilities must restrict available computational power (Heraud & Nowak, 2011). Formalized safe recursion. The formalization of safe recursion was motivated by its envisioned usefulness in cryptographic proofs (Heraud & Nowak, 2011). At the time of its appearance, the technique was integrated into the Certicrypt proof assistant, for cryptographic proofs (Barthe, Grégoire, & Zanella Béguelin, 2009). However, Certicrypt has since then been superseded by EasyCrypt (Barthe, Dupressoir, Grégoire, Kunz, Schmidt, & Strub, 2014). The support for complexity proofs in EasyCrypt is limited (Barbosa, Barthe, Grégoire, Koutsos, & Strub, 2023). Thus, the integration of safe recursion did not survive the “test of time”. Type system dℓT. The type system dℓT (Baillot, Barthe, & Dal Lago, 2015, 2019) is simultaneously complexity-aware and has capabilities to support cryptographic proofs. Among its applications, dℓT allows proving that the constructed adversary for the Goldreich-Levin Theorem is polynomial time. Such applications are interesting because they involve computations that are inherently non-polynomial in time complexity. Because ICC systems are traditionally designed to characterize at most polytime computations, handling sub-computations that exceed this class requires unconventional flexibility from an ICC system. A limitation of dℓT is that it has not been implemented. 110 Both dℓT and the formalization of safe recursion have inspired other mechanized proofs (Barbosa, Barthe, Grégoire, Koutsos, & Strub, 2021; Férée, Hym, Mayero, Moyen, & Nowak, 2018). 1.2.5.7 From Quasi-Invariant Chunks to Non-Interference Reinforcing the existing connections, §3.2 presents a program logic for non-interference. The logic is inspired by implicit computational complexity. The motivating idea was to explore the power and usefulness of ICC techniques in language-based security. The logic analyzes information flows in imperative programs. It abstracts information flow patterns between variables into matrices. Once the matrix is paired with a security policy, it is possible to evaluate whether the program satisfies an anytime non-interference property, which is introduced in the paper. The technique is a refinement of prior works (refer to §2.2 and (Moyen, Rubiano, & Seiller, 2017a)). A previous version of the logic was used to obtain a compile-time program optimization (in §2.2). Although the logic no longer guarantees complexity bounds, it demonstrates the benefit of connecting techniques between the ICC and security. Adjusting the logic to track non-interference revealed various mathematical insights. For example, the treatment of loops is more straightforward for non-interference than complexity analysis, because the latter requires fixed point computations. As a data flow analysis, that tracks different program properties based on dependence, the QI framework is reminiscent of the Dependency Core Calculus (DCC) (Abadi, Banerjee, Heintze, & Riecke, 1999). The multiplicity of the program logic suggests it may possess representational capabilities similar to DCC. 111 1.2.6 Programs Proofs for Formal Reasoning The size and complexity of modern software makes it almost impossible to avoid implementation errors. Asynchronous computation, the rich array of computing environments and their communication, and continuous modifications of source code are among the challenges that can lead to software “going wrong”. Prominent and costly examples of failures include the Ariane 5 rocket explosion on its maiden flight (Ariane 501 Inquiry Board, 1996), the Therac-25 radiation therapy machine with six instances of lethal overdoses (Leveson & Turner, 1993); and the loss of NASA’s Mars Climate Orbiter (Mars Climate Orbiter Mishap Investigation Board, 1999). In more recent memory, the CrowdStrike incident caused multiple days of system outages across critical infrastructure like airports, banks, and hospitals (Wikipedia contributors, 2024). In a case involving the University System of Georgia (USG) (2024), a software-related failure exposed sensitive personal information of USG employees with potential harm to the Augusta University community. Unreliability of software is not isolated to these few publicized instances. A pithy comment in Dijkstra (1970, p. 3) captures a similar sentiment. Present-day computers are amazing pieces of equipment, but most amazing of all are the uncertain grounds on account of which we attach any validity to their output. The context of Dijkstra’s statement is modest compared to exploding rockets. It refers to the operation of multiplying two 27-bit integers. Checking that a calculator actually performs the correct operation for all inputs—i.e., meets its specification—at a rate of few microseconds per input-pair, would require more than 10,000 years. Thus, skepticism around soft112 ware correctness is a long-held position among some computer scientists. It is also the core issue tackled by formal methods. Formal methods motivations and challenges. Formal methods aims to remove uncertainty by providing techniques that allow establishing strong behavioral guarantees. Formal methods is deeply rooted in mathematics and logic (Shankar, 2023). In this view, programs are defined as precise mathematical models with specifications. The specification defines what behavior is expected from the model under study. Formally verifying a program involves constructing a proof that the model satisfies its specification. In contrast to manual inspection and tests—like a test of inspecting the multiplication result of some input-pairs— a proof conclusively ensures correctness for all inputs, at the model’s level of abstraction. As noted later by Dijkstra (1972), “[t]he only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness.” The motivation for using formal methods is based on the strength of guarantees it provides. Being formal helps when the goal is to be precise (Leino, 2023). However, thinking formally requires a different engineering mindset. Instead of thinking of all possible scenarios and how they might go wrong, formal reasoning requires defining how a system is expected to work, and identifying conditions that must be met to ensure the correct behavior (Cook, 2024). Those conditions are then formally verified with proofs. Despite the clear benefits, wider adoption of formal methods continues to face many challenges. These include e.g., resource investment (crafting and maintaining formal proofs is time-consuming), tooling and tool maintenance, and technical education (ter Beek et al., 2024). Another challenge concerns the methods themselves. The Four Color theorem is the first famous result with a proof that requires large computer calculations. When the proof appeared in 2008, such proofs were still controversial. The source of the controversy was that computer programs could not be reviewed with mathematical rigor (Gonthier, 2008). 113 Thus, advancing formal methods also concerns improving communication about the available capabilities and offered guarantees. We can envision […] a world in which computer programs are always the most reliable components of any system or device (Hoare, Misra, Leavens, & Shankar, 2021). 1.2.6.1 Foundational Concepts Formal models. A formal model is an abstract description of a computer system of interest. In the context of this dissertation, the systems of interest are programs. Then, a formal model is used to reason about the program and the consequences of design choices relating to the program (Ölveczky, 2017; Zave & Nelson, 2023a). The formal model is expressed in (some) modeling language (refer to Table 8 for examples of modeling languages). The choice modeling formalism should enable expressing the model as naturally and intuitively as possible, while still generating mathematically precise structures (Ölveczky, 2017; ter Beek et al., 2024). The formalism should (i) omit unnecessary technicalities, (ii) enable focusing on the problem of interest, at an appropriate level of abstraction, and (iii) facilitate analysis and reasoning about the program (Ölveczky, 2017). Specifications. Aspecification is a part of the formal model that describes the behavior of the program (Zave & Nelson, 2023b). The specification should be simpler and easier to comprehend than the implementation (Zave & Nelson, 2023b). Temporally, the development of the specification should precede the implementation, or minimally be developed concurrently (Dijkstra, 1972). Critically, we want the specification to be independent from the implementation (Furia, 2014). Independence isolates the mathematical properties of interest and enables showing that the implementation is consistent with those properties. In 114 verification, where the verification process is based on some form of logical inference, i.e., deduction. The properties to be proven are expressed in a formal specification language, as structured comments, next to the program constructs they relate to (Hähnle & Huisman, 2019). A deductive verifier them aims at to prove that all possible behaviors of a program satisfy the specification using the available program annotations (Cassez, Fuller, & Quiles, 2022). The remainder of this section briefly introduces two tools for formal methods: the (interactive) Rocq theorem prover (§1.2.6.3) and the verification-aware programming language Dafny (§1.2.6.4). These tools are relevant for some of the dissertation manuscripts and assumed to be familiar to the reader. 1.2.6.3 The Rocq Theorem Prover The Rocq theorem prover is an interactive proof assistant for machine-checked formal reasoning. It provides a rich and flexible environment for various proof developments. Rocq is a widely-adopted tool in the programming languages research community. Among its applications are formal assurance of mathematics, semantics, and verification. In 2013, The ACM has recognized Rocq with the Software System Award – the highest distinction awarded to research software (The Rocq Development Team, 2025a). The success of Rocq has also created abundant interest in dependent type theory (Coquand & P. Huet, 1988), i.e., the core logic of Rocq. Technical overview. As a guiding example, consider simple proof in Listing 42. The lemma keywords starts a statement that we wish to prove. The specification language for stating theorems is called Gallina. The code between Proof and Qed is a proof script. Proof scripts consists of tactics. Tactics perform operations on the proof state and make explicit 121 the steps needed to prove the associate lemma. The Rocq prover comes with dozens of built-in tactics. In the example, intros,simpl and reflexivity are tactics. The tactic language is called Ltac. 1Lemma add_0_l : ∀(n : nat), 0 + n = n. 2Proof. 3intros.simpl.reflexivity. 4Qed.Rocq Listing 42: A simple proof in Rocq. Proof engineers write proof scripts incrementally. At each step (marked with a period) it is possible to evaluate the proof and see what goal should be proved next. Refer to Fig. 16 for a visual example. In the editor, the goal (on top right) shows the current proof state. A full-fledged proof development consists roughly of definitions, lemmas, and proofs. Definitions describe the abstract structures we want to reason about in the mechanization. Lemmas prove facts about the structures.35 Definitions and lemmas provide the specification of a proof development. Formal verification then reduces to discovering the proofs that show that the specification is satisfied. A finished proof is machine-checkable to everyone familiar with these technical basics. A program proved in Rocq can be extracted to other target languages. The functional languages currently available as output targets are OCaml, Haskell and Scheme (The Rocq Development Team, 2025b). Mathematical Components. The Mathematical Components library—colloquially mathcomp—extends the Rocq ecosystem with an extensive collection of formalized mathematical theories. The library covers a wide spectrum of topics, including formal theory 35In Rocq tThe distinction between a lemma, theorem, corollary, etc., is just syntactic sugar. 122 Figure 16: A development view of the simple Rocq proof. The Emacs editor is enhanced with the Proof General interface and the Company-coq plug-in. The left view contains the proof code under development. Focusing between Proof and Qed activates the proof mode. While in proof mode, the proof state is visible in the top-right view. The bottom-right view shows the search results, of a database lookup, for existing lemmas that are similar in form to the current goal. of general purpose data structures—like lists, prime numbers, and finite graphs—and advanced topics in algebra. The theories are organized into hierarchical levels where the design facilitates reuse. The proof style is based on Rocq, but Mathematical Components uses a specialized language extension called SSReflect (small-scale reflection). SSReflect significantly influences proof writing style and poses its own learning curve. To demonstrate the difference, §1.2.6.5 shows examples in “standard” Rocq and SSReflect. The Mathematical Components library has an essential role in the Rocq community because several landmark results of finite group theory are based on it. For example, the mechanical proofs of the Four Color theorem (Gonthier, 2008) and the Odd Order theorem (Gonthier et al., 2013) utilize the library extensively. 123 Demonstrated applications. Conventional uses of Rocq include proving properties of programming languages, formalizing mathematics, and teaching. Table 9 contains representative examples in the first two categories. Additional resources. There are multiple literature sources for learning more about Rocq. Coq’Art (Bertot & Castéran, 2004) is the first book dedicated to the proof assistant and its theory. The Software Foundations (Pierce et al., 2025) book series is a hands-on, active learning experience. The books are implemented in Rocq and updated regularly. The Mathematical Components book (Mahboubi & Tassi, 2022) provides a guide to using the library and the SSReflect proof language. Karate Coq of Affeldt (2025) is an additional resource about Mathematical Components. There are multiple books about engineering Rocq proofs with dependent types and type systems (Chlipala, 2013, 2022; Sergey, 2014; Smolka, 2025). For a curated list of awesome Coq libraries, plugins, tools, and resources see the Awesome Coq list (The Rocq Community, 2025). Finally, the Rocq prover has an active community, with discussion forums and a mailing list (The Rocq Development Team, 2025a). 1.2.6.4 Dafny: The Verification Aware Programming Language Dafny is an open source verification-aware programming language, and a verifier for functional correctness (Dafny Language Developers, 2025; Leino, 2010a). Dafny was designed for reasoning, and it can automatically check programs against specifications during program development. Fig. 17 shows a visual overview of the verification workflow. Technical overview. Dafny is a hybrid language, influenced by Java and C#. It has both functional and object-oriented features. They include curly-bracket block-style, (mathematical) functions, and inductive and co-inductive data types. The programming constructs 124 Formalization target Authors 𝜋-calculus in (Co)inductive-type theory Honsell, Miculan, & Scagnetto (2001) Gödel-Rosser Incompleteness Theorem O’Connor (2005) Modal model of impredicative semantics Appel, Melliès, Richards, & Vouillon (2007) Four Color TheoremaGonthier (2008) Verified Optimizing C Compiler, CompCertbc Leroy (2009) Flocq: floating-point numbers Boldo & Melquiond (2011) Bedrock: low-level programming library Chlipala (2011) Safe Recursion – §1.2.1.3 Heraud & Nowak (2011) Desargues’s Theorem in projective geometry Magaud, Narboux, & Schreck (2012) Feit-Thompson’s Odd Order Theorem Gonthier et al. (2013) Coquelicot: Real Analysis Boldo, Lelay, & Melquiond (2014) Homotopy Type Theory (HoTT) Bauer, Gross, Lumsdaine, Shulman, Sozeau, & Spitters (2017) Regular Language representations Doczkal & Smolka (2018) Caspar blockchain finality Palmskog, Gligoric, Pena, Moore, & Roşu (2018) Interaction Trees: Recursive and impure programs Xia et al. (2019) Undecidable Problems Forster et al. (2020) SSProve: modular cryptographic proofs Haselwarter et al. (2023) abased on (Robertson, Sanders, Seymour, & Thomas, 1997) and (Appel & Haken, 1989) bA verifying compiler is one of the grand challenges for computing research posed in Hoare (2003) cCompCert received the ACM Software System Award in 2021. Table 9: A small sample of results formalized with the Rocq prover. 125 Dafny source file typically *.dfy Dafny AST Boogie intermediate verification language SMT formulas Verification result Correctness, error model, or timeout Output Parsing Translation Verification condition generator SMT solver Figure 17: A (simplified) overview of Dafny implementation and verification workflow. “A welldesigned language and verifier, plus a great SMT solver, go a long way.” – Leino (2010b). include loops, if-statements, arrays, classes and methods; variables, types, generics, lambdas, inheritance, etc. (Dafny Contributors, 2025) The real power of Dafny comes from the ability to annotate methods to specify their behavior. For verification tasks, the idea is to define specifications and write proofs aside the implementation, in deductive verificationstyle. The built-in verification constructs include preand postconditions; loop invariants, termination metrics, lemmas, and ghost constructs.36 This language design enables writing functionally-correct verified programs fully in Dafny (Leino, 2023). Dafny programs can be compiled to various target languages, like C#, Java, and Go (Dafny Contributors, 2025). Dafny has an associated static program verifier. The role of the verifier is to check a program’s specification constructs.37 As visualized by the chart in Fig. 18 (inspired by (Leino, 2010b)), the built-in verifier in Dafny adds a high degree of automation. The verifier resolves many low-level proof steps. For example, if we wanted to prove the lemma of Listing 42 in Dafny, the verifier succeeds at discharging the proof obligations automatically – see Add0Left in Fig. 19. 36Aghost is any construct that is used for verification only; they are erased during compilation (Leino, 2023, p. 19). 37These are Eiffel-like contracts from (Meyer, 1988). 126 Automation Assurance functional correctness manual verification limited verification proof assistants SMT solvers static checking Dafny Figure 18: Automation degree. A program accepted by the Dafny verifier is guaranteed to be totally correct, i.e., it terminates and satisfies its specification. During program development and when given a candidate specification, the verifier runs automatically on code edits, as shown in Fig. 19. The engineer receives immediate feedback on the verification efforts. When Dafny verifier fails, the engineer must annotate the program with additional guidance—assertions, preconditions, lemmas, etc.—to assist the verifier, until the verification succeeds. Logical contradictions, like the ones raised in Fig. 19, will obviously never succeed. The verifier helps to catch such errors early, during program development. Proof style. In Dafny, proofsare developed in “top-down” style. This allows the developer to focus on the proof architecture before the detailed proof steps. To this end, Dafny provides assume statements, i.e., assertions without a proof; and ghost methods, i.e., lemmas that are not yet proven. Obviously, the proof is not complete until these temporary constructs have been replaced with concrete proofs. However, they are useful for facilitating the proof development. Boogie. Boogie (Leino, 2008) is an intermediate verification language, used in the verification workflow of Dafny programs (cf. Fig. 17). More generally, Boogie is an open 127 Figure 19: The Dafny verifier checking Dafny code running in Visual Studio Code. A big green check nmeans the verifier succeeds at proving the corresponding program construct. A big red cross oidentifies program constructs that fail to verify completely, even if some inner declarations succeed. A green filled check ¬means the verifier succeeds at the proof obligation at the corresponding line. The verification fails at declarations marked with a red block and::::: squiggly:::::: underline. 128 source modeling language and a verification tool for sequential and concurrent programs, and distributed systems (Microsoft, 2025). It provides a layer on which to build program verifiers.38 When viewed as a verification tool, Boogie takes as input a program written in the Boogie language. Then, the tool infers invariants, generates verification conditions, and passes them to an SMT solver. The default SMT solver is Z3 (de Moura & Bjørner, 2008). Applications of Dafny. Dafny is a mature, industry-grade tool for program verification. It has been used in research projects, industrial applications, verification projects, and in teaching formal methods. Among the hallmark results, the AWS authorization engine— that handles 1 billion API calls per second (Wagner & McLaughlin, 2024)—is verified in Dafny (Chakarov et al., 2025). 1.2.6.5 Tool Comparison by Light Examples This section covers three verification tasks that are suitable for paper presentation while illustrating differences between the formal proof techniques. To match the dissertation theme, the examples are about program proofs. However, proving programs is only a subset of the general utility of these tools. Refer to Table 9 for more cases. Program Equivalence. Listing 1, in the Introduction Chapter, showed two programs with a claim that the programs are equivalent. Equivalence means that, for all inputs, the programs compute the same result. With manual inspection, one can become reasonably convinced that the claim is true. However, such inspection provides only weak informal guar38Several program verifies are built on Boogie, for example Dafny, Chalice, Spec#, and Move (Microsoft, 2025). 129 antees. We can do better – we now have the tools to prove formally the claim about equivalence. 1Definition equiv (c1 c2 : com) : Prop := 2∀(st st' : state), 3(st =[ c1 ]⇒st') ↔(st =[ c2 ]⇒st'). 4 5Theorem program_equivalence (b: nat) (X Y : aexp) (Z : string) : 6b = 0 ∨b = 1 → 7equiv <{ if b = 1 then Z := X else Z := Y end }> 8<{ Z := X * b + Y * (1 - b) }>. 9Proof. 10 intros;split. 11 (* if ... →Z := ... *) 12 -intros C1; inversion C1; subst; clear C1; 13 inversion H; subst; try discriminate; 14 inversion H6; subst; 15 apply E_Asgn; simpl; 16 rewrite mul_0_r, mul_1_r; auto. 17 (* Z := ... →if ... *) 18 -intros C2; destruct Has [H|H]; subst; 19 [apply E_IfFalse|apply E_IfTrue]; auto; 20 inversion C2; subst; 21 apply E_Asgn; simpl; 22 rewrite mul_0_r, mul_1_r; auto. 23 Qed.Rocq Listing 43: A Rocq proof of program equivalence (theorem only). The full proof with the programming language syntax, semantics, and notations is about 200 LoC.39 130 3.1.5 mwp-bounds as Postconditions 3.1.5.1 Optimal mwp-bounds by form The enhanced flow calculus now provides a technique for postcondition inference. We aim to compute the optimal postconditions for each variable, if they exist. There are two unresolved concerns. First, mwp-bounds cannot be totally ordered since some forms are incomparable. Second, mwp-bounds of different form can evaluate to the same numeric polynomial. For example, the three mwp-bounds 𝑊1≡max(0,X1+X2)+0and 𝑊2≡max(X1,0)+X2 and 𝑊3≡max(X2,0)+X1are all numerically equal to X1+X2. Therefore, reasoning about optimality requires an alternative approach. To establish an ordering, we leverage two built-in features of the flow calculus. The individual coefficient are ordered 0 < 𝑚 < 𝑤 < 𝑝 < ∞. Moreover, the mwp-bounds carry semantic meaning by form. The growth of a variable value is at most linear (resp. iteration-independent, iteration-dependent) if its mwp-bound contains at most 𝑚(resp. 𝑤, 𝑝) coefficients. This gives sufficient justification for our definition of optimality. Definition 7 (Optimality).We define an order on mwp-bounds by form, by the maximal coefficient it contains: 0<𝑚-bound <𝑤-bound <𝑝-bound <∞(none). A variable’s mwp-bound is optimal if it is the least bound in this order. □ For example, among 𝑊1,𝑊2, and 𝑊3, the 𝑤-bound max(0,X1+X2)+0is optimal because it contains no 𝑝coefficients. It supplies the evidence that the variable’s value growth is eventually loop iteration independent (discussed in §3.1.5.4). The other candidates 𝑊2and 𝑊3are too weak to reach the same conclusion. Finding a single derivation that admits the optimal form is sufficient. 233 3.1.5.2 Variable postcondition search When a program is derivable, or a variable is disjoint from failure, the general procedure for deriving a variable’s optimal postcondition is as follows. 1. Run the mwp-matrix evaluation (Algorithm 4) iteratively. Construct the set 𝒮from monomials whose flow coefficient is greater than 𝑚(next 𝑤, then 𝑝). 2. Stop at the first choice vector. This solution is optimal. Since the search focuses on individual variables, we may want to ask whether multiple postconditions can occur concurrently. To determine the answer, we take the intersection of their choice vectors (Def. 8). A non-empty intersection specifies the derivations in which both postconditions hold. Related questions about postconditions can be formulated similarly, as operations on choice vectors. Definition 8 (Choice vector intersection).Letting  𝐶𝑎=(𝑎1,𝑎2,…,𝑎𝑘)and  𝐶𝑏=(𝑏1,𝑏2, …,𝑏𝑘)be choice vectors of length 𝑘, we define the intersection of  𝐶𝑎and  𝐶𝑏as  𝐶𝑎∩ 𝐶𝑏=⎧ { ⎨ { ⎩(𝑎1∩𝑏1,𝑎2∩𝑏2,…,𝑎𝑘∩𝑏𝑘), if ∄𝑖such that 𝑎𝑖∩𝑏𝑖=∅, ∅, otherwise. □ Example 25 (Successful and optimal postcondition of X3).By Ex. 22, LucidLoop is derivable by choice vector ({0,1,2},{0}). By Ex. 23, variable X3is assigned its optimal postcondition in derivations ({2},{0,1,2}). The whole-program is derivable and variable X3 is assigned its optimal postcondition in derivations defined by choices ({0,1,2},{0})∩ ({2},{0,1,2})=({2},{0}).□ 234 3.1.5.3 Program analysis for postcondition inference Postcondition inference requires adjusting the imperative language (§3.1.3.1) to a language of loops. A loop program starts with a looping command (while or loop) whose body is any command in the imperative language. Using the mwp-matrix evaluation procedure, we compute postconditions for all variables that have expressible mwp-bounds. To avoid repeated analysis, we proceed from loop nests to parent and compose mwp-matrices in a bottom-up manner. Postcondition inference of loop 𝒞is defined as follows. 1. Extract all (possibly nested) loops from the program 𝒞. 2. (bottom-up) For each loop 𝑙: (i) Run the mwp analysis to derive the mwp-matrix, 𝑙∶𝑀. (ii) Using Algorithm 4, evaluate 𝑀to determine if 𝑙is derivable. ▷If yes: mark every variable as satisfactory. ▷If no: mark the non-failing variables as satisfactory (§3.1.4.4). (iii) Evaluate satisfactory variables for optimal postconditions (§3.1.5.2). (iv) Record the postconditions of satisfactory variables. 3. Return the analysis result for 𝒞. 235 3.1.5.4 Postcondition categories as descriptors of variable value behavior A language of loops restricts the kind of computations we may encounter. The inferred postconditions can be described by the following categories. Linear. A variable’s mwp-bound is linear if its value does not change or it is a target of direct assignment (without arithmetic). Inside loops, other operations are “too strong” to retain linear behavior. In LucidLoop, variables X1,X2and X5are linear because their values never change. Iteration-independent. A variable is iteration-independent if its final value depends on a fixed number of iterations (e.g., the first or last one) or eventually reaches a fixed point. Iteration independence means that, beyond the fixed point, the variable is unaffected by an increase in loop iteration count. Thus, iteration-independence is a quasi-invariance property. In LucidLoop, if the loop iterates at least once, the final value of X3is determined by X2and X5. Iteration-dependent. Arithmetic computations involving multiple changing variables lead to iteration-dependent value growth. It may occur in bounded loops, but not otherwise. This is because a continuously increasing value may be boundable under finite iteration, but not if the loop is unbounded. In LucidLoop, changing the number of times the loop iterates changes the final value of X4respectively. This makes X4 iteration-dependent. Inconclusive. If no expressible postcondition exists, the variable is inconclusive. It characterizes cases where a variable’s value growth is outside the previous three categories. In Ex. 24, since the loop does not terminate, the value of X4grows in perpetuity. This makes the variable’s value growth inconclusive. 236 A note on numerical minimality. One variable may be assigned multiple incomparable mwp-bounds. The definition of optimality does not guarantee the selected postcondition is the numerical minimum by evaluation. For example, variable X3in LucidLoop is assigned three mwp-bounds 𝑊1≡max(X3,X2)+X1×X5and 𝑊2≡max(X3,X2+X5)and 𝑊3≡max(X3,X5)+X1×X2. For purpose of this example, assume X1>0to consider the iterative case and ignore 𝑊2. This leaves two alternatives. These can evaluate to distinct numeric values, yet both are equally optimal by definition. 3.1.5.5 Implementing postcondition inference with mwpℓ We implemented the analysis of §3.1.5.3 as an extension of the static analyzer pymwp. pymwp (Aubert, Rubiano, Rusch, & Seiller, 2023b) is an open source implementation of the flow calculus of mwp-bounds on a subset of C. pymwp takes as input a Cfile and analyzes variable value growth in each of its functions. Our implementation adds to pymwp a new loop analysis mode, mwpℓ. The loop analysis is complementary to the default function analysis mode, which we name mwp𝑓for distinction. The primary differences are that mwpℓlooks for optimal bounds by variable in a loop, and mwp𝑓finds existence of any bound for all variables in a function. Though applicable to both, the paper enhancements are implemented only in mwpℓto enable evaluation. During program analysis, the input file is mapped to the imperative language of Def. 1. Only loops that are fully expressible in the imperative language are analyzed. Analyzing program fragments is possible due to compositionality of the flow calculus. Stated differently, we can apply the analysis early, even if some program parts are missing. pymwp supports all loop constructs of C. The flow calculus treats the iteration space conservatively as an overapproximation. Keywords break and continue have no observable impact. Similarly, verification macros like assert may be present, but they do not impact the analysis. 237 When a Cloop construct is obviously bounded,8it is treated as a bounded loop in the flow calculus. Otherwise, the construct is treated as an unbounded loop. Detection of loop boundedness impacts the number of derivable variables, since a bounded loop permits iterationdependency. The current detection is based on loop form and it is still rudimentary. In the future, improving the analyzer’s handling of richer loop forms would yield more bounded variables. To use the analysis results as concrete verification assertions, two more steps are required. First, we must record the initial variable values because they are needed to express postconditions. Next, we must complete the parts that are left implicit in mwp-bounds, like constants. §3.1.9 demonstrates how we perform both steps. In general, the postconditions provide bounding expressions w.r.t. input variables, with some possible omissions. However, filling in the expression is easier than starting with no expression at all. 3.1.6 Comparing Related Techniques 3.1.6.1 Automatic inference of specification conditions Our work relates primarily to approaches that aim to unify software verification and complexity. Whereas loop invariants are used in (Nguyen, Antonopoulos, Ruef, & Hicks, 2017) to obtain complexity results, we synthesize specification conditions starting from complexity analysis. The bidirectionality suggests that further investigations that connect the two topics is warranted. Narrowing down to specifications, automatic specification inference in general is a challenging problem (Dillig, Dillig, Li, & McMillan, 2013; Yu, Wang, & Wang, 2023). It is common to break down the problem into smaller parts: preconditions, postconditions, and (inductive) invariants. Inference of postconditions is the most relevant 8For example, in for(int i=0;i<N;i++) the iterator imust not occur in the body and the body operations are arithmetic. Without nesting, it is clearly a finite loop. 238 to our analysis. Although invariant inference is studied extensively in literature (Colón, Sankaranarayanan, & Sipma, 2003; Cousot & Halbwachs, 1978; Dillig, Dillig, Li, & McMillan, 2013; Karr, 1976; Nguyen, Antonopoulos, Ruef, & Hicks, 2017; Nguyen, Kapur, Weimer, & Forrest, 2014; Ryan, Wong, Yao, Gu, & Jana, 2020; Sankaranarayanan, Sipma, & Manna, 2004; Si, Dai, Raghothaman, Naik, & Song, 2018; Yao, Ryan, Wong, Jana, & Gu, 2020; Yu, Wang, & Wang, 2023), existing works that intentionally target postconditions are rare (Molina, Ponzio, Aguirre, & Frias, 2021; Popeea & Chin, 2007). There are a few instances that infer postconditions statically. In (Popeea & Chin, 2007), show how abstract interpretation can be used to obtain a static technique for postcondition inference. Conceptually it is close to our goals, but abstract interpretation differs considerably from the flow calculus. Moreover, no implementation is available for comparison. The complexity analyzer KoAT (Giesl, Lommen, Hark, & Meyer, 2022) is a static analyzer with an open source implementation. However, it targets complexity-theoretic program properties, like time and size bounds, and is not specialized in verification. Dynamic analyzers are complementary to static techniques. They inspect program traces to infer likely invariants at the traced program points. EvoSpex (Molina, Ponzio, Aguirre, & Frias, 2021) is a dynamic postcondition analyzer. It is designed for Java methods for reasoning about postconditions in classes (accessors, mutators, heap structures, etc.); and thus distant from numerical loop analysis. The invariant detector Daikon (Ernst et al., 2007) handles many program constructs, including numerical loops. Since Daikon is compatible with our problem formulation, we discuss it in §3.1.6.2). DIG (Nguyen, Kapur, Weimer, & Forrest, 2014) is another dynamic numeric invariant generator. DIG can perform invariant inference at arbitrary program points, which makes it usable as a postcondition detector. Although it is similar to Daikon, DIG mixes static and dynamic techniques to obtain more informative results. In general, dynamic program analysis differs notably from static program analysis. Since the results are based on traces, they are necessarily incomplete. The 239 quality of inferred results is directly related to the available analysis inputs. Importantly, a dynamic analyzer requires executing the input program, which implies that the program must be runnable. The same is not necessary for our analysis that can work with program fragments. 3.1.6.2 A Comparison of Alternative Approaches Since we aim to support concrete verification tasks, we must compare our analysis to available implementations that can address the same problem. In this section, we compare9 mwpℓto three mature10 analyzers: KoAT, Duet, and Daikon. These analyzers are designed for complexity analysis, verification, and invariant inference, resp. Each analyzer analyzes different program scopes (cf. Table 19 and §3.1.10.3) and has a different specification of output format. Therefore, a statistical comparison is insufficient for useful comparison. A better way is to present canonical cases that the analyzers handle differently. As comparison workloads we consider the loops of Fig. 32. They are instances from the benchmarks used in §3.1.7. To give a preview of our findings—which we summarize in Table 19—the alternative analyzers are orthogonal. The comparison shows mwpℓis useful in cases the other tools ignore, and vice versa. 9Refer to §3.1.10 for the technical details of this comparison. 10Each analyzer is developmentally stable with 10+ years of history. 240 for(int i=0;i<X1;i++) { X3=X2*X2; X3=X3+X5; X4=X4+X5; } Listing 62: LucidLoop while(nondet()) { X1=X2+X2; X2=X3+X3; X4=X5+X5; } Listing 63: Function condition assume(y==0); while(y<1000) { x=x+y; y=y+1; } Listing 64: Finite iteration Figure 32: Loop cases for analyzer comparison. The loop in 62 is known to terminate and its guard variable X1does not occur in the body. In 63, the loop iteration space and termination are unknown since they are controlled by a nondeterministic function. The loop in 64 has a fixed iteration space, but the postcondition of xis difficult to infer. Assuming y=0, the precise formula is x' =x+(y' ×y' −y')÷2where y' is iteration count. Inference with mwpℓ.The results of mwpℓgive a baseline for comparison. • Listing 62: As explained in §3.1.1.1. • Listing 63: X3and X5are linear. The other are X2'≤max(X2,X3), X4'≤max(X4,X5), and X1'≤max(X1,X2+X3). • Listing 64: The program converts to a bounded loop. The constants 1and 1000 are lifted to inputs c1and c2, resp. The postconditions are x' ≤x+c2×(c1+y)and y' ≤y+(c1×c2). Complexity analyzer KoAT. KoAT (KoAT2 Developers, 2024) is a part of the automated termination and complexity prover AProVE (Giesl et al., 2016). KoAT infers complexity bounds: time, cost, size bounds, etc. The bound most relevant to our problem is the size bound, which indicate how large the absolute value of an integer variable may become (Lommen & Giesl, 2023). Applying KoAT on C programs requires compiling the C code (through LLVM bitcode) into an integer program. The transformed program is then analyzed by KoAT (Giesl, Lommen, Hark, & Meyer, 2022). The translation step renames the program 241 variables. Variables that do not contribute to the complexity result are discarded during pre-processing. This treatment has the following effects: (i) KoAT can distinguish between loops that differ only on iteration counts, and (ii) size bounds are inferred only for variables that impact the loop iteration. The latter is the complement of the flow calculus, where the iterator of a bounded loop is not allowed to occur in the body. • Listing 62: We obtain X1'∶2⋅X1and i' ∶X1+2; and X2–X5are discarded. • Listing 63: No size bounds are generated for variables X1–X5. • Listing 64: Variable yhas precise size bound y∶1000. Variable xis discarded. Duet – the analyzer of unbounded concurrency. Duet is a static verifier for concurrent programs whose thread count cannot be statically bounded (Duet Developers, 2024). We include it in this comparison because it contains analysis techniques that relate to our problem. In particular, the implementation of transition ideals (Cyphert & Kincaid, 2024) computes loop summaries that produce over-approximations of a formula that describes the loop body. The summaries can capture non-linear invariants and generalize over arbitrary control flow. The theory of transition ideals is monotone. In other words, a program with more precise specifications yields a more informative loop summary. Then, Duet aims to prove program correctness using the invariants generated from transition ideals. • Listings 62 – 64: In absence of assertions, Duet produces a single response, no errors and no unsafe assertions. This response is not meaningful for our use case. After adding postconditions (assertions) manually, Duet verifies them successfully. For example, if we add to Listing 64 the assertions x' =x+(y' × y' −y')÷2and y' =1000, Duet verifies the program with 0errors, 2safe assertions. When assertions are not available, mwpℓcould assist Duet toward obtaining the initial assertions. 242 3.1.9 Appendix A: Application to Program Verification The following example shows how to complete an implementation with specification conditions, in the verification-aware Dafny programming language. The postconditions are those inferred by our analysis. 0method LucidLoop(X1∶nat, X2∶nat, X3∶nat, X4∶nat, X5∶nat){ 1 2// for bookkeeping -- record initial values 3var X1', X2', X3', X4', X5' ≔X1, X2, X3, X4, X5; 4 5for i ≔0 to X1' 6// invariants (omitted) 7{ 8X3' ≔X2' * X2' + X5'; 9X4' ≔X4' + X5'; 10 } 11 12 // postconditions 13 assert X1'≤X1; // linear 14 assert X2'≤X2; // linear 15 assert X5'≤X5; // linear 16 assert X3'≤Max(X3, X2*X2+X5); // weak polynomial 17 assert X4'≤X4+X1*X5; // polynomial 18 }Dafny Listing 65: LucidLoop verified in Dafny. Concrete program verification requires two additional steps. First, recording the initial variable values (L4). This is simply a matter of creating copies of variables. Recording the 249 initial values enables referring to them in the postconditions. Second, we add the constants (L14–16) omitted in the postconditions of our analysis. Although this step requires manual effort, is it significantly easier to “fill in” the constants, than to infer full assertion clauses. Maintaining human oversight in this step has an additional benefit. It forces to check that the assertions are sensible. If the implementation has a bug—e.g., variable grows exponentially when it should not—the bug becomes detectable during this step. A fully automatic technique would not alert to the issue. After adding invariants, the Dafny verifier immediately constructs a proof, which confirms that the assertions always hold. Generating suitable inductive loop invariants is a challenge for the related works that specialize in invariant inference. 3.1.10 Appendix B: Technical Details of Analyzer Comparison 3.1.10.1 Executing the analyzers We analyzed the programs in Listings 71–73 as follows. mwpℓ.We run pymwp v0.6.0 in the loop analysis mode. pymwp [program].c --mode L --strict cmd Listing 66: Running pymwp in loop analysis mode. 250 KoAT. The KoAT web interface is sufficient to confirm our findings. We applied the following options: ✓control-flow refinement ✓size bounds ✓unsolvable loops, and default timeout. The web interface address is: https://aprove.informatik.rwth-aachen.de/interface/v-koat/c Duet. We ran Duet from source, git revision 1d36b05, with following options. The compositional recurrence analysis generates invariants for sequential programs. Transition ideals is implemented as linear and quadratic simulation modes. duet.exe [program].c -cra # compositional recurrence analysis -cra-refine # enable loop refinement -monotone # disable non-monotone analysis features -[theory] # lirr-usp or lirr-sp-quad cmd Listing 67: Program analysis with Duet. Daikon. Daikon requires multiple version of a program, then compiling and tracing them with Kvasir. The *means we trace multiple versions of input. Supply options to Kvasir before the program name argument. 251 kvasir-dtrace --dtrace-file=[program].dtrace # trace destination --decls-file=[program].decls # declarations file [program]_*.o # compiled program cmd Listing 68: Creating a trace with Daikon. After tracing, we run Daikon with following options to infer postconditions. java -cp $DAIKONDIR/daikon.jar daikon.Daikon --conf_limit=.50 # confidence -o [program].inv.gz # output [program]_*.dtrace # path to traces [program].decls # path to declarations cmd Listing 69: Infer invariants using Daikon. After inference, the invariants can be printed to a suitable display format. java -cp $DAIKONDIR/daikon.jar daikon.PrintInvariants --wrap_xml --output_num_samples # format options [program].inv.gz # source [program].txt # output path cmd Listing 70: Displaying invariants inferred by Daikon. 252 3.1.10.2 Comparison programs int loop(int X1,int X2,int X3, int X4,int X5) { for(int i=0; i < X1; i++) { X3= X2* X2; X3= X3+ X5; X4= X4+ X5; } return X3; }C Listing 71: mwp/example 3.4. int loop(int X1,int X2,int X3, int X4,int X5) { while(__VERIFIER_nondet_int()){ X1= X2+ X2; X2= X3+ X3; X4= X5+ X5; } return X4; }C Listing 72: mwp/not infinite #4. int loop(int x, int y) { y=0; while(y<1000) { x = x + y; y=y+1; } return x; }C Listing 73: Linear #02. These are programs of Fig. 32 expanded with headers and return statements. For Duet analysis, loop must be renamed to main. Having a main function raises an error with 253 KoAT. Daikon expects adding a separate main method with calls to loop. In Listing 73, assume is unsupported and should be omitted before analyzing it with KoAT. 3.1.10.3 Analyzer scopes int main(int X, int Y, int Z) { for(int i=0; i<Y; i++) X=X+Z; assert(...); return X; } KoAT mwpℓ Duet Daikon Figure 33: Postcondition analysis scopes. The analyzers focus on complementary program regions identified by the different colors. KoAT tracks variables that control loop iteration. mwpℓ analyzes variables inside the loop body. Duet infers loop summaries based on available assertions. Daikon infers likely invariants of the return variable and abstracts function internals. 3.1.11 Appendix C: Details of Experimental Evaluation The complexity suite is the “Complexity C Integer” suite from the Termination Problem Database version 11.3 (TPDB maintainers, 2022), This suite is used in the annual Termination and Complexity Competition. The linear suite (Si, Dai, Raghothaman, Naik, & Song, 2018) contains inference problems for linear loop invariants. The problems are pre-annotated with assertions (these have no impact on our analysis). We excluded 9 benchmarks that are known to be invalid (Ryan, Wong, Yao, Gu, & Jana, 2020, Appendix G) as they violate the specified assertions. We also unified benchmarks that have the same precondition and loop, as 254 Suite Linear mwp Complexity Non-linear Total Benchmarks 49 30 504 37 620 Lines of code 652 (13.31) 270 (9.00) 6,066 (12.04) 710 (19.19) 7,698 Loops 49 (1.00) 30 (1.00) 740 (1.47) 48 (1.30) 867 Variables – loop 117 (2.39) 105 (3.50) 1,921 (3.81) 208 (5.62) 2,351 – functions 131 (2.67) 105 (3.50) 1,519 (3.01) 208 (5.62) 1,963 Table 23: Benchmark suite characteristics by count and (mean). they are identical for the purpose of postcondition inference, ending with 49 benchmarks in total. The nonlinear suite (Nguyen, Antonopoulos, Ruef, & Hicks, 2017) (also referred to as NLA-suite in literature) is an extended formulation of the suite, with the additional problems coming from (Yu, Wang, & Wang, 2023). The mwp suite (Aubert, Rubiano, Rusch, & Seiller, 2023b) is designed specifically to be challenging for the flow calculus of mwp-bounds, with complex data flows and arithmetic operations. To obtain strictly comparable results between mwpℓand mwp𝑓, as they scope variables differently, we exclude nested loops and loopless benchmarks. The statistics of the suites are summarized in Table 23. A single benchmark can contain multiple functions, loops, and sequential and/or nested loops. Due to differences in the targeted program scopes between mwpℓand mwp𝑓, the variable counts are specified by scope. Loop-scoped variables include loop guards and variables in the loop body. Functionscoped variables contain all parameters and variables in the function body. We modified the benchmarks by expanding n-ary expressions to binary form to match the input language 255 of pymwp. Since the boundedness check is still rudimentary, some loop conditions were rewritten in detectable form. A more robust approach would use a specialized compiler. 256 3.2 A Logic for Anytime Non-Interference ȷImplicit computational complexity & security Clément Aubert and Neea Rusch Research paper draft. An earlier version of this work appeared at the 19th workshop on Programming Languages and Analysis for Security (PLAS) 2024. 257 Abstract Non-interference is an information flow policy for guaranteeing confidentiality, i.e., that effects of sensitive data are not exposed to lower-level users, even indirectly. When phrased in terms of programming languages, non-interference is studied by attaching security classes to variables, then analyzing the classes to determine if a violation, or a data “leak”, can occur. Security type systems are common controls for analyzing and enforcing non-interference. Unfortunately, they require inference algorithms, program-level security specifications, nonstandard compilers, and are generally too restrictive or complex for practical implementation. In this paper, we present a program logic ⊤∗ NI that guarantees the semantic security property of anytime non-interference. By anytime, we mean a malicious actor with lowlevel access cannot infer anything about higher-level values at any point of the program execution. The logic links non-interference violations precisely to the faulty commands and violations cannot be erased by program composition. We draw rich inspiration from complexity-theoretic flow calculi, but obtaining a logic for security analysis required significant adjustments. Finally, we share a prototype to demonstrate ⊤∗ NI can be implemented as an automatic, annotation-free, static security analyzer to obtain confidentiality guarantees in practice. 3.2.1 Introduction Verifying that data is handled securely during computation is challenging because it requires information beyond the program syntax. For example, consider a hash function that computes a checksum of its input. Assume there exists a malicious actor who can observe outputs of the hash function. If all inputs are public data, we can guarantee the function does not expose secrets to the actor. However, if we change the inputs to secret data, like social security numbers, we no longer have the same guarantee for the same function. The 258 3.2.3 The Non-interference Logic 3.2.3.1 A Simple Imperative While Language We use a simple imperative while language, with semantics similar to C. The grammar is given in Fig. 34. The language supports arrays and we let for and do...while loops be represented using while loops. How function calls can be added is discussed in §3.2.5. The language subsumes (up to letvar construct) the “core block-structured language” (Volpano, Irvine, & Smith, 1996), and it maps easily to the core fragment of C,Java, and other imperative programming languages. var ≔i|⋯|t|⋯|x1|⋯|var[exp](Variable) exp ≔var |val |op(exp,…,exp)(Expression) com ≔var =exp |skip |if exp then com else com |while exp do com |com;com (Command) Figure 34: A simple imperative while language A variable x,y,z,…represents either an undetermined “primitive” data type, e.g., not a reference variable, or an array, whose indices are given by an expression. We reserve tfor arrays. An expression is either a variable, a value (e.g., integer literal) or the application to expressions of some operator op, which can be e.g., relational (==,<, etc.) or arithmetic (+, -, etc.). We let e(resp. C) range over expressions (resp. commands). We also use compound assignment operators and write e.g., x++ for x+=1. We assume commands to be correct, e.g., with operators correctly applied to expressions, no out-of-bounds errors, etc. A program C is a sequence of commands, each command being either an assignment, a skip, a branching, 265 Command COut(C)In(C)Occ(C)= Out(C)∪In(C) x = e x Occ(e)x∪Occ(e) t[e1] = e2tOcc(e1)∪Occ(e2)t ∪Occ(e1)∪Occ(e2) skip ∅∅∅ if e then C1 else C2 Out(C1)∪Out(C2)Occ(e)∪In(C1)∪ In(C2) Occ(e)∪Occ(C1)∪ Occ(C2) while e do C Out(C)Occ(e)∪In(C)Occ(e)∪Occ(C) C1;C2Out(C1)∪Out(C2)In(C1)∪In(C2)Occ(C1)∪Occ(C2) Table 24: Definition of Out, In and Occ for commands. a while loop or the composition of two commands. A program C′is a sub-program of C, denoted C′⊆C, if C′occurs verbatim in C. We also define the following sets of variables. Definition 10 (Occ, Out and In).We define the variables occurring in an expression eby: Occ(x)=xOcc(op(e1,…,e𝑛))=∪𝑛 𝑖=1Occ(e𝑖)Occ(t[e])=t∪Occ(e)Occ(val)=∅ The set Occ(C)(resp. Out(C),In(C)) of variables occurring in (resp. modified by, used by) a program Cis defined in Table 24. We let |Occ(C)|be the cardinal of Occ(C).□ 3.2.3.2 Security-Flow Matrices for Non-interference Violation The ⊤∗ NI logic relies fundamentally on its ability to analyze data-flow dependencies between variables occurring in commands. In this section, we define the principles of this depen266 dency analysis, founded on the theory of security-flow matrices, and how it maps to the presented language. This dependency analysis is reminiscent of the one we developed to distribute loops (Aubert, Rubiano, Rusch, & Seiller, 2023e). We assume familiarity with monoids and matrices addition. A security-flow matrix 𝕄(C)for a command Cis a hollow matrix (i.e., a matrix with only ⋅ on the diagonal11) over a monoid with an implicit choice of a denumeration of Occ(C)12 Definition 11 (Security monoid).The security monoid is ({⋅,},max), with ⋅<.□ This monoid is isomorphic to the two-element Boolean algebra with only the disjunction, with representing a possible (non-interference) violation that cannot be erased. Definition 12 (Security-flow matrix).C, its security-flow matrix 𝕄(C)is a |Occ(C)|× |Occ(C)|matrix over the security monoid, whose construction is the object of §3.2.3.3. For x,y∈Occ(C), we write 𝕄(C)(x,y)for the coefficient in 𝕄(C)at the row corresponding to the in-variable xand column corresponding to the out-variable y.□ Definition 13 (Violation).Given C, its security-flow matrix 𝕄(C)and a class assignment ℓ, Chas a violation if there exists xand ysuch that 𝕄(C)(x,y)=and either ℓ(y)<ℓ(x)or ℓ(y)⊥ℓ(x): ⎛ ⎜ ⎜ ⎜ ⎝ …y… ⋮ ⋱ ... x ⋮...⋱⎞ ⎟ ⎟ ⎟ ⎠⟹Chas a violation if ℓ(y)<ℓ(x)or ℓ(y)⊥ℓ(x). 11This choice is clarified after Def. 13. 12We will use the order in which the variables occur in the program as their implicit order. 267 □ Since ℓ(x)<ℓ(x)and ℓ(x)⊥ℓ(x)are always false, there is no point keeping track of the values on the diagonal: this is why hollow matrices are enough. This is also confirmed by the intuition: it does not make sense to track data “leaking” from a variable to itself. How a security-flow matrix is constructed by induction over the command is explained in §3.2.3.3. To avoid resizing matrices whenever additional variables are considered, we identify 𝕄(C)with its embedding in any larger matrix, i.e., we abusively call the securityflow matrix of Cany matrix containing 𝕄(C)(up to rows swapping and columns swapping) and containing ⋅otherwise, implicitly viewing the additional rows and columns as variables not occurring in C. Visually, this means that the following matrices are all viewed as 𝕄(C) with Occ(C)={x,y}and 𝕄(C)(x,y)=: (x y x⋅ y⋅ ⋅)⎛ ⎜ ⎜ ⎝ y x z y⋅ ⋅ ⋅ x⋅ ⋅ z⋅ ⋅ ⋅⎞ ⎟ ⎟ ⎠⎛ ⎜ ⎜ ⎝ w x y w⋅ ⋅ ⋅ x⋅ ⋅  y⋅ ⋅ ⋅⎞ ⎟ ⎟ ⎠ Continuing this example and using our compact presentation of information flow policy and class assignment as single Hasse diagram, Cwould have a violation with the level assignments ℓ(y) ℓ(x)and 𝑐1 ℓ(y) ℓ(x) 𝑐2, but would be free of violation with ℓ(x)=ℓ(y)or ℓ(y) ℓ(x). 3.2.3.3 Constructing Security-Flow Matrices The security-flow matrix of a command is constructed by induction, using the security monoid. §3.2.9 gathers additional examples with longer discussion. 268 COut(C), In(C) 𝕄(C)Chas violation(s) if … w = 3Out(C)={w} In(C)=∅ (w w⋅)(Impossible) y = x Out(C)={y} In(C)={x}(y x y⋅ ⋅ x⋅)ℓ(y)<ℓ(x)or ℓ(y)⊥ℓ(x). w = t[x + 1]Out(C)={w} In(C)={t,x}⎛ ⎜ ⎜ ⎝ w t x w⋅ ⋅ ⋅ t⋅ ⋅ x⋅ ⋅⎞ ⎟ ⎟ ⎠ ℓ(w)<ℓ(t),ℓ(w)⊥ℓ(t), ℓ(w)<ℓ(x)or ℓ(w)⊥ℓ(x). t[i] = u + j Out(C)={t} In(C)={i,u,j}⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ t i u j t⋅ ⋅ ⋅ ⋅ i⋅ ⋅ ⋅ u⋅ ⋅ ⋅ j⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ℓ(t)<ℓ(i),ℓ(t)⊥ℓ(i), ℓ(t)<ℓ(u),ℓ(t)⊥ℓ(u), ℓ(t)<ℓ(j)or ℓ(t)⊥ℓ(j). Table 25: Statement Examples, Sets, Representations of their Possible Violation(s). 3.2.3.3.1 Base Cases: Assignment and Skip. The security-flow matrix for an assignment Csimply tracks flows from In(C)to Out(C): Definition 14 (Assignment).Given an assignment C, we define 𝕄(C)by: 𝕄(C)(x,y)=⎧ { ⎨ { ⎩ if x∈In(C),y∈Out(C)and x≠y ⋅otherwise □ We illustrate in Table 25 some basic cases: we consider an array a single entity, and that changing one value in it means being able to access it completely. More precisely, t[i] on the left-hand side of an assignment is a violation if ℓ(t)>ℓ(i)(resp. ℓ(t)⊥ℓ(i)). Indeed, it 269 implies that a lower-class (resp. orthogonal-class) variable (i) can decide where to write in a higher-class (resp. orthogonal-class) variable (t). However, t[i] as an expression (e.g., on the right-hand side of an assignment or in a condition, as discussed in paragraph 3.2.3.3.3) is acceptable as long as the variable(s) storing the result of this calculation or dependent on that condition’s truth value have class higher or equal to tand iclasses. Definition 15 (Skip).We let 𝕄(skip)be the matrix with 0rows and columns. □ Identifying 𝕄(skip)with its embeddings, it is the empty matrix of any size. 3.2.3.3.2 Composition as a Commutative Operation. The security-flow matrix for a composition of commands is an abstraction that allows manipulating a sequence of commands as one command with its own matrix. Definition 16 (Composition).We let 𝕄(C1;⋯;C𝑛)be 𝕄(C1)+⋯+𝕄(C𝑛).□ C1C2C1;C2 ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ w x y z w⋅ ⋅ ⋅ ⋅ x⋅ ⋅ ⋅ y⋅ ⋅ ⋅  z⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ +⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ w x y z w⋅ ⋅ ⋅ ⋅ x⋅ ⋅ ⋅ y⋅⋅ z⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ =⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ w x y z w⋅ ⋅ ⋅ ⋅ x⋅ ⋅ ⋅ y⋅⋅ z⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ w = w + x; z=y+2 x=y*2; z = 0 Figure 35: Security-Flow Matrix of compositions. 270 The composition of commands C1and C2—themselves already the result of compositions of assignments involving disjoint variables—is illustrated in Fig. 35. Two important observations: 1. Some existing approaches might consider C1;C2as free of violation even if ℓ(z)< ℓ(y), since z=0will wipe out the content of zand “cancel” the violation introduced by z = y. The intuition is that an attacker observing the output (or even all the final values) cannot deduce anything about z’s value (and, transitively, about the value of the higher-class y) once the computation is over. Our “once a violation, always a violation” approach ignores the fact that “ultimately”, this violation may be hidden– the anytime non-interference guarantee is discussed in §3.2.4. 2. Interestingly, 𝕄(C1;C2) = 𝕄(C2;C1)since composition is interpreted as a sum of matrices over our commutative security monoid. While previous flow-based approaches (Aubert, Rubiano, Rusch, & Seiller, 2022a; Aubert, Rubiano, Rusch, & Seiller, 2023e; Jones & Kristiansen, 2009) require a semi-ring because composition was handled via product of matrices, the current set-up simplifies the machinery precisely to keep track of past violations. 3.2.3.3.3 A Correction for Implicit Flows. To account for implicit flows, branchings and loops require a correction. The main idea is that interpreting if e then C1else C2 (resp. while e do C) require to record that all the variables modified in C1and C2(resp. in C) depend on the variables occurring in e(as opposed to the assignment considering the variables used by C). Definition 17 (Correction).The correction Cr(e)Cof an expression eon a program Cis Cr(e)C(x,y)=⎧ { ⎨ { ⎩ if x∈Occ(e),y∈Out(C)and x≠y ⋅otherwise 271 □ Intuitively, the correction states that if the variable yis modified in the body of either branch of the branching or in the body of the loop and xoccurs in the expression, then there is a violation if ℓ(y)<ℓ(x)or ℓ(y)⊥ℓ(x). As an example, let us use Fig. 35 to construct Cr(w x)C1;C2, e.g., w > x’s correction for C1;C2. Variables wand x, through the expression w > x, control the values of w,xand z since C1and C2set those values, and their execution depend on it, giving: ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ w x y z w⋅⋅ x⋅ ⋅  y⋅ ⋅ ⋅ ⋅ z⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠. Observe also that in Cr(t[i] != x)Cthe variables t,iand xwould be marked as controlling the variables occurring in Out(C). However, no constraint would be imposed between the classes of t,iand x, since they would all be required to flow into classes that are higher or equal to theirs. 3.2.3.3.4 Conditionals and Loops. Following our previous observation, branchings and loops are interpreted similarly. Definition 18 (Branching).We let 𝕄(if e then C1else C2)be 𝕄(C1;C2)+Cr(e)C1;C2. □ 272 Adding Cr(w > x)C1;C2to 𝕄(C1)+𝕄(C2)from Fig. 35, we obtain: 𝕄 ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ if (w > x) then w = w + x; z = y + 2 else x = y * 2; z = 0 ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ =⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ w x y z w⋅⋅ x⋅ ⋅  y⋅⋅ z⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ . Observe that there is a violation if ℓ(w)<ℓ(x)or ℓ(w)⊥ℓ(x)from the statement w=w+x, and that there is a violation if ℓ(x)<ℓ(w)or ℓ(x)⊥ℓ(w). The latter comes from the fact that the value of wwill decide if x=y*2will execute through the expression. To be free of violations, such a program must be given a class assignment satisfying ℓ(w)=ℓ(x)and the other constraints recorded in the matrix. Definition 19 (Loop).We let 𝕄(while e do C)be 𝕄(C)+Cr(e)C.□ 𝕄 ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ while(t[i]!=j){ s1[i] = j*j; s2[i] = 1/j; i++ } ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ =⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ t i j s1s2 t⋅⋅  i⋅ ⋅ ⋅   j⋅⋅  s1⋅ ⋅ ⋅ ⋅ ⋅ s2⋅ ⋅ ⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ Since s1and s2do not control any other variable, their rows are all ⋅s. On the other hand, t, iand jcontrol the values of s1,s2and i, since they determine how many times the body will execute. 273 3.2.4 Capturing Anytime Non-Interference In the seminal work of Volpano et al. (Volpano, Irvine, & Smith, 1996, pg. 173), “[s]oundness [wa]s formulated as a kind of noninterference property. […I]f a variable 𝑣has security [class 𝑐], then one can change the initial values of any variables whose security levels are not dominated by [𝑐], execute the program, and the final value of 𝑣will be the same, provided the program terminates successfully.” (our emphasis). Anytime non-interference, defined below and captured by ⊤∗ NI, inspects the values while the program is being executed. It allows us to 1. avoid making assumptions of program termination, or avoid waiting for termination, and 2. model attackers who are capable of observing updates to variables at class 𝑐or lower. First, we need to define a notion of timed execution, which captures the idea that an external observer can see updates on variables below a particular security class in “real time”. Definition 20 (Timed command execution).Given 1. a program Cwith variables x1,…,x𝑛, 2. a class assignment ℓ∶Occ(C)→SC, 3. a security class c∈SC, 4. a time (counter) 𝑡∈ℕ, 5. and a value list 𝑣=𝑣1,…,𝑣𝑛, we write •C[ 𝑣]0for the program Cwhere the variable x𝑖was assigned 𝑣𝑖,13 for 1⩽𝑖⩽𝑛, 13Since arrays have a fixed size, we assume, for simplicity, that a variable x𝑖representing an array of size 𝑠is given a value 𝑣𝑖=𝑣1 𝑖,…,𝑣𝑠 𝑖. 274 C𝕄e(C)=⋯ Out(C), In(C) 𝕄e(C) g(x + y) 𝕄(gout x,y= x + y) +𝕄(skip) Out(C)={gout x,y} In(C)={x,y}⎛ ⎜ ⎜ ⎝ x y gout x,y x⋅ ⋅  y⋅ ⋅  gin x,y⋅ ⋅ ⋅ ⎞ ⎟ ⎟ ⎠ x = f(y) 𝕄(fout y= y) +𝕄(x = f(y)) Out(C)={x,fout y} In(C)={y,fin y}⎛ ⎜ ⎜ ⎝ x y fout y x⋅ ⋅ ⋅ y⋅ ⋅  fin y⋅ ⋅ ⎞ ⎟ ⎟ ⎠ if (g()==1) then x = 0 else skip Cr(g()==1)x=0;skip +𝕄(x = 0) +𝕄(gout ∅=)+𝕄(skip) Out(C)={x,gout ∅} In(C)=∅ (x gout ∅ x⋅ ⋅ gin ∅  ) Table 28: Statement Examples, Interpretation and Sets – Involving Effects. (henceforth simply denoted f(  e)) and in  eto get a more complete picture: Occ(f(  e))=fin  eOcc( e)=⎧ { { ⎨ { { ⎩ Occ(e1)∪⋯∪Occ(e𝑛)if 𝑛>0 fin ∅otherwise with the “otherwise” case above handling functions with 0 parameters. We then let 𝕄(f(  e))=𝕄(skip) 𝕄e(C)=∑ f(  e)⊆Occ(C) 𝕄(fout  e= e)+𝕄(C) and study 𝕄e(C)moving forward, where the above definition interprets all function calls as assignments and then interpret the rest of the program as before, skipping the commands calling a function without using their return value. Table 28 gathers examples of programs involving effectful functions. The last example follows our definitions, but may be hard to unpack: the critical point is to see that gin ∅controlling the values of xand gout ∅reflects the fact that g“on its own” (i.e., without any input) will decide of its output and hence if x = 0 will execute. 281 This interpretation entails the following two principles: • An effectful function is completely transparent: the first example of Table 28 requires ℓ(gout x,y)⩾max(ℓ(y),ℓ(x)), e.g., as if gis revealing all the data it is processing. • A function can nevertheless have ℓ(fin  e)be less than or orthogonal to the level of its arguments. This means that a function can have a return value that is independent of its arguments, e.g., a success or failure code in displaying the arguments at the screen. Those principles can be both desirable and are not incompatible. Indeed, a program success = print(secret); if (success==0) then x++ else x-- with the class assignment ℓ(success)=ℓ(printin secret) ℓ(x) ℓ(secret)=ℓ(printout secret) should be considered as anytime non-interfering: a user having access to secret’s class can see its value be displayed on the screen, but an attacker having access to at most x’s class cannot infer secret’s value, despite being able to access the return value of print(↲ secret)—which is constantly set to the lowest class available. Three challenges remain: • The intuitive reading of our security-flow matrices is lost. For example, since y∉ In(x = f(y))),𝕄e(x = f(y))(x,y) ≠ , and yis not recorded as impacting the value of x. This design choice is a feature, as it does not “force” yto control x’s value when processed through f: this allows finer constraints on the level of fin y. 282 • It rigidly assumes that functions with side effects will reveal all their data at all times. This conservative approach is also a feature, but could be tuned by refining how constraints for fout  eclass assignments are recorded. • Developing a definition of anytime non-interference for programs with side effects (Def. 22) will requires to develop a notion of external observer and of contextual equivalences, to correctly account for side effects and multiple communication channels. We believe that those issues can be addressed by developing a richer theory that incorporates external knowledge on functions, but reserve it for future work. 3.2.6 Practical Applications and Comparison 3.2.6.1 Implementing the Anytime Non-interference Logic We have created a prototype static analyzer TYNI that implements the ⊤∗ NI logic. The way matrices are composed in ⊤∗ NI is a key feature in making the analysis straightforward and efficient in practice. Because composition order is irrelevant (Ex. 27), it suffices to represent matrices as hash maps where composition is a union of maps. The TYNI analyzer accepts as input a program file written in Java. It first translates the program into a parse tree (without optimizations), then analyzes the tree based on the rules of ⊤∗ NI. The analysis is recursive over the methods of a Java class. Obtaining a sound result requires a Java method fully expressible in the ⊤∗ NI grammar (Fig. 34). Commands that are not covered are highlighted by TYNI and the analyzer outputs a partial result. This handling assists the continued development of ⊤∗ NI. Currently, it already handles all the examples from §3.2.9. 283 The outlined engineering choices have multiple advantages. Java is frequently used to implement taint analyzers, an instance of non-interference fixed to two security classes. TYNI is thus prepared for a similar use case. Since Java compiles into bytecode, a kind of intermediate stack language, it enables program analysis at multiple language representations. Although compiler optimizations could reduce the rate of false alarms, e.g., by eliminating dead-code, it would artificially inflate the analysis precision and thus we prefer our strategy. Currently, TYNI produces security-flow matrices for input programs. The security flow matrices serve as basis for the extended applications, including the directions presented next. Preservation of anytime non-interference. The ⊤∗ NI logic does not require much language structure; in particular, it assumes no language-specific syntactic features. It is possible to map its grammar to numerous language representations, including intermediate representations and bytecode. Comparing security-flow matrices of the same program at different representations enables analyzing preservation of security properties and detecting compilation issues. Security class inference. When security classes of variables are known partially, it is possible to infer them for all variables. The inference requires a security-flow matrix, an information flow policy, and the known class assignments. The inference is then framed as a satisfiability problem. If a satisfactory assignment exists, it provides the security classes for all variables. This application is similar to type inference, but requires no program as input. Further, the same security-flow matrix can be easily evaluated against different information flow policies. Taint analysis. Taint analysis detects information flow issues between a high source and a low sink. Aside a program, the sources and sinks are necessary, and analyzers commonly assume them as inputs. The analyzers then compete on precision along various axes: path-coverage, syntax-coverage, context-sensitivity, false alarm rate, 284 etc. Taint analysis can be formulated with security-flow matrices by analyzing source to sink connectivity. 3.2.6.2 Circumventing Termination-insensitivity via Distribution Several real-world programs are non-terminating by design: web servers, embedded systems, and cyber-physical systems are among the examples. While the programs can terminate, the termination events are infrequent and uncharacteristic of standard behavior. Security analyses that can handle absence of termination are necessary to support such programs. Anytime non-interference is termination-insensitive and compatible with the study of nonterminating programs. However, termination-insensitivity is too weak to guard against untrusted code, e.g., execution of the eval command. To offer an alleviation strategy, we present an approach to distribute security-sensitive computation. This way, computations that require elevated security checks are handled separately from trusted code. The idea is to pair ⊤∗ NI with a distribution analysis (Aubert, Rubiano, Rusch, & Seiller, 2023e) that detects disjoint program fragments. That program fragments are disjoint means there exists no exchange of variable data between program fragments. The judgement of disjointness is derived via a sound data flow analysis that guarantees the property. It is then permissible to execute the program fragments in separate execution contexts. Although the distribution analysis naturally fits parallel computations, it is not restricted to this use case. We conjecture it offers broader utility here, to ensure program security. To combine the two analysis, we first analyze a program with ⊤∗ NI to identify its information flow constraints. Then, we use the distribution analysis to identify the program’s distribution potential. Merging the results, the disjoint program fragments are assigned appropriate security classes. The fragments are then allocated to different execution contexts, where 285 each fragment can have a different security class designation. This way, a program must not adhere to a monolithic security strategy, but can have a finer-grained strategy based on its content. Due to paper scope, we reserve a detailed treatment for an extended version. 3.2.6.3 Overview of Alternative and Related Approaches In language-based security, non-interference is commonly achieved through security type systems. Type theoretic non-interference provides strong end-to-end confidentiality guarantees in a static and scalable way. Initiating from the seminal work of Volpano et al. (Volpano, Irvine, & Smith, 1996), security type systems have been extended to consider noninterference under numerous paradigms, including concurrency (Derakhshan, Balzer, & Yao, 2024; Frumin, Krebbers, & Birkedal, 2021; Volpano & Smith, 1998), formal reasoning (Frumin, Krebbers, & Birkedal, 2021; Nelson, Bornholt, Krishnamurthy, Torlak, & Wang, 2020), secure compilation (Barthe, Basu, & Rezk, 2004), etc. A major challenge among the security type systems is declassification, a kind of security downgrading operation (Cecchetti, Myers, & Arden, 2017). A downgrading mechanisms permits elevating the security judgement around control-flow constructs then lowering it afterward. In other words, information is allowed to flow contrary to the policy (Cecchetti, Myers, & Arden, 2017). The mechanism is necessary to increase the expressive power of security type systems. However, downgrading is generally not safe (Derakhshan, Balzer, & Yao, 2024) and eliminates the strong compositional guarantees of non-interference (Cecchetti, Myers, & Arden, 2017). In practice, security type systems are challenging to use because they modify the programming language. A program must be annotated with security types and compiled with non-standard tools that can enforce the types (Lamba, Taylor, Beardsley, Bambeck, Bond, & Lin, 2024). There is also a stark contrast in expressiveness of theoretical and practical systems. E.g., (Huang, Dong, & Milanova, 2014) categorically excludes implicit flows. 286 The Dependency Core Calculus (DCC) (Abadi, Banerjee, Heintze, & Riecke, 1999) is conceptually related to ⊤∗ NI. The DCC is an extension of lambda-calculus, framed around the notion of data dependence, of which non-interference is an instance. Though similarly rooted in dependency analysis ⊤∗ NI originates from works of implicit computational complexity (ICC). It is a refinement of (Aubert, Rubiano, Rusch, & Seiller, 2023e; Moyen, Rubiano, & Seiller, 2017a), but ⊤∗ NI required significant adjustment, particularly around matrix composition and functions. Implicit computational complexity studies machine-free characterizations of complexity classes by introducing restrictions in programming languages that in turn guarantee semantic properties (Dal Lago, 2011). A critical idea is that ICC techniques can benefit from, and offer support in, other analytic domains. The use of ICC techniques is such extended ways is an emerging research topic. Previously, a non-interference type system provided a foundation for a series of complexity-theoretic results (Hainry & Péchoux, 2023; Marion, 2011). In the opposite direction, an ICC system was applied to cryptographic proofs (Baillot, Barthe, & Dal Lago, 2019). Although ⊤∗ NI has transformed from its origins to not enforce complexity bounds, it reinforces the bidirectional connection between ICC and language-based security. 3.2.7 Conclusion: Strengths, Limitations and Future Directions Anytime non-interference detects violations at any program point, enforcing a finer-grained security policy than classic non-interference that is defined in terms of inputs and outputs. We have presented ⊤∗ NI, a sound and compositional program logic, that captures the semantic security property of anytime non-interference in imperative programs. The logic assigns security flow matrices to commands where the matrices represent the program’s potentially interfering information flows. The logic is lightweight and does not require program anno287 tations, specialty compilers, and adds no run-time overhead. Beside the compelling theory, ⊤∗ NI can be implemented to obtain automated security analysis in practice. We have constructed a prototype static analyzer TYNI to analyze Java programs. By extension, TYNI can support a range of applications, e.g., security class inference, taint analysis, and security preservation analysis. Although the utility of ⊤∗ NI is encouraging, the development is still mainly theoretical. Our immediate priority is enriching the syntax with effectful functions and object oriented constructs. For additional strength, we hope to mechanize the theory. On the practical side, the prototype analyzer has room for enhancements. It already computes security-flow matrices, but an extension to the applications requires additional engineering steps. With the current syntax coverage, experimental comparisons are still out of scope. In the meantime, ⊤∗ NI provides an promising avenue for security analysis and future enhancements. 288 3.2.8 Appendix A: Proof of Thm. 3 A first useful observation is that if C′⊆C, then 𝕄(C′)is included in 𝕄(C), in the sense that 𝕄(C′)(x,y)=⟹ 𝕄(C)(x,y)=. This simple observation comes from our “additive” interpretation of commands, and is useful in proving our theorem. One should also note that if ℓis not anytime non-interfering for C’, then any class assignment extending ℓto Occ(C) is not anytime non-interfering for C. Theorem 3 (Correspondance).A program Cis anytime non-interfering for ℓ(Def. 22) if and only if ℓis anytime non-interfering for C(Def. 23). Proof. Let us assume given C,ℓ∶Occ(C)→SC, and that 𝕄(C)has been computed. For the if part Suppose that ℓis anytime non-interfering for C, but that Cis not anytime non-interfering for ℓ. Then there must exist a class c∈SC and a counter 𝑡such that for some 𝑣and  𝑤′, 𝑣 c ∼ 𝑤 (3.1) C[ 𝑣→  𝑣′]𝑡(3.2) C[ 𝑤→  𝑤′]𝑡(3.3)  𝑣′c ≁ 𝑤′(3.4) For c ≁the negation of c ∼, i.e., there must exists x𝑖such that ℓ(x𝑖)⩽c(3.5) 𝑣′𝑖≠𝑤′𝑖(3.6) For Equation 3.6 to hold, it must be the case that Ccontains a statement of the form x𝑖= e1,15 possibly guarded by while and if statements using the expressions 15Which can be t[e1 1]= e2 1, in which case we let Occ(e1)=Occ(e1 1)∪Occ(e2 1)and carry out the same reasoning. 289 e2,…,e𝑛. Let x1,…,x𝑚=⋃𝑛 𝑗=1Occ(e𝑗), and observe that since by Equation 3.1 our input value lists are up-to cequivalent, it must be the case that there exists 𝑗∈{1,…,𝑚}such that ℓ(x𝑗)>cor ℓ(x𝑗)⊥c, (3.7) otherwise Equation 3.6 could not hold.16 Furthermore, thanks to Equation 3.5 we know that 𝑗≠𝑖. (3.8) Let C′be the smallest sub-program of Cwhere x𝑖= e1occurs and either x𝑗∈Occ(e1) or x𝑗occurs in the condition of a while or if command guarding the command x𝑖↲ = e1. Intuitively, C′has one of the following forms: x𝑖=⋯x𝑗⋯; Listing 75: (A)ssignment Case while(⋯x𝑗⋯){ ⋯ x𝑖=⋯; ⋯ } Listing 76: (L)oop Case if(⋯x𝑗⋯){ ⋯ x𝑖=⋯; ⋯ } Listing 77: (B)ranching Case Hence, x𝑗∈In(C′),x𝑖∈Out(C′), and inspecting the rules of our interpretation allows us to conclude that 𝕄(C)(x𝑗,x𝑖)=, since 𝕄(C′)is included in 𝕄(C).17 16To be more rigorous, it could be the case that the classes of x1,…,x𝑚are cor below, but that one of them is itself impacted by a variable at a higher or incomparable class. To handle, this case, one simply replaces x𝑖 and x𝑗with those “problematic” variables, decreases the counter 𝑡to when the value of the one with the lower class was changed, and carry out the same reasoning, possibly repeating this step again. Since 𝑡decreased, we are guaranteed to identify “the first” anytime non-interference violation and to reason about it. 17In brief terms, this comes from Table 24, remembering that x𝑗being in the condition in the (L) and (B) cases implies that it is in In(C′)and that a was introduced between its in-variable and x𝑖’s out-variable in 𝕄(C′). 290 3.3 Certifying Complexity Analysis nImplicit computational complexity & formal methods Neea Rusch Workshop paper/ongoing research. The workshop paper was presented at the Ninth International Workshop on Coq for Programming Languages (CoqPL) 2023. 297 Abstract This work drafts a strategy that leverages the field of Implicit Computational Complexity to certify resource usage in imperative programs. This original approach sidesteps some of the most common–and difficult–obstacles “traditional” complexity theory face when implemented in Coq. 3.3.1 Motivation The ability to statically infer resource bounds of programs offers numerous benefits, e.g., to insure safe memory usage. Even more preferable if those guarantees are established with the rigor of formal verification, because that increases confidence in the obtained analysis result and enables integration of complexity analyses into larger formal developments. Unfortunately, computational complexity is notoriously difficult to represent formally for several reasons. In general, deriving a complexity bound for an arbitrary program is an undecidable problem. In the area of complexity theory, “formalisations of even basic complexitytheoretic results are not available” (Forster, Kunze, & Wuttke, 2020, p. 114), hindering certification attempts. For practical complexity analyses, many existing techniques present methodological challenges if they require e.g., program termination or inlining functions (Carbonneaux, Hoffmann, & Shao, 2015). Therefore, a realistic pathway toward formal certification of a program’s resource usage is narrow. A few encouraging early results exist, and we discuss some of those in §3.3.3. In this proposal we will sketch how a different approach, founded on Implicit Computational Complexity, could sidestep some of the usual difficulties in implementing and verifying complexity analyses in Coq. 298 The field of Implicit Computational Complexity (ICC) (Dal Lago, 2011) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. The core idea is to bound resources while the program is being written (or type checked) instead of measuring its resource usage afterwards on an abstract model of computation. This can be done through e.g., bounded recursion or using typing mechanisms. The goal is to find a syntactical restriction or a type system such that a program can be written or typed only if it belongs to a particular complexity class. ICC-based systems are often compositional, and they offer more natural tools to write programs than theoretical models of computation used in complexity theory. We speculate these combined properties could make ICC-approaches a conceivable pathway toward certified complexity and sketch a more detailed plan below. 3.3.2 Preliminary Action Plan We plan to formalize in Coq an ICC-based complexity analysis technique, the mwp-flow analysis (Jones & Kristiansen, 2009).20 We chose this method because its internal mechanics has been recently studied (Aubert, Rubiano, Rusch, & Seiller, 2022a), and by our assessment, it seems suitable for formalization in Coq. As for Coq, it seems like the ideal target language because of its existing libraries and preliminary work–some of which are discussed in §3.3.3–, most notably related to compilers (Leroy, 2009). 3.3.2.1 Overview of mwp-Flow Analysis The mwp-flow analysis certifies polynomial bounds on the size of the values manipulated by an imperative program. While it does not ensure (or require) program termination, it 20Where mwp stands for maximum, weak polynomial and polynomial, representing increasing growth rates of variables values. 299 provides a certificate guaranteeing that the program uses throughout its execution at most a polynomial amount of space, and as a consequence that if it terminates, it will do so in polynomial time in the size of its inputs. The analysis computes, for each program variable, a vector tracking how it depends on other variables. The vector values are determined by applying the nondeterminitic rules of the sound mwp-calculus to the commands of the program. Those vectors are collected in a matrix. A program is assigned a matrix only if all the values in it are bounded by a polynomial in the inputs sizes. This technique is compositional, abstracts away e.g., iteration bounds, and operates on a memory-less imperative language, reminiscent of the Imp language from Software Foundations (Pierce et al., 2025). 3.3.2.2 The Coq Formalization Our goal is to certify the analysis as presented in the original paper (Jones & Kristiansen, 2009). Note that this does not mean that the bound is certified, but that the mechanism to compute those bounds is certified. Of course, this implies the correctness of the bounds as a by-product but constitutes a major difference w.r.t. the results discussed in §3.3.3. Preliminary explorations have led us to establish the following milestones. The mathematical foundations Our first goal is to define the mathematical structure required to carry out the rest of the construction. This requires defining vectors, matrices and their operations, semi-rings, and honest polynomials21 that are needed to represent the mwp-bounds. The Mathematical Components library (Mahboubi & Tassi, 2022; Mathematical Components development team, 2024) will lay the foundations 21Which are “polynomial build up from constants in ℕand variables by applying the operations +(addition) and ×(multiplication).” (Jones & Kristiansen, 2009, p. 5) 300 for the linear algebra representations, but likely requires extensions to accommodate our specific analysis. Implementing the language The analyzed language is a simple imperative language that manipulates natural numbers, held in a fixed number of program variables. Its syntax includes variables, expressions (operations +and ×), Boolean expressions, and commands (e.g., assignment, loop and decision statements, command sequences, and skip), with their usual semantics. We expect implementing it and its small-steps semantics in Coq to be relatively simple, following the examples from Software Foundations (Pierce et al., 2024, 2025). Implementing the typing system Even if it can be computationally expensive to run an automatic inference (Aubert, Rubiano, Rusch, & Seiller, 2023b), the typing system in itself is relatively simple. It contains only 10 rules, essentially one for each type of command, and except for the initial assignment of vectors to variables, is fully deterministic. We conjecture that standard methods (Chlipala, 2010, 2022) to implement simple type systems will be enough, but will require some care to scale to the matrix-as-type paradigm of this analysis. Certifying the analysis This will be the most demanding part of our plan. The original paper contains all the required handwritten proofs, but the authors caution that “[t]hese proofs are long, technical and occasionally highly nontrivial” (Jones & Kristiansen, 2009, p. 2). The main result of the paper is the soundness proof of the analysis (Jones & Kristiansen, 2009, Theorem 5.3), i.e., the proof of the existence of a matrix typing the program implies the existence of an honest polynomial bounding the variables’ growth rates. The main result follows from 15 pages of proofs presented in section 7 of the paper. This section revolves around proving the soundness properties of the calculus, and we expect the most substantial effort to be spent on formalizing these proofs. Some of them are quite intricate but with a satisfactory level of detail. The 301 cases concerning soundness of loops are the most difficult on paper, but their inductive nature should (we hope!) be processed by Coq rather easily. We leave for future work the possibility of creating a formally verified, automatic static analyzer founded on the proof of correctness of this method: as we discussed in other works (Aubert, Rubiano, Rusch, & Seiller, 2022a, 2023b), care is required to implement a typing strategy that does not rapidly become intractable. 3.3.3 Related Work A few prior results exist that combine formalization of complexity and Coq. They range from practical analyses to proofs in computational complexity theory. For practical application, Coq has been used to verify stack bounds for assembly code (Carbonneaux, Hoffmann, Ramananandro, & Shao, 2014) and to obtain WCET loop-bound estimation (Blazy, Maroneze, & Pichardie, 2013). Carbonneaux et al. (Carbonneaux, Hoffmann, Reps, & Shao, 2017) presented an automatic static analyzer for imperative programs, and although the analyzer itself is not verified, it generates bounds with machine-checkable certificates, to guarantee that the computed bound holds. For functional paradigm, McCarthy et al. (McCarthy, Fetscher, New, Feltey, & Findler, 2018) developed a Coq library, with a monad that counts abstract steps, which enabled running time analysis of programs written using the monad. An ICC-based characterization was introduced by Férée et al. (Férée, Hym, Mayero, Moyen, & Nowak, 2018), in the form of a Coq library, that allows for readily proving that a function is computable in polynomial time. Coq has also been used to formalize some of the foundations of modern complexity theory. Ciaffaglione (Ciaffaglione, 2016) proved the undecidability of the halting problem. Guéneau et al. (Guéneau, Charguéraud, & Pottier, 2018) formalize the 𝒪notation. Forster 302 et al. (Forster, Kunze, & Wuttke, 2020) implemented a multi-tape to single-tape compiler, and introduced the first formalized Universal Turing Machine verified w.r.t. time and space complexity, for any model of computation, in any proof assistant. More recently, Gäher and Kunze formalized the Cook-Levin Theorem in Coq (Gäher & Kunze, 2021). Despite these advances, formalization of complexity is in early stages and basic complexity-theoretic results e.g., time and space hierarchy theorems, remain unavailable. Our proposed project differs from these earlier results primarily in its intent. We plan to formalize the complexity analysis mechanism itself—not its computed result, as was done previously. In their work with the Turing Machines, Forster et al. (Forster, Kunze, & Wuttke, 2020) were explicit in emphasizing the challenge they experienced in formalizing complexity. We hypothesize that our ICC-based approach, with e.g., its built-in abstractions, will help reduce this challenge. It is our hope that CoqPL will welcome our proposal for a certified complexity analysis in Coq, and will be keen on indicating any library, tool or resource that could help. 303 4 Discussion 304 4.1 Observations About Specific Techniques The specific techniques are the flow calculus of mwp-bounds and the QI Framework. 4.1.1 Advancements of the Flow Calculus The original flow calculus of mwp-bounds (Jones & Kristiansen, 2009) provides a purely syntactic, sound and compositional theoretical technique for analyzing value growth of variables in imperative programs. Although promising, the technique poses various application challenges. In particular, issues arise from the nondeterministic inference rules and handling of potential derivation failure. The developments presented in this dissertation resolve or ease those tensions in several directions. At conclusion, we have arrived to an enhanced variant—i.e., the MWP∞calculus—with richer capabilities and utility than the original system. From principles to practical efficiency. Two critical changes—in §7.1.3—were keeping track of derivation choices through polynomial structures, and introducing the flow coefficient ∞that tracks derivation failure. These adjustments enables exploring all derivation paths concurrently, without needing to back-track during the analysis procedure. In the new formulation every input program is assigned precisely one complex mwp-matrix, instead of up to exponentially many simple mwp-matrices. Although the technical adjustments make program analysis automatable, they also introduce a new problem. Critically, the mwp-bounds—that represent variable value growth and are the output of the analysis—become “hidden” in the complex matrix. It is necessary to invent ways to interpret the new complex data structure to mitigate the gap. 305 How to completely solve this new problem is described in a second “phase” of technical developments, in §3.1. The manuscript provides an evaluation procedure that enables recovering mwp-bounds from a complex mwp-matrix. With this enhancement, the MWP∞ calculus computes mwp-bounds that are comparable to the original calculus, but in a practically efficient way. The surpassing capabilities. Because the complex mwp-matrix contains information about all derivations,1the MWP∞calculus enables certain analysis features that are not possible in the original calculus. For example, it is possible to determine the optimal mwp-bounds of each program variable. In case of derivation failure, it is possible to precisely identify the variable(s) involved, and the program point that induces the failure. It may also be possible to bound the value growth of certain variables in presence of whole-program derivation failure. This increases expressiveness, because it enables bounding more variables than what was previously possible (refer to §3.1.7 for comparison). A critical step to obtain these capabilities is projecting the complex mwp-matrices on individual variables (described in §3.1.4.3). Extracting new information from programs. A side effect of the derivation-history tracking is that it enables extracting new information about the analyzed program. Although a complex mwp-matrix encapsulates the information, a clever strategy is required to extract it. A bit surprisingly, the evaluation procedure—developed in §3.1.4.2 to determine mwpbounds—serves as a kind of “oracle” method. We can issue “queries” against it to answer a variety of questions about the analyzed program. For example, the following questions can be answered. 1Essentially, the complex mwp-matrix encodes a derivation history. 306 exists for breaking the security mechanism. Yet, these are isolated use cases; a coarse binary analysis has limited utility in general. The practical relevance of an analysis increases if we can show it can support software engineering or verification tasks. Such analyses produce quantitative information that helps engineers understand the program behavior, and detect and repair issues early. Ideally, an analysis should express resource bounds and flag resource-intensive procedures. Certain ICC systems—like the flow calculus of mwp-bounds—can target such the practically-oriented applications up to an extent. However, if some computation exceeds polynomial bounds, the analysis should still yield an informative result. This last requirement is often beyond capabilities of ICC systems (Baillot, Dal Lago, & Moyen, 2012). On the analysis input side, the utility improves with expressive power. Essentially, we would want the analyzer to handle the rich constructs that occur in real-world programs. ICC systems are typically defined on core languages (“toy” languages). However, it is possible to work around this limitation by focusing on interesting sub-classes of programs, e.g., integer programs or numerical loops. Through compositional analysis of program fragments, ICC systems extend to analysis of general programming languages. This approach is demonstrated in pymwp (§2.1). Having a restricted syntax is thus not an insurmountable hurdle to applications, in our experience. To make an analysis comparable with many existing resource analyzers (Montoya, 2017c), it suffices to target the C Integer Programs grammar (Termination Portal, 2015) used in the Termination Competition (Giesl, Rubio, Sternagel, Waldmann, & Yamada, 2019). 4.2.2 Motivating Analyzer Developments A second line of observations concerns the automatic resources analyzers. There are various challenges with locating, reusing, and running experiments with the analyzers. 313 First, resource analyzers differ greatly in input/output formats (cf. §1.2.2.4). For example, the ones that are based on cost equation systems are different from the analyzers of C programs. This is problematic because it is difficult to faithfully compare new techniques with the existing ones (on the same workloads), or replace an analyzer with an alternative. Although some concerted efforts—like the Termination Competition—push to establish a shared I/O format, there is no widely adopted standard. Since resource analyzers are primarily developed as “standalone” tools, their continued maintenance and development is not strongly incentivized. Certain analyzers, although they regularly appear in scientific literature, are inaccessible (Sinn, Zuleger, & Veith, 2017), difficult to locate (Carbonneaux, Hoffmann, & Shao, 2015), or deprecated (Gulwani, Mehra, & Chilimbi, 2009; Srikanth, Sahin, & Harris, 2017). These issues extend beyond resource analysis. Scientific software is general differs from “mainstream” software (Hannay, MacLeod, Singer, Langtangen, Pfahl, & Wilson, 2009; Joppa et al., 2013). For example, scientific software aims to materialize ideas that correspond to publishable research results. After presentation, the software is archived (ACM, 2020), and authors move on to the next prototype. This pattern does not encourage solving the issues identified earlier. One community, that operates differently, is formal methods (see as evidence Table 8). Many formal verification tools are developed with continuity in mind (Beyer, 2022; TPTP.org, 2025). Moreover, the SMT-LIB Standard (Barrett, Clark and Fontaine, Pascal and Tinelli, Cesare, 2025) is a model for promoting the adoption of common languages interface. It would be beneficial for resource analyzers to follow similar practices. 314 4.2.3 The Implicit Costs of Applied ICC The dissertation manuscripts follow a pattern of pairing ICC with a secondary research domain. While such intersectional strategy comes with rich application potential, a substantial challenge involved identifying suitable research domains where ICC techniques could offer meaningful benefit. There are thus added “costs” with this research strategy, as suggested in §1.1.2. One cost that became particularly pronounced was the learning overhead. This is reflected in §1.2. Making a meaningful contribution requires first having sufficient familiarity with the secondary domain to identify research gaps. It also requires learning the terminology and implicit assumptions of the secondary domain. For example, in presenting developments of the flow calculus, we learned through trial-and-error that experiments were necessary to support our findings. The second cost is about understanding different measures of significance. While we might hold the theoretical origins in high esteem, it becomes minutiae when targeting applications in other domains. Using an ICC technique to solve a problem in ways that is comparable to existing techniques is not enough for a scientific contribution. The significance of the application must be standalone and independent of the theoretical origin. In other words, a technique becomes interesting only after we can show that it can solve an interesting problem. This described research strategy has repeated a few times throughout the dissertation, thus multiplying these costs. Following the strategy requires persistence, and due to the learning overhead, is quite challenging for dissertation research. 315 4.3 Open Problems for Future Work 4.3.1 Questions About the Flow Calculus The following questions remain unanswered about the flow calculus of mwp-bounds. •Have the developments changed the complexity of the derivability problem?5The manuscripts in §7.1, §2.1, and §3.1 alter the inference procedure, therefore the answer is not obvious. •How to obtain concrete bounds from mwp-bounds? The honest polynomials of mwpbounds are composed of variables, constants, and operators, but how to extract the exact combination is unclear. •Could the flow-calculus also capture lower bounds? A lower bounds analysis would complement the existing capabilities by detecting variables that have certainly exponential value growth, which is useful e.g., for bug finding. •Issues around translating real-world programming languages to the imperative language of the flow calculus. Although the flow calculus inference rules are phrased as while and loop commands, they should be interpreted as unbounded and bounded loops. An ideal translation should compile the input program to the language of the flow calculus, while accounting for loop boundedness. A solution might be already available in the compilers literature. •How to account for various rich program constructs, like arrays? Looping over arrays is a frequently occurring programming pattern. Although this is a natural extension to the flow calculus, there is no existing approach to this problem. 5The problem is NP-complete by (Jones & Kristiansen, 2009, p. 40)). 316 As evidenced in these open programs, the flow calculus of mwp-bounds is interesting because it provides an extensible and rich logical framework for reasoning. Its full potential still remains to be explored. 4.3.2 Other Emerging Research Questions Generalizing the loop distribution. The solution of §2.2 assumes a setting where loop distribution should be applied. Relaxing this assumption raises at least two new important questions relating to the loop transformation strategy. First, loop distribution and parallelization introduce computational overhead. The overhead comes from replicating loop headers across distributed loops and instrumenting parallel runtimes. It is therefore necessary to first determine the profitability of the operation. Only if the operation is beneficial by some metric, should we “accept” the overhead of loop distribution. Second, compiler loop transformations do not occur in isolation. We must consider combinations of loop transformations—like fusion, tiling, and interchange, etc.—and their combined effect on the input program. Investigating these questions is a natural extension of the prior work. Complexity-by-Construction. The X-by-Construction paradigm (ter Beek, Cleophas, Schaefer, & Watson, 2018) is concerned with ensuring non-functional properties by construction. The XbC aim is to automatically generate error-free software from specifications (ter Beek, Cleophas, Legay, Schaefer, & Watson, 2020). ICC systems define the programming language-based mechanics to construct polytime programs, therefore it is conceivable that ICC systems could extend the XbC approach in cases where X stands for complexity. It would require pairing ICC techniques with program synthesis. Conceptually, this is the “bottom-up” dual of the “top-down” approach implemented in pymwp. 317 Formally verifying complexity. ICC systems are based on programming languages, making them naturally suited to formalization. However, the number of works that support this claim is still modest—refer to e.g., (Atkey, 2024; Férée, Hym, Mayero, Moyen, & Nowak, 2018; Heraud & Nowak, 2011). The investigation is necessary to have formal guarantees of complexity. There are two separate questions (i) the formalization of logical systems that provide guarantees, and (ii) formalizing analyzers that provide complexity guarantees. The existing works address the first question. The closes solution to the second is giving guarantees to the results computed by an analyzer (Carbonneaux, Hoffmann, Reps, & Shao, 2017). Extending beyond traditional programming paradigms. ICC has been widely studied in the context of “traditional” programming paradigms, including imperative and functional programs.6However, there are many more important programming paradigms, like probabilistic programs and quantum computing, that warrant investigation. These paradigms change the notion of programming languages and thus require different analytical approaches. Representative works exploring this direction include (Avanzini, Moser, Péchoux, & Perdrix, 2024; Avanzini, Moser, & Schaper, 2020; Colledan & Dal Lago, 2024; Dal Lago, Masini, & Zorzi, 2010). 4.4 Completion of Dissertation Goals As part of the dissertation aims, Section §1.1.3 outlined four goals. We can now assess the completion status of the goals. 6For example, the works building on Resource Aware ML (Hoffmann, Aehlig, & Hofmann, 2012) have been extended to many paradigms. 318 ŐGoal 1. Extend applied capabilities in automatic program analysis and verification. The works extending the flow calculus of mwp-bounds—in Sections §7.1, §2.1, and §3.1)—and the loop distribution technique of §2.2, immediately support the goal. Each manuscript takes lifts implicit computational complexity beyond its theoretical origins, and demonstrates its uses in an applied context. The complementary nature of these techniques is discussed in §2.1.2.3 (see in particular Table 10), §2.2.4 and §3.1.6. Therefore, the goal was met satisfactorily. ЗGoal 2. Take ICC techniques closer to integration with real-world software development workflows. The dissertation work is consistently supported by software artifacts (cf. §8). While the artifacts demonstrate the practical relevance of the investigations, and have driven advancements in the underlying theories, the results so far are still a step in “isolation”. Integrating techniques based on implicit computational complexity into other software development tools (compilers, verifiers, etc.) is important to promote relevance and continue advancement of ICC. Such ambitions encourage thinking about ICC from new (more practical) perspectives. However, concrete integration remains as an outstanding goal. The work in using the flow calculus to infer specification conditions (Rusch, 2025a) is one step in that direction. ЗGoal 3. Initiate conversations about the relevance of ICC applications. The third goal is “internal” to those who are already familiar with ICC. The dissertation introduction (i.e., “Addressed Problem” in §1.1.2), and the introduction to ICC (“A Snapshot of Theoretical Results” in §1.2.1.4), both highlighted the strong preference for pure theoretical development. Taking inspiration from (Moyen, 2017), the motivation is to push theoretical developments beyond this pure framing. There was some progress in initiating conversations about applications—via (Aubert, Rubiano, Rusch, & Seiller, 2022a) and a presentation at the Seminar on Semantic and Formal Approaches to Complexity (Rusch, 2023))—but the overall effort toward the goal was limited. Al319 though this outcome is less than ideal, the motivations presented in the published works, and this dissertation, will remain discoverable to others in perpetuity. ŐGoal 4. Expose ideas from implicit computational complexity to broader research communities. The dissemination of the dissertation work involved many written works and giving presentations to diverse audiences. The “themes” of the presentations venues included type theory (the TYPES’22 conference (Aubert, Rubiano, Rusch, & Seiller, 2022d)), interactive theorem proving (CoqPL’23 (Aubert, Rubiano, Rusch, & Seiller, 2023c)), language-based security (PLAS’24 (Aubert & Rusch, 2024)), and programming languages (at the doctoral symposiums of SPLASH’22 (Rusch, 2022) and ECOOP’25 (Rusch, 2025b)), to name a few. The number of attendees at these events was in the magnitude of hundreds. Based on observation, implicit computational complexity was largely an unfamiliar topic to the audiences. Conversely, through the different modes of dissemination, a substantial effort was made to increase exposure and awareness of implicit computational complexity. Therefore, the final goal was satisfactorily met. Although the goals were completed with a mixed degree of success, there was progress in every direction. The goals are intentionally open-ended. They need not be fully achieved within the timespan of doctoral studies. It is always possible to push further, even in the cases that were completed satisfactorily. 4.5 Research Conclusions We can now summarize the key takeaways of this dissertation – in Fig. 36. The first finding recognizes the fact that Implicit computational complexity offers complementary techniques to perform automatic resource analysis (cf. §7.1 and §2.1). However, 320 Primary findings. 1. Implicit computational complexit (ICC) provides complementary techniques of automatic resource analysis. 2. ICC systems are flexible and can be modified to track other non-functional properties, beyond complexity. 3. Although this dissertation has provided early evidence, continued exploration is needed to unlock further application potential. Figure 36: Primary research findings. such applications may require substantial adjustment to the base theory. While designing ICC systems, it is therefore important to consider practical challenges ahead of time. The second finding emphasizes extensibility. Starting with an ICC system, it is possible to adjust it to track alternate properties. The value of such exploration is two-fold. Due to the unusual starting point, the obtained analysis may be complementary to existing techniques (as in §2.2). Moreover, the adjustment provides new insights of the technique itself. The third finding is reflective. The dissertation investigation has explored many applications of ICC. However, investigation has been far from exhaustive and many more applications remain to be discovered. In particular, the guarantees ICC can offer by construction should be investigated further. Yet, such exploration necessitates a viewpoint shift and seeing ICC as more than “just” a complementary approach to complexity theory. When viewed broadly, ICC systems become rich reasoning frameworks that allow analyzing and verifying wide varieties of program properties. 321 5 Summary 322 5.1.3.2 Analyzing Extended Properties The second series of work applies implicit computational complexity to track other nonfunctional properties. The idea is to select an ICC system and adjust it to capture a different non-functional property. The motivation is multifaceted. It requires developing deep understanding of the mechanics of the chosen technique. Conceptually, it pushes to think about ICC outside the usual frame of computational complexity. Lastly, investigations in this direction are important to expose ICC to broader research communities, since the application is shifted away from (or beyond) resource consumption. In this series of work, the starting point is an ICC system based on quasi-invariants (QI), as formulated in (Moyen, Rubiano, & Seiller, 2017a). Similar to the flow calculus, the QI framework is a data-flow analysis of imperative programs. However, the QI framework supports a richer input language and is founded on a seemingly adjustable mathematical framework. In the prior formulation (Moyen, Rubiano, & Seiller, 2017a), it was used to obtain a compile-time program optimization. The optimization lifts nested loops outside their containing loop, such that post-transformation the program complexity is reduced. We ask the following questions about the extended uses of the QI framework. (RQ4) How to develop a program transformation to increase parallelization potential? (RQ5) How to use it to analyze security properties, specifically non-interference? Research questions 4 and 5 are posed here with an air of obviousness. However, arriving to those questions was not obvious. A substantial hidden challenge of the dissertation research plan involves identifying suitable research domains—like parallel programming or language-based security (Sabelfeld & Myers, 2003)—where ICC-based techniques could offer meaningful benefit. 329 Another consideration is that adjusting an ICC system may lead to losing the original guarantee about resource consumption. In return, we gain an alternative guarantee about program behavior. Whether this trade is beneficial depends on the application. Therefore, besides tracking properties, this investigation is also about studying the mechanics of ICC systems, and uncovering how exactly they provide behavioral guarantees. Finally, this direction of research contains a bonus challenge. Simply showing that an ICCbased technique can solve a problem in another application domain is not enough. It is necessary to show that the solution is independently relevant in the target domain, regardless of the origins of the solution. Based on experience, this criterion is strongly enforced by the scientific peer review process. 5.1.4 Methodology and Research Deliverables Following the approaches of §5.1.3, we conducted a series of investigations. These resulted in several publications (Aubert, Rubiano, Rusch, & Seiller, 2022a, 2023b; Aubert, Rubiano, Rusch, & Seiller, 2023e), workshop presentations (Aubert, Rubiano, Rusch, & Seiller, 2022d, 2023c; Rusch, 2022), and ongoing work. We can summarize the main contributions as follows. For RQ1, we enhanced the theory to develop an automatic resource analysis in (Aubert, Rubiano, Rusch, & Seiller, 2022a, 2023b; Rusch, 2025a). Due to inherent nondeterminism, developing an efficient and useful practical analysis was surprisingly difficult, but eventually achievable. The enhanced flow calculus can answer the same questions as the original formulation, but automatically and in practice. Moreover, through the enhancements we discovered how to make the calculus more expressive, allowing it to cover a larger class of programs than the original theory (Rusch, 2025a). The flow calculus is implemented 330 as an open source static analyzer, pymwp1,2 for analyzing a subset of C programs (Aubert, Rubiano, Rusch, & Seiller, 2023b). Based on this work, we discovered that the analysis can support inference of specification conditions (Rusch, 2025a) that are needed for formal verification. This finding corresponds to RQ3. Proving the soundness of the flow calculus (RQ2) is still ongoing work (Aubert, Rubiano, Rusch, & Seiller, 2023e). However, given the other developments, a formalization effort is now even more strongly motivated and justified. Along the second direction, for RQ4, we applied the QI framework to develop a program optimization for loop parallelization (Aubert, Rubiano, Rusch, & Seiller, 2023e). This is useful, because the optimization can be applied to loops whose iteration count is unknown. Parallelizing such loops is outside the capabilities of prior techniques. In an ongoing investigation, for RQ5, we apply the QI framework to tracking programs non-interference (Goguen & Meseguer, 1982), a kind of confidentiality property. Non-interference ensures a program does not reveal secrets; and if it does, we can identify where the violation occurs. Our working intuition is that, since the analysis can be adjusted to different programming languages, it enables tracking preservation of the non-interference property at different compilation stages, while a program is transformed from source code to an executable. This is different from many existing techniques that analyze programs only at one stage of representation. 5.1.5 Research Findings and Conclusions On automatic resource analysis. We can now confirm that it is possible to obtain automatic program analysis from the flow calculus of mwp-bounds, but only after substantial 1Pronounced paI em double-you pē. 2https://statycc.github.io/pymwp/ 331 adjustments. An efficient program analysis required inventing ways to manage costly subcomputations and solving additional problems that were exposed in the process. At conclusion, the enhanced technique is not just automatable, but can analyze more programs than the original theory. We can now confirm the analysis results are complementary to alternative state-of-the-art techniques (Aubert, Rubiano, Rusch, & Seiller, 2023b, p. 5). Thus, it enables us to analyze different questions about resource consumption. The implemented flow calculus can also be used in specification inference. There are potentially many more applications of the flow calculus remaining to be discovered. On analysis of extended program properties. The QI framework provides a case example showing that ICC systems can be flexible enough to track other program properties. While adjusting the system, we made a surprising discovery in that changing the property of interest simplified the mathematical analysis. For example, to track a complexity property, we must compute fixed points and preserve the program command order. In the adjusted analysis, it was possible to relax these conditions. More generally, that the QI framework can be used to track various properties is reminiscent of the Dependency Core Calculus (DCC) (Abadi, Banerjee, Heintze, & Riecke, 1999). In DCC, different program properties are modeled as instances of a central notion of dependency. This mirrors our observations about the QI framework. This suggests that the QI framework encapsulates even wider utility than uncovered so far during this dissertation work. On broader dissertation goals. Zooming out of the specific projects, we can reflect on the main hypothesis and the research goals. We have successfully gathered evidence of the application potential of ICC. The evidence supports the main hypothesis, but is still too limited to draw generalizing conclusions. However, our experiences of developing the ICC systems strongly reinforced the symbiotic view of theory and application. In the process, we faced many scientific and engineering challenges, and identified compelling motivations to 332 justify the investigations. At conclusion, we have strengthened the theories of interest and clarified their practical relevance. In §5.1.2, we crafted four goals to define the dissertation expectations. The first was about extending the applied capabilities of ICC, which was met successfully. The second was about introducing ICC in development workflows. Although we have developed a static analyzer, it is a step in “isolation.” Integrating ICC analyses into other software development tools (compilers, verifiers, etc.) remains as an outstanding task. Such integration is important to promote relevance and continue development of ICC techniques. Our work in using the flow calculus to infer specification conditions (Rusch, 2025a) is a first step in that direction. The last two goals were social and about disseminating ideas across research communities. Within the ICC community, our efforts materialized in seminar talks and informal conversations. Although this record is below ideal, the ideas in the published works will remain discoverable to others in written form, asynchronously and in perpetuity, like (Moyen, 2017). In regard to other communities, we were successful at exposing the work at verification, programming languages, and security venues. Thus, the fourth goal was satisfactorily met. Final thoughts & future perspectives. The ICC approach of guaranteeing program properties demonstrates great applied potential. For example, if offers a pathway toward formal verification of many non-functional properties. One research direction, that deserves more attention, is applying ICC systems to ensure properties by construction. This would provide guarantees before any program exists and eliminates the need for aposteriori analysis. Although the dissertation research did not extend that far, exploring this direction is an intriguing future goal. Whether it is attainable depends crucially on a viewpoint shift. We should regard implicit computational complexity in the broader context it offers—including as a rich toolbox of techniques for static program analysis—and continue the exploration of 333 its applied potential. 334 6 References Aaronson, S., Kuperberg, G., & Habryka, O. (2025). Complexity Zoo [Accessed: 2025-0625]. https://complexityzoo.net/Complexity_Zoo Abadi, M., Banerjee, A., Heintze, N., & Riecke, J. G. (1999). A core calculus of dependency. Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 147–160. https://doi.org/10.1145/292540.292555 Abel, A., & Altenkirch, T. (2002). A predicative analysis of structural recursion. Journal of Functional Programming,12(1), 1–41. https://doi.org/10.1017/S09567968010041 91 Abu-Sufah, Kuck, & Lawrie. (1981). On the Performance Enhancement of Paging Systems Through Program Analysis and Transformations. IEE Transactions on Computers, C-30(5), 341–356. https://doi.org/10.1109/TC.1981.1675792 Aceto, L., Gorla, D., & Lybech, S. (2024). A Sound Type System for Secure Currency Flow. 38th European Conference on Object-Oriented Programming (ECOOP 2024),313, 1:1–1:27. https://doi.org/10.4230/LIPIcs.ECOOP.2024.1 ACM. (2020, August). Artifact Review and Badging - Current (Artifact Review and Badging Version 1.1 - August 24, 2020) [Accessed: 2025-03-22]. ACM. https://www.acm.o rg/publications/policies/artifact-review-and-badging-current Affeldt, R. (2025, January). An Introduction to MathComp-Analysis (Version 9 - January 13, 2025) [Accessed: 2025-05-07]. Lecture notes. https://staff.aist.go.jp/reynald.aff eldt/documents/karate-coq.pdf Aho, A. V., Lam, M. S., Sethi, R., & Ullman, J. D. (2006, August). Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley. Aho, A. V., Lam, M. S., Sethi, R., & Ullman, J. D. (2007). Compilers Principles, Techniques & Tools (2nd Edition). Pearson Education. Alagarsamy, S., Tantithamthavorn, C., & Aleti, A. (2024). A3Test: Assertion-Augmented Automated Test case generation. Information and Software Technology,176, 107565. https://doi.org/10.1016/j.infsof.2024.107565 Albert, E., Arenas, P., Genaim, S., & Puebla, G. (2008). Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In Static Analysis (pp. 221–237). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-69166-2_15 Albert, E., Arenas, P., Genaim, S., & Puebla, G. (2010). Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning,46(2), 161–203. https://doi .org/10.1007/s10817-010-9174-1 Albert, E., Arenas, P., Genaim, S., Puebla, G., & Zanardini, D. (2007). COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W. P. de Roever (Eds.), Formal Methods for Components and Objects (pp. 113–132, Vol. 5382). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-92188-2_5 335 Albert, E., Arenas, P., Genaim, S., Puebla, G., & Zanardini, D. (2012). Cost analysis of object-oriented bytecode programs. Theoretical Computer Science,413(1), 142– 159. https://doi.org/10.1016/j.tcs.2011.07.009 Albert, E., Bofill, M., Borralleras, C., Martin-Martin, E., & Rubio, A. (2019). Resource Analysis driven by (Conditional) Termination Proofs. Theory and Practice of Logic Programming,19(5–6), 722–739. https://doi.org/10.1017/s1471068419000152 Alias, C., Darte, A., Feautrier, P., & Gonnord, L. (2010). Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. Static Analysis, 117–133. https://doi.org/10.1007/978-3-642-15769-1_8 Allen, F. E. (1970). Control flow analysis. ACM SIGPLAN Notices,5(7), 1–19. https://doi .org/10.1145/390013.808479 Amadio, R. M., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D. P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C. S., Stark, I., & Tranquilli, P. (2013). Certified Complexity (CerCo). In U. D. Lago & R. Peña (Eds.), Foundational and Practical Aspects of Resource Analysis (pp. 1–18, Vol. 8552). Springer International Publishing. https://doi.org/10.1007/978-3-319-1 2466-7_1 Amini, M. (2012, December). Source-to-Source Automatic Program Transformations for GPU-like Hardware Accelerators [PhD thesis]. Ecole Nationale Supérieure des Mines de Paris. https://pastel.archives-ouvertes.fr/pastel-00958033 Amini, M., Creusillet, B., Even, S., Keryell, R., Goubier, O., Guelton, S., Mcmahon, J. O., Pasquier, F.-X., Péan, G., & Villalon, P. (2012). Par4All: From Convex Array Regions to Heterogeneous Computing. IMPACT 2012 : Second International Workshop on Polyhedral Compilation Techniques HiPEAC 2012. https://hal-mines-paristech .archives-ouvertes.fr/hal-00744733 Arabnejad, H., Bispo, J., Cardoso, J. M. P., & Barbosa, J. G. (2020). Source-to-source compilation targeting OpenMP-based automatic parallelization of C applications. The Journal of Supercomputing,76(9), 6753–6785. https://doi.org/10.1007/s11227-01 9-03109-9 Ariane 501 Inquiry Board. (1996). ARIANE 5 Flight 501 Failure (Technical report). European Space Agency. https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., Le Traon, Y., Octeau, D., & McDaniel, P. (2014). FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. ACM SIGPLAN Notices,49(6), 259–269. https://doi.org/10.1145/2666356.2594299 Atkey, R. (2024). Polynomial Time and Dependent Types. Proceedings of the ACM on Programming Languages,8(POPL), 2288–2317. https://doi.org/10.1145/3632918 Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2021, March). LQICM On C Toy Parser (Version 3.0.0) [git rev e21a3c9]. https://github.com/statycc/LQICM_On_C_Toy _Parser Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2022a). mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), 228, 26:1–26:23. https://doi.org/10.4230/LIPIcs.FSCD.2022.26 336 Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2022b, May). A Novel Loop Fission Technique Inspired by Implicit Computational Complexity [Draft]. https://hal.archivesouvertes.fr/hal-03669387v1 Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2022d, June). Realizing Implicit Computational Complexity [At the 28th International Conference on Types for Proofs and Programs (TYPES)]. https://types22.inria.fr/files/2022/06/TYPES_2022_paper_1 4.pdf Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2023a). pymwp documentation [Accessed: 2025-06-23]. https://statycc.github.io/pymwp/ Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2023b). pymwp: A Static Analyzer Determining Polynomial Growth Bounds. In Automated Technology for Verification and Analysis (pp. 263–275). Springer Nature Switzerland. https://doi.org/10.1007/9783-031-45332-8_14 Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2023c, January). Certifying Complexity Analysis [At the Ninth International Workshop on Coq for Programming Languages (CoqPL)]. https://hal.science/hal-04083105v1/file/main.pdf Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2025, March). pymwp: MWP analysis in Python (Version 0.5.4). Zenodo. https://doi.org/10.5281/zenodo.7879822 Aubert, C., & Rusch, N. (2024, October). Presentation of “An Information Flow Calculus for Non-Interference” [Accessed: 2025-09-14]. https://plas24.github.io Presentation at the PLAS 2024 Workshop. Aubert, C., & Seiller, T. (2016). Logarithmic space and permutations. Information and Computation,248, 2–21. https://doi.org/10.1016/j.ic.2014.01.018 Aubert, C. A., Rubiano, T., Rusch, N., & Seiller, T. (2023e). Distributing and Parallelizing Non-canonical Loops. In Verification, Model Checking, and Abstract Interpretation (pp. 1–24). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-24950 -1_1 Avanzini, M., & Dal Lago, U. (2017). Automating Sized-Type Inference for Complexity Analysis. Proceedings of the ACM on Programming Languages,1(ICFP), 43:1– 43:29. https://doi.org/10.1145/3110287 Avanzini, M., Moser, G., Péchoux, R., & Perdrix, S. (2024). On the hardness of analyzing quantum programs quantitatively. In Programming languages and systems (pp. 31– 58). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-57267-8_2 Avanzini, M., Moser, G., & Schaper, M. (2016). TcT: Tyrolean Complexity Tool. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 407–423). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49674-9_24 Avanzini, M., Moser, G., & Schaper, M. (2020). A modular cost analysis for probabilistic programs. Proceedings of the ACM on Programming Languages,4(OOPSLA), 1– 30. https://doi.org/10.1145/3428240 Avanzini, M., Moser, G., & Schnabl, A. (2008). Automated Implicit Computational Complexity Analysis (System Description). In Automated Reasoning (pp. 132–138). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_10 Bae, H., Mustafa, D., Lee, J., Aurangzeb, Lin, H., Dave, C., Eigenmann, R., & Midkiff, S. P. (2013). The Cetus Source-to-Source Compiler Infrastructure: Overview and 337 Evaluation. International Journal of Parallel Programming,41(6), 753–767. https: //doi.org/10.1007/s10766-012-0211-z Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking [Contributor Kim Guldstrand Larsen]. The MIT Press. Baillot, P., Barthe, G., & Dal Lago, U. (2015). Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 203–218). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_15 Baillot, P., Barthe, G., & Dal Lago, U. (2019). Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. Journal of Automated Reasoning,63(4), 813–855. https://doi.org/10.1007/s10817-019-09530-2 Baillot, P., Dal Lago, U., & Moyen, J.-Y. (2012). On quasi-interpretations, blind abstractions and implicit complexity. Mathematical Structures in Computer Science,22(4), 549– 580. https://doi.org/10.1017/s0960129511000685 Baillot, P., & Terui, K. (2004). Light Types for Polynomial Time Computation in LambdaCalculus. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004, 266–275. https://doi.org/10.1109/LICS.2004.1319621 Banerjee, U. (1997). Dependence analysis (Vol. 3). Springer Science and Business Media. https://doi.org/10.1007/b102376 Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., & Strub, P.-Y. (2021). Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, 2541–2563. https://doi.org/10.1145/3460120.3484548 Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., & Strub, P.-Y. (2023). Mechanized proofs of adversarial complexity and application to universal composability. ACM Transactions on Privacy and Security,26(3), 1–34. https://doi.org/10.1145/3589962 Barrett, Clark and Fontaine, Pascal and Tinelli, Cesare. (2025). The SMT-LIB Standard, Version 2.7 (Technical report). Department of Computer Science, The University of Iowa. https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.pdf Barthe, G., Basu, A., & Rezk, T. (2004). Security Types Preserving Compilation. Verification, Model Checking, and Abstract Interpretation,2937, 2–15. https://doi.org/10.1 007/978-3-540-24622-0_2 Barthe, G., Demange, D., & Pichardie, D. (2014). Formal Verification of an SSA-Based Middle-End for CompCert. ACM Transactions on Programming Languages and Systems,36(1), 4:1–4:35. https://doi.org/10.1145/2579080 Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., & Strub, P.-Y. (2014). Easycrypt: A tutorial. In Foundations of security analysis and design vii (pp. 146–166). Springer International Publishing. https://doi.org/10.1007/978-3-319-10082-1_6 Barthe, G., Grégoire, B., & Zanella Béguelin, S. (2009). Formal certification of code-based cryptographic proofs. Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 90–101. https://doi.org/10.1145 /1480881.1480894 Barthe, G., Pichardie, D., & Rezk, T. (2007). A Certified Lightweight Non-interference Java Bytecode Verifier. In Programming Languages and Systems (pp. 125–140). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-71316-6_10 338 Flores-Montoya, A., & Hähnle, R. (2014). Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems (pp. 275–295). Springer International Publishing. https://doi.org/10.1007/978-3-319-12736-1_15 Focardi, R., & Gorrieri, R. (1997). The Compositional Security Checker: a tool for the verification of information flow security properties. IEEE Transactions on Software Engineering,23(9), 550–571. https://doi.org/10.1109/32.629493 Forster, Y., Kunze, F., & Wuttke, M. (2020). Verified programming of Turing machines in Coq. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 114–128. https://doi.org/10.1145/3372885.3373816 Frumin, D., Krebbers, R., & Birkedal, L. (2021). Compositional Non-Interference for FineGrained Concurrent Programs. 2021 IEEE Symposium on Security and Privacy (SP), 1416–1433. https://doi.org/10.1109/sp40001.2021.00003 Furia, C. A. (2014). Software Verification Assertion Inference†[Accessed: 2025-04-19]. https://se.inf.ethz.ch/courses/2014b_fall/sv/slides/06-AssertionInference.pdf Lecture notes of Software Verification course, ETH Zürich, Fall 2014. Furia, C. A., Meyer, B., & Velder, S. (2014). Loop invariants: Analysis, classification, and examples. ACM Computing Surveys,46(3), 1–51. https://doi.org/10.1145/2506375 Furia, C. A., & Meyer, B. (2010). Inferring Loop Invariants Using Postconditions. In A. Blass, N. Dershowitz, & W. Reisig (Eds.), Fields of Logic and Computation (pp. 277–300). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-150 25-8_15 Gäher, L., & Kunze, F. (2021). Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. 12th International Conference on Interactive Theorem Proving (ITP 2021), 193, 20:1–20:18. https://doi.org/10.4230/LIPIcs.ITP.2021.20 Garg, D., & Pfenning, F. (2006). Non-Interference in Constructive Authorization Logic. 19th IEEE Computer Security Foundations Workshop (CSFW’06), 283–296. https: //doi.org/10.1109/csfw.2006.18 Silber, G.-A., & Pop, S. (2022). gcc.gnu.org Git - gcc.git/blob - gcc/tree-loop-distribution.c [Accessed: 2025-06-23]. https://gcc.gnu.org/git/?p=gcc.git;a=blob;f=gcc/tree-loop -distribution.c;h=65aa1df4abae2c6acf40299f710bc62ee6bacc07;hb=HEAD#l39 Georges, A. L., Peters, B., Elbeheiry, L., White, L., Dolan, S., Eisenberg, R. A., Casinghino, C., Pottier, F., & Dreyer, D. (2025). Data race freedom à la mode. Proceedings of the ACM on Programming Languages,9(POPL), 656–686. https://doi.org/10.1145 /3704859 Giallorenzo, S., Montesi, F., & Peressotti, M. (2024). Choral: Object-oriented Choreographic Programming. ACM Transactions on Programming Languages and Systems,46(1), 1–59. https://doi.org/10.1145/3632398 Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., & Thiemann, R. (2016). Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning,58(1), 3–31. https://doi.org/10.100 7/s10817-016-9388-y Giesl, J., Lommen, N., Hark, M., & Meyer, F. (2022). Improving Automatic Complexity Analysis of Integer Programs. In The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthda 345 (pp. 193–228). Springer International Publishing. https://doi.org/10.1007/978-3-03 1-08166-8_10 Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., & Yamada, A. (2019). The termination and complexity competition. In D. Beyer, M. Huisman, F. Kordon, & B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 156–166, Vol. 11429). Springer International Publishing. https://doi.org/10.1007/978-3-03017502-3_10 Goguen, J. A., & Meseguer, J. (1982, April). Security policies and security models. In 1982 IEEE Symposium on Security and Privacy (pp. 11–20). IEEE. https://doi.org/10.11 09/SP.1982.10014 Goldreich, O. (2008). Computational Complexity: A Conceptual Perspective. Cambridge University Press. Gonthier, G. (2008). The Four Colour Theorem: Engineering of a Formal Proof. In Computer Mathematics (pp. 333–333). Springer Berlin Heidelberg. https://doi.org/10.1 007/978-3-540-87827-8_28 Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., & Théry, L. (2013). A Machine-Checked Proof of the Odd Order Theorem. In Interactive Theorem Proving (pp. 163–179). Springer Berlin Heidelberg. https://do i.org/10.1007/978-3-642-39634-2_14 Grodin, H., Niu, Y., Sterling, J., & Harper, R. (2023, October). Decalf: A Directed, Effectful Cost-Aware Logical Framework (Version v2.0.0-rc.1). Zenodo. https://doi.org/10.5 281/zenodo.8423788 Grodin, H., Niu, Y., Sterling, J., & Harper, R. (2024). Decalf: A Directed, Effectful CostAware Logical Framework. Proceedings of the ACM on Programming Languages, 8(POPL), 273–301. https://doi.org/10.1145/3632852 Grosser, T. (2011, April). Enabling Polyhedral Optimizations in LLVM [Diploma Thesis]. Universität Passau. https://polly.llvm.org/publications/grosser-diploma-thesis.pdf Guéneau, A. (2019, December). Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. (Vérification mécanisée de la correction et complexité asymptotique de programmes) [PhD thesis]. Université de Paris. https://tel.archi ves-ouvertes.fr/tel-02437532 Guéneau, A., Charguéraud, A., & Pottier, F. (2018). A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In Programming Languages and Systems (pp. 533–560). Springer International Publishing. htt ps://doi.org/10.1007/978-3-319-89884-1_19 Gulwani, S., Mehra, K. K., & Chilimbi, T. (2009). SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 127–139. https://doi.org/10.1145/1480881.1480898 Hague, M., Jeż, A., & Lin, A. W. (2024). Parikh’s Theorem Made Symbolic. Proceedings of the ACM on Programming Languages,8(POPL), 1945–1977. https://doi.org/10 .1145/3632907 346 Hähnle, R., & Huisman, M. (2019). Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In Computing and Software Science (pp. 345–373). Springer International Publishing. https://doi.org/10.1007/978-3-319-91908-9_18 Hainry, E., Jeandel, E., Péchoux, R., & Zeyen, O. (2021). Complexityparser: An automatic tool for certifying poly-time complexity of Java programs. In A. Cerone & P. C. Ölveczky (Eds.), Theoretical Aspects of Computing – ICTAC 2021 (pp. 357–365). Springer International Publishing. https://doi.org/10.1007/978-3-030-85315-0_20 Hainry, E., Kapron, B., Marion, J.-Y., & Péchoux, R. (2024). Declassification Policy for Program Complexity Analysis. Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. https://doi.org/10.1145/3661814.3662100 Hainry, E., Kapron, B. M., Marion, J.-Y., & Péchoux, R. (2020). A tier-based typed programming language characterizing Feasible Functionals. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 535–549. https://do i.org/10.1145/3373718.3394768 Hainry, E., Marion, J.-Y., & Péchoux, R. (2013). Type-Based Complexity Analysis for Fork Processes. In Foundations of Software Science and Computation Structures (pp. 305–320). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-370 75-5_20 Hainry, E., & Péchoux, R. (2015). Objects in Polynomial Time. In Programming Languages and Systems (pp. 387–404). Springer International Publishing. https://doi.org/10.1 007/978-3-319-26529-2_21 Hainry, E., & Péchoux, R. (2018). A type-based complexity analysis of Object Oriented programs. Information and Computation,261, 78–115. https://doi.org/10.1016/j.ic .2018.05.006 Hainry, E., & Péchoux, R. (2023). A General Noninterference Policy for Polynomial Time. Proceedings of the ACM on Programming Languages,7(POPL), 806–832. https://d oi.org/10.1145/3571221 Hamann, T., Herda, M., Mantel, H., Mohr, M., Schneider, D., & Tasch, M. (2018a). A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode. In Secure IT Systems (pp. 437–453). Springer International Publishing. https://doi.o rg/10.1007/978-3-030-03638-6_27 Hamann, T., Herda, M., Mantel, H., Mohr, M., Schneider, D., & Tasch, M. (2018b). IFSPEC benchmark suite (Version 1.0) [Refactored and updated online arhive]. https://githu b.com/statycc/ifspec Hannay, J. E., MacLeod, C., Singer, J., Langtangen, H. P., Pfahl, D., & Wilson, G. (2009). How do scientists develop and use scientific software? 2009 ICSE Workshop on Software Engineering for Computational Science and Engineering, 1–8. https://doi .org/10.1109/secse.2009.5069155 Hedin, D., & Sabelfeld, A. (2012). A perspective on information-flow control. In Software safety and security (pp. 319–347). IOS Press. https://doi.org/10.3233/978-1-61499 -028-4-319 Heraud, S., & Nowak, D. (2011). A Formalization of Polytime Functions. In Interactive Theorem Proving (pp. 119–134). Springer Berlin Heidelberg. https://doi.org/10.10 07/978-3-642-22863-6_11 347 Heraud, S., & Nowak, D. (2018, September). The “BellantoniCook” formalization library (Version 1.0.0) [git rev de94ed6]. https://github.com/davidnowak/bellantonicook Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM,12(10), 576–580. https://doi.org/10.1145/363235.363259 Hoare, T. (2006). The Ideal of Verified Software. In Computer Aided Verification (pp. 5–16). Springer Berlin Heidelberg. https://doi.org/10.1007/11817963_4 Hoare, T., Misra, J., Leavens, G. T., & Shankar, N. (2021, October). The verified software initiative: A manifesto. In Theories of Programming: The Life and Works of Tony Hoare (pp. 81–92). ACM. https://doi.org/10.1145/3477355.3477361 Hoffmann, J., Aehlig, K., & Hofmann, M. (2012). Resource Aware ML. In P. Madhusudan & S. A. Seshia (Eds.), Computer Aided Verification (pp. 781–786). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_64 Hoffmann, J., Das, A., & Weng, S.-C. (2017). Towards automatic resource bound analysis for OCaml. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 359–373. https://doi.org/10.1145/3009837.3009842 Hoffmann, J., & Jost, S. (2022). Two decades of automatic amortized resource analysis. Mathematical Structures in Computer Science,32(6), 729–759. https://doi.org/10.1 017/s0960129521000487 Hoffmann, J., & Shao, Z. (2015). Automatic static cost analysis for parallel programs. In Programming languages and systems (pp. 132–157). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_6 Hofmann, M. (1999). Linear types and non-size-increasing polynomial time computation. Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 464–473. https://doi.org/10.1109/lics.1999.782641 Holewinski, J., Ramamurthi, R., Ravishankar, M., Fauzia, N., Pouchet, L.-N., Rountev, A., & Sadayappan, P. (2012). Dynamic trace-based analysis of vectorization potential of applications. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, 371–382. https://doi.org/10.1145/2254064 .2254108 Hritcu, C., Hughes, J., Pierce, B. C., Spector-Zabusky, A., Vytiniotis, D., Azevedo de Amorim, A., & Lampropoulos, L. (2013). Testing noninterference, quickly. Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, 455–468. https://doi.org/10.1145/2500365.2500574 Huang, W., Dong, Y., & Milanova, A. (2014). Type-Based Taint Analysis for Java Web Applications. In Fundamental Approaches to Software Engineering (pp. 140–154). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-54804-8_10 Ileri, A. M., Zeldovich, N., Chlipala, A., & Kaashoek, F. (2024). Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism. 2024 IEEE 37th Computer Security Foundations Symposium (CSF), 96–111. https://doi .org/10.1109/csf61375.2024.00041 Intel Corporation. (2022). Intel C++ Compiler Classic Developer Guide and Reference [Accessed: 2025-06-23]. https://www.intel.com/content/dam/develop/external/us/e n/documents/cpp_compiler_classic.pdf 348 Jones, N. D. (1999). LOGSPACE and PTIME characterized by programming languages. Theoretical Computer Science,228(1–2), 151–174. https://doi.org/10.1016/s03043975(98)00357-0 Jones, N. D. (2001). The expressive power of higher-order types or, life without CONS. Journal of Functional Programming,11(1), 55–94. https://doi.org/10.1017/s09567 96800003889 Jones, N. D., & Kristiansen, L. (2009). A flow calculus of mwp-bounds for complexity analysis. ACM Transactions on Computational Logic,10(4), 28:1–28:41. https://do i.org/10.1145/1555746.1555752 Jones, N. D., & Nielson, F. (1995). Abstract Interpretation: A Semantics-Based Tool for Program Analysis. In S. Abramsky, D. M. Gabbay, & T. S. E. Maibaum (Eds.), Semantic Modelling (pp. 527–636, Vol. 4). Oxford University Press. https://doi.org/1 0.1093/oso/9780198537809.003.0005 Joppa, L. N., McInerny, G., Harper, R., Salido, L., Takeda, K., O’Hara, K., Gavaghan, D., & Emmott, S. (2013). Troubling trends in scientific software use. Science,340(6134), 814–815. https://doi.org/10.1126/science.1231535 Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., & Pichardie, D. (2015). A formally-verified C static analyzer. ACM SIGPLAN Notices,50(1), 247–259. https://doi.org/10.1145 /2775051.2676966 Kaminski, B. (2025, March). Ina Schaefer on X-by-Construction [Accessed: 2025-04-27]. https://etaps.org/blog/031-ina-schaefer/ ETAPS Blog, Published on 25 March 2025. Kammüller, F. (2008). Formalizing non-interference for a simple bytecode language in Coq. Formal Aspects of Computing,20(3), 259–275. https://doi.org/10.1007/s00165-00 7-0055-2 Karbyshev, A., Svendsen, K., Askarov, A., & Birkedal, L. (2018). Compositional Noninterference for Concurrent Programs via Separation and Framing. In Principles of Security and Trust (pp. 53–78). Springer International Publishing. https://doi.org/1 0.1007/978-3-319-89722-6_3 Karp, R. M., Miller, R. E., & Winograd, S. (1967). The Organization of Computations for Uniform Recurrence Equations. Journal of the ACM,14(3), 563–590. https://doi.or g/10.1145/321406.321418 Karr, M. (1976). Affine relationships among variables of a program. Acta Informatica,6(2), 133–151. https://doi.org/10.1007/BF00268497 Keidel, S. (2021, March). Modular Specification and Compositional Soundness of Abstract Interpreters [Doctoral dissertation, Johannes Gutenberg-Universität Mainz]. https: //doi.org/10.25358/openscience-6384 Kennedy, K., & Allen, J. R. (2001). Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann Publishers Inc. KoAT2 Developers. (2024, February). KoAT2 (Version koat2-twn-journal) [git rev 9c511e3]. https://github.com/aprove-developers/KoAT2-Releases Kristiansen, L. (2005). Neat function algebraic characterizations of logspace and linspace. Computational Complexity,14(1), 72–88. https://doi.org/10.1007/s00037-005-019 1-0 349 Kristiansen, L. (2017, April). On Resource Analysis of Imperative Programs†[Accessed: 2025-01-06]. Presentation slides at DICE-FOPARA 2017, Uppsala, Sweden. Kristiansen, L., & Jones, N. D. (2005). The Flow of Data and the Complexity of Algorithms. In S. B. Cooper, B. Löwe, & L. Torenvliet (Eds.), New Computational Paradigms (pp. 263–274, Vol. 3526). Springer Berlin Heidelberg. https://doi.org/10.1007/114 94645_33 Lafont, Y. (2004). Soft linear logic and polynomial time. Theoretical Computer Science, 318(1), 163–180. https://doi.org/10.1016/j.tcs.2003.10.018 Laird, J., Manzonetto, G., McCusker, G., & Pagani, M. (2013). Weighted Relational Models of Typed Lambda-Calculi. 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 301–310. https://doi.org/10.1109/LICS.2013.36 Lamba, A., Taylor, M., Beardsley, V., Bambeck, J., Bond, M. D., & Lin, Z. (2024). Cocoon: Static Information Flow Control in Rust. Proceedings of the ACM on Programming Languages,8(OOPSLA1), 166–193. https://doi.org/10.1145/3649817 Lamport, L. (1977). Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering,SE-3(2), 125–143. https://doi.org/10.1109/tse.1977.2299 04 Lattner, C., & Adve, V. S. (2004). LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. International Symposium on Code Generation and Optimization, 2004. CGO 2004., 75–88. https://doi.org/10.1109/CGO.2004.1281665 Lawson, N. (2009). Side-channel attacks on cryptographic software. IEEE Security & Privacy Magazine,7(6), 65–68. https://doi.org/10.1109/msp.2009.165 Lee, C. S., Jones, N. D., & Ben-Amram, A. M. (2001). The size-change principle for program termination. Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 81–92. https://doi.org/10.1145/360204.360 210 Leino, K. R. M. (2008). This is boogie 2 (Technical report). Microsoft. https://www.micro soft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf Leino, K. R. M. (2010a). Dafny: An automatic program verifier for functional correctness. Logic for Programming, Artificial Intelligence, and Reasoning, 348–370. https://do i.org/10.1007/978-3-642-17511-4_20 Leino, K. R. M. (2010b, April). Dafny An automatic program verifier for functional correctness†[Accessed: 2025-04-14]. https://www.microsoft.com/en-us/research/p ublication/dafny-automatic-program-verifier-functional-correctness/ Presentation slides of LPAR-16, on 27 April 2010. Leino, K. R. M. (2023). Program proofs. The MIT Press. Leivant, D. (1993). Stratified functional programs and computational complexity. In M. S. Van Deusen & B. Lang (Eds.), Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’93 (pp. 325–333). ACM Press. https://doi.org/10.1145/158511.158659 Leivant, D., & Marion, J.-Y. (1995). Ramified recurrence and computational complexity II: Substitution and poly-space. In Computer Science Logic (pp. 486–500). Springer Berlin Heidelberg. https://doi.org/10.1007/bfb0022277 350 Leivant, D., & Marion, J.-Y. (2013). Evolving Graph-Structures and Their Implicit Computational Complexity. In Automata, Languages, and Programming (pp. 349–360). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39212-2_32 Leroy, X. (2009). Formal verification of a realistic compiler. Communications of the ACM, 52(7), 107–115. https://doi.org/10.1145/1538788.1538814 Leroy, X. (2018). Le logiciel, entre l’esprit et la matière [Accessed: 2025-06-30]. https://w ww.college-de-france.fr/fr/agenda/lecon-inaugurale/le-logiciel-entre-esprit-et-lamatiere/le-logiciel-entre-esprit-et-la-matiere Lecture notes of Collège de France, 15 Novembre 2018. Leveson, N., & Turner, C. (1993). An investigation of the Therac-25 accidents. Computer, 26(7), 18–41. https://doi.org/10.1109/mc.1993.274940 Levin, L. A. (1973). Universal sequential search problems [English translation]. Problems of Information Transmission,9(3), 265–266. Lichtman, B., & Hoffmann, J. (2017). Arrays and References in Resource Aware ML. In D. Miller (Ed.), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (26:1–26:20, Vol. 84). Schloss Dagstuhl - LeibnizZentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSCD.2017.26 Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J. N., Chang, B.-Y. E., Guyer, S. Z., Khedker, U. P., Møller, A., & Vardoulakis, D. (2015). In defense of soundiness: a manifesto. Communications of the ACM,58(2), 44–46. https://doi.or g/10.1145/2644805 LLVM project contributors. (2020). Loop Fission Interference Graph (FIG) [Accessed: 2025-06-23]. https://reviews.llvm.org/D73801 LLVM project contributors. (2025, May). LLVM Loop Terminology (and Canonical Forms) – LLVM Compiler Infrastructure (Version last updated on 2025-05-06) [Accessed: 2025-03-06]. Technical documentation. LLVM Project. https://llvm.org/docs/Loop Terminology.html Lommen, N., & Giesl, J. (2023). Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs. In Frontiers of Combining Systems (pp. 3–22). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-43369-6_1 Mahboubi, A., & Tassi, E. (2022, September). Mathematical Components. Zenodo. https: //doi.org/10.5281/zenodo.7118596 Marion, J.-Y. (2011). A Type System for Complexity Flow Analysis. 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 123–132. https://doi.org/10.1109/lics.2 011.41 Marion, J.-Y., & Moyen, J.-Y. (2000). Efficient First Order Functional Program Interpreter with Time Bound Certifications. In Logic for Programming and Automated Reasoning (pp. 25–42). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-444041_3 Mars Climate Orbiter Mishap Investigation Board. (1999). Mars Climate Orbiter Mishap Investigation Board, Phase I Report, November 10, 1999 (Technical report). NASA. https://llis.nasa.gov/llis_lib/pdf/1009464main1_0641-mr.pdf Mastroeni, I., & Pasqua, M. (2019). Statically analyzing information flows: an abstract interpretation-based hyperanalysis for non-interference. Proceedings of the 34th 351 ACM/SIGAPP Symposium on Applied Computing, 2215–2223. https://doi.org/10.1 145/3297280.3297498 Mathematical Components development team. (2024, December). The Mathematical Components Library (Version 2.3.0). https://github.com/math-comp/math-comp McCarthy, J. A., Fetscher, B., New, M. S., Feltey, D., & Findler, R. B. (2018). A Coq library for internal verification of running-times. Science of Computer Programming,164, 49–65. https://doi.org/10.1016/j.scico.2017.05.001 Mehta, S., Lin, P., & Yew, P. (2014). Revisiting loop fusion in the polyhedral framework. In J. E. Moreira & J. R. Larus (Eds.), Proceedings of the 19th ACM SIGPLAN symposium on Principles and practice of parallel programming (pp. 233–246). ACM. https://doi.org/10.1145/2555243.2555250 Meyer, B. (1988). Object-oriented software construction (Vol. 1). Prentice Hall International. Microsoft. (2025, March). Boogie (Version 3.5.1). https://github.com/boogie-org/boogie Mogbil, V. (2012, November). Complexité en logique linéaire, et logique linéaire en complexité implicite [Habilitation à diriger des recherches en informatique (HDR)]. Université Paris XIII. http://lipn.univ-paris13.fr/~mogbil/hdr/mogbil-hdr-memoire.pdf Molina, F., Ponzio, P., Aguirre, N., & Frias, M. (2021). EvoSpex: An Evolutionary Algorithm for Learning Postconditions. 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), 1223–1235. https://doi.org/10.1109/ICSE43902 .2021.00112 Møller, A. (2024, August). Static Program Analysis†[Accessed: 2025-02-08]. Lecture notes from Marktoberdorf Summer School 2024, Herrsching am Ammersee, Germany. Møller, A., & Schwartzbach, M. I. (2024). Static Program Analysis. Department of Computer Science, Aarhus University. https://cs.au.dk/~amoeller/spa/spa.pdf Montoya, A. F. (2017a). Cost Analysis of Programs Based on the Refinement of Cost Relations [PhD thesis]. Technische Universität Darmstadt. http://tuprints.ulb.tu-darmsta dt.de/6746/ Montoya, A. F. (2017b). Experimental evaluation of Cost Analysis of Programs Based on the Refinement of Cost Relations [Accessed: 2025-03-08]. https://aeflores.github.i o/CoFloCo/experimentsPhD Montoya, A. F. (2017c). Experimental evaluation of Cost Analysis of Programs Based on the Refinement of Cost Relations [Accessed: 2025-09-15]. https://aeflores.github.i o/CoFloCo/experimentsPhD/ Results of the experimental evaluation performed in the PhD thesis. Moser, G., & Schneckenreither, M. (2018). Automated amortised resource analysis for term rewrite systems. Functional and Logic Programming (FLOPS 2018), 214–229. http s://doi.org/10.1007/978-3-319-90686-7_14 Moyen, J.-Y. (2017, February). Implicit Complexity in Theory and Practice [Habilitation à Diriger des Recherches (HDR)]. University of Copenhagen. https://lipn.univ-paris 13.fr/~moyen/papiers/Habilitation_JY_Moyen.pdf Moyen, J.-Y., & Rubiano, T. (2016, April). Detection of Non-Size Increasing Programs in Compilers [At Developments in Implicit Computational Complexity (DICE 2016)]. https://lipn.univ-paris13.fr/DICE2016/Abstracts/paper_2.pdf 352 Moyen, J.-Y., Rubiano, T., & Seiller, T. (2017a). Loop Quasi-Invariant Chunk Detection. In Automated Technology for Verification and Analysis (pp. 91–108). Springer International Publishing. https://doi.org/10.1007/978-3-319-68167-2_7 Moyen, J., Rubiano, T., & Seiller, T. (2017b). Loop Quasi-Invariant Chunk Motion by peeling with statement composition. In G. Bonfante & G. Moser (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 47–59, Vol. 248). Open Publishing Association. https://doi.org/10.4204/EPTCS.248.9 Müller, P. (2024, August). Ownership in program verification – from separation logic to Rust and back†[Accessed: 2025-04-19]. Lecture notes from Marktoberdorf Summer School 2024, Herrsching am Ammersee, Germany. Myers, A. C. (1999). JFlow: practical mostly-static information flow control. Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 228–241. https://doi.org/10.1145/292540.292561 Nelson, L., Bornholt, J., Krishnamurthy, A., Torlak, E., & Wang, X. (2020). Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review,54(1), 31–39. https://doi.org/10.1145/3421473.3421478 Ngo, V. C., Carbonneaux, Q., & Hoffmann, J. (2018). Bounded Expectations: Resource Analysis for Probabilistic Programs. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 496–512. https://d oi.org/10.1145/3192366.3192394 Nguyen, T., Antonopoulos, T., Ruef, A., & Hicks, M. (2017). Counterexample-guided approach to finding numerical invariants. Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 605–615. https://doi.org/10.1145/310623 7.3106281 Nguyen, T., Kapur, D., Weimer, W., & Forrest, S. (2014). DIG: A dynamic invariant generator for polynomial and array invariants. ACM Transactions on Software Engineering and Methodology (TOSEM),23(4), 1–30. https://doi.org/10.1145/2556782 Nguyen, T., Nguyen, K., & Duong, H. (2022). SymInfer: inferring numerical invariants using symbolic states. Proceedings of the ACM/IEEE 44th International Conference on Software Engineering: Companion Proceedings, 197–201. https://doi.org/10.11 45/3510454.3516833 Nielson, F., Nielson, H. R., & Hankin, C. (2010). Principles of program analysis. Springer. Niggl, K.-H., & Wunderlich, H. (2006). Certifying Polynomial Time and Linear/Polynomial Space for Imperative Programs. SIAM Journal on Computing,35(5), 1122–1147. h ttps://doi.org/10.1137/s0097539704445597 Niu, Y., Sterling, J., Grodin, H., & Harper, R. (2022). A cost-aware logical framework. Proceedings of the ACM on Programming Languages,6(POPL), 1–31. https://doi.org /10.1145/3498670 Ölveczky, P. C. (2017). Designing Reliable Distributed Systems. Springer London. https://d oi.org/10.1007/978-1-4471-6687-0 oneTBB Contirbutors. (2025, March). oneAPI Threading Building Blocks (oneTBB) (oneTBB 2022.1.0) [Accessed: 2025-03-09]. Technical documentation. Intel. https://uxlfoundation.github.io/oneTBB 353 OpenMP Architecture Review Board. (2024, November). OpenMP Application Programming Interface (Version 6.0 November 2024) [Accessed: 2025-03-08]. API documentation. OpenMP Architecture Review Board. https://www.openmp.org/wp-con tent/uploads/OpenMP-API-Specification-6-0.pdf Palkowski, M., Klimek, T., & Bielecki, W. (2015). TRACO: An automatic loop nest parallelizer for numerical applications. In M. Ganzha, L. A. Maciaszek, & M. Paprzycki (Eds.), Proceedings of the 2015 Federated Conference on Computer Science and Information Systems (pp. 681–686, Vol. 5). IEEE. https://doi.org/10.15439/2015F34 Patrignani, M., & Garg, D. (2017). Secure Compilation and Hyperproperty Preservation. 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 392–404. http s://doi.org/10.1109/csf.2017.13 Péchoux, R. (2020, December). Complexité implicite : bilan et perspectives [Habilitation à Diriger des Recherches (HDR)]. Université de Lorraine. https://hal.univ-lorraine.fr /tel-02978986v3/file/HDR-RP.pdf Pierce, B. C., Azevedo de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., Tolmach, A., & Yorgey, B. (2024). Programming Language Foundations (B. C. Pierce, Ed.; Version 6.7, Vol. 2). https://softwarefoundations.ci s.upenn.edu/plf-current/index.html Pierce, B. C., Azevedo de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., & Yorgey, B. (2025). Logical Foundations (B. C. Pierce, Ed.; Version 6.7, Vol. 1). https://softwarefoundations.cis.upenn.edu/lf-current/inde x.html Piessens, F. (2024, August). Software security across abstraction layers†[Accessed: 202502-15]. Lecture notes from Marktoberdorf Summer School 2024, Herrsching am Ammersee, Germany. Popeea, C., & Chin, W.-N. (2007). Inferring Disjunctive Postconditions. Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 331–345. https: //doi.org/10.1007/978-3-540-77505-8_26 Popeea, C., & Chin, W.-N. (2010). Dual analysis for proving safety and finding bugs. Proceedings of the 2010 ACM Symposium on Applied Computing, 2137–2143. https://d oi.org/10.1145/1774088.1774538 Pophale, S. (2023). Introduction to OpenMP Offload: Part I [Accessed: 2025-03-08]. https: //www.olcf.ornl.gov/wp-content/uploads/OpenMP_Introduction_to_Offload_Part 1.pdf OpenMP training series at the National Energy Research Scientific Computing Center (NERSC). Pouchet, L.-N., & Yuki, T. (2016, February). PolyBench/C 4.2 (Version 4.2). https://source forge.net/projects/polybench/files/ Prema, S., Nasre, R., Jehadeesan, R., & Panigrahi, B. (2019). A study on popular autoparallelization frameworks. Concurrency and Computation: Practice and Experience,31(17), e5168. https://doi.org/10.1002/cpe.5168 Pugh, W. (1991). The Omega test: a fast and practical integer programming algorithm for dependence analysis. Proceedings of the 1991 ACM/IEEE conference on Supercomputing - Supercomputing ’91, 4–13. https://doi.org/10.1145/125826.125848 354 7 Additional Published Manuscripts 361 7.1 mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity IJImplicit computational complexity & static analysis Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller The 7th International Conference on Formal Structures for Computation and Deduction (FSCD), 2022 “mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity” © by Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller. This work is licensed under a Creative Commons Attribution 4.0 International License. You should have received a copy of the license along with this work. If not, see https://creativecommons.org/licenses/by/4.0/. 362 mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity Clément Aubert #Ñ School of Computer and Cyber Sciences, Augusta University, GA, USA Thomas Rubiano #Ñ LIPN – UMR 7030 Université Sorbonne Paris Nord, France Neea Rusch #Ñ School of Computer and Cyber Sciences, Augusta University, GA, USA Thomas Seiller #Ñ LIPN – UMR 7030 Université Sorbonne Paris Nord, France CNRS, Paris, France Abstract Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis [ 23 ] certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper’s contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it. 2012 ACM Subject Classification Software and its engineering → Automated static analysis; Theory of computation →Complexity theory and logic; Theory of computation →Logic and verification Keywords and phrases Static Program Analysis, Implicit Computational Complexity, Automatic Complexity Analysis, Program Verification Digital Object Identifier 10.4230/LIPIcs.FSCD.2022.26 Related Version Technical report:https://hal.archives-ouvertes.fr/hal-03596285 [4] Supplementary Material Software (Source Code):https://github.com/statycc/pymwp archived at swh:1:dir:22a4ab0cfad49138981ed25fc2abfe830fb7ccdf Software (Documentation and Demo):https://statycc.github.io/pymwp Funding This research is supported by the Th. Jefferson Fund of the Embassy of France in the United States and the FACE Foundation, and has benefited from the research meeting 21453 “Static Analyses of Program Flows: Types and Certificate for Complexity” in Schloss Dagstuhl. Th. Rubiano and Th. Seiller are supported by the Île-de-France region through the DIM RFSI project “CoHOp”. Acknowledgements The authors wish to express their gratitude to Assya Sellak for her contribution to this work, to the reviewers of previous versions for their comments, and to the FSCD community: in particular, the reviews we received were extremely interesting, and generated new directions and questions, for which we are thankful. ©Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller; licensed under Creative Commons License CC-BY 4.0 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Editor: Amy P. Felty; Article No. 26; pp. 26:1–26:23 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 363 26:2 mwp-Analysis Improvement and Implementation: Realizing Implicit Complexity 1 Introduction: letting ICC drive the development of static analyzers Certifying program resource usages is possibly as crucial as the specification of program correctness, since a guaranteed correct program whose memory usage exceeds available resources is, in fact, unreliable. The field of Implicit Computational Complexity (ICC) theory [ 15 ] pioneers in “embedding” in the program itself a guarantee of its resource usage, using e.g., bounded recursion [ 8 , 27 ] or type systems [ 6 , 26 ]. This field initiated numerous distinct and original approaches, primarily to characterize complexity classes in a machineindependent way, with increasing expressivity, but these approaches have rarely materialized into concrete programming languages or program analyzers: even if, as opposed to traditional complexity, its models are generally expressive enough to write down actual algorithms [ 30 , p. 11], they rarely escape the sphere of academia or extend beyond toy languages, with a few exceptions [ 5 , 22 ]. However, by abstracting away constant factors and insignificant orders of magnitude, it is frequently conjectured that ICC will allow sidestepping some of the difficult issues one usually has to face when inferring the resource usage of a concrete program. This work reinforces this conjecture by adjusting, improving and implementing an existing ICC technique, the mwp-bounds analysis [ 23 ], which certifies that the values computed by an imperative program will be bounded by polynomials in the program’s input. This flow analysis is elegant but computationally costly, and it missed an opportunity to leverage its built-in compositionality: we address both issues by revisiting and expanding the original flow calculus, and further make our point by implementing it on a subset of the C programming language. While the theory has been improved to allow analysis of function definitions and calls – including recursive ones, a feature not widely supported [ 21 , p. 359] – , its integration into the implementation is underway, as we placed primary focus on developing an efficient and implementable technique for program analysis. Implementing a tool along the theory enabled testing improvements in real-life, which in return drove adjustments to the theory. Our enhanced technique answers positively two questions asked by the authors of the original analysis [23, Section 1.2], namely 1. Can the method be extended to richer languages? 2. Can it lead to powerful and convenient tools? It also supports the conjecture that ICC can be used to construct concrete tools, but highlights that doing so requires adjusting the theory to make it tractable in practice. This work also provides better insight into the original analysis, by e.g., separating the algorithm to decide the existence of a bound from its evaluation into a concrete bound; and by illustrating its plasticity: while our analysis conservatively extends the original one, it nevertheless greatly alters its internal machinery to ease its implementability. Last but not least, our technique is orthogonal to most static analysis methods, which focus on worst-case resource-usage complexity or termination, while ours establishes that the growth rate of variables values is at most polynomially related to their inputs. Our paper starts by recalling the “original” mwp-bounds analysis [ 23 ] – to which we refer for a more gentle introduction – and discuss its limitations (Sect. 2). In Sect. 3, we motivate, introduce and justify two modifications to this original analysis, and state that this calculus can be reduced to the original one. We then extend this analysis along two axis (Sect. 4): we detail how functions calls can be analyzed, and how the structures we implemented allowed to speed up some very costly operations. Finally, Sect. 5 presents and discuss our implementation, and Sect. 6 concludes. The proofs, some additional details on semi-rings and the detail of our benchmarks are in appendix, with the exception of some tedious proofs relative to semi-rings that are only in our technical report [4]. 364 C. Aubert, T. Rubiano, N. Rusch, and T. Seiller 26:3 2 Background: the original flow analysis The original analysis [ 23 ] computes a polynomial bound – if it exists – on the sizes (of the value itself) of variables in an imperative while programming language, extended with a loop operator, by computing for each variable a vector that tracks how it depends on other variables – and the program itself gets assigned a matrix collecting those vectors. While this does not ensure termination, it provides a certificate guaranteeing that the program uses throughout its execution at most a polynomial amount of space, and as a consequence that if it terminates, it will do so in polynomial time. 2.1 Language analyzed: fragments of imperative language ▶ Definition 1 (Imperative Language).Letting natural number variables range over X and Y and boolean expressions over b, we define expressions eand commands Cas follows: e:=X∥X-Y∥X+Y∥X*Y C:=X=e∥if bthen Celse C∥while bdo {C} ∥loop X {C} ∥C;C where loop X {C} means “do C X times” and C;C is used for sequentiality (“do C , then C ”). We write “program” for a series of commands composed sequentially. This language assumes that the program’s inputs are the only variables, and that assigning a value to a variable inside the program is not permitted. Extending flow calculi to those operations has been discussed [ 23 , p. 3] and proven possible [ 9 ], but we leave this for future work – in particular, our C examples will be of foo functions with their variables listed as parameters 1 . However, we disallow w.l.o.g. composed expressions of the form X+Y*Y , which can always be dealt with in the style of three-address code. 2.2 A flow calculus of mwp-bounds for complexity analysis Flows characterize controls from one variable to another, and can be, in increasing growth rate, of type 0– the absence of any dependency – maximum, weak polynomial and polynomial. The bounds on programs written in the syntax of Sect. 2.1 are represented and calculated thanks to vectors and matrices whose coefficients are elements of the mwp semi-ring. ▶ Definition 2 (The mwp semi-ring and matrices over it).Letting mwp = { 0, m , w , p} with 0 < m < w < p , and α , β , γ range over mwp, the mwp semi-ring ( mwp , 0, m , +, × )is defined with + = max,α×β= max(α,β)if α,β= 0, and 0otherwise. We denote M ( mwp )the matrices over mwp, and, fixing n∈N , M for n×n matrices over mwp, Mij for the coefficient in the i th row and j th column of M , ⊕ for the componentwise addition, and ⊗ for the product of matrices defined in a standard way. The 0-element for addition is 0 ij = 0 for all i , j , and the 1-element for product is 1 ii = m ,1 ij = 0 if i = j , and the resulting structure ( M ( mwp ), 0, 1, ⊗ , ⊕ )is a semi-ring that we simply write M ( mwp ). The closure operator ·∗is M∗= 1 ⊕M⊕(M2)⊕. . ., for M0= 1,Mm+1 =M⊗Mm. 1 Our implementation allows to relax this condition, as exemplified in inline_variable.c , without losing any of the results expressed in this paper. Assuming a fixed number of variables, known ahead of time, is mostly a theoretical artifact used to simplify the analysis. FSCD 2022 365 26:4 mwp-Analysis Improvement and Implementation: Realizing Implicit Complexity E1 ⊢jk Xi :{m i}E2 ⊢jk e:{w i|Xi ∈var(e)} ⊢jk Xi :V1⊢jk Xj :V2 ⋆∈ {+, −} E3 ⊢jk Xi⋆Xj :pV1⊕V2 ⊢jk Xi :V1⊢jk Xj :V2 ⋆∈ {+, −} E4 ⊢jk Xi⋆Xj :V1⊕pV2 (a) Rules for assigning vectors to expressions. ⊢jk e:VA ⊢jk Xj = e : 1 j ←− V ⊢jk C1 :M1⊢jk C2 :M2C ⊢jk C1; C2 :M1⊗M2 ⊢jk C1 :M1⊢jk C2 :M2I ⊢jk if bthen C1 else C2 :M1⊕M2 ⊢jk C:M ∀i,M∗ ii =mL ⊢jk loop Xl {C} :M∗⊕ {p l→j| ∃i,M∗ ij =p} ⊢jk C:M ∀i,M∗ ii =mand ∀i,j,M∗ ij =pW ⊢jk while bdo {C} :M∗ (b) Rules for assigning matrices to commands. Figure 1 Original non-deterministic (“Jones-Kristiansen”) flow analysis rules. Although not crucial to understand our development, details about (strong) semi-rings and the mwp semi-ring, and the construction of a semi-ring whose elements are matrices with coefficients in a semi-ring – so, in particular, M ( mwp )– are given in our technical report [ 4 , A.1 and A.2] and sketched in appendix Appendix A. Below, we let V1 , V2 be column vectors with values in mwp, αV1 be the usual scalar product, and V1⊕V2 be defined componentwise. We write {α i} for the vector with 0 everywhere except for αin its ith row, and {α i,β j}for {α i}⊕{β j}. Replacing in a matrix M the j th column vector by V is denoted Mj ←− V . The matrix M with Mij = α and 0everywhere else is written {α i→j} , and the set of variables in the expression e is written var ( e ). The assumption is made that exactly n different variables are manipulated throughout the analyzed program, so that n -vectors are assigned to expressions – in a non-deterministic way, to capture larger classes of programs [ 23 , Section 8] – and n×n matrices are assigned to commands using the rules presented Fig. 1 [23, Section 5]. The intuition is that if ⊢jk C : M can be derived, then all the values computed by C will grow at most polynomially w.r.t. its inputs [ 23 , Theorem 5.3], e.g., will be bounded by max ( x , p1 ( y )) + p2 ( z ), where p1 and p2 are polynomials and x (resp. y , z ) are m -(resp. w -, p -)annotated variables in the vector for the considered output. Since the derivation system is non-deterministic, multiple matrices and polynomial bounds – that sometimes coincide – may be assigned to the same program. Furthermore, the coefficient at Mij carries quantitative information about the way Xi depends on Xj , knowing that 0and m -flows are harmless and without constraints, but that w - and p - flows are more harmful w.r.t. polynomial bounds and need to be handled with care, particularly in loops – hence the condition on the L and W rules. The derivation may fail – some programs may not be assigned a matrix – if at least one of the variables used in the body of a loop depends “too strongly” upon another, making it impossible to ensure polynomial bounds on the loop itself. We will use the following example as a common basis to discuss possible failure, non-determinism, and our improvements. 366 [Document text truncated for crawler view.]