
arXiv: 2203.03943
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 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 threefold: 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.
Program Verification, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Implicit Computational Complexity, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Formal Languages and Automata Theory (cs.FL), Computer Science - Formal Languages and Automata Theory, Mathematics - Logic, 004, Automatic Complexity Analysis, Logic in Computer Science (cs.LO), Static Program Analysis, Complexity theory and logic, Logic and verification phrases Static Program Analysis, FOS: Mathematics, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Logic (math.LO), 2012 ACM Subject Classification Automated static analysis, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], ddc: ddc:004
Program Verification, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Implicit Computational Complexity, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Formal Languages and Automata Theory (cs.FL), Computer Science - Formal Languages and Automata Theory, Mathematics - Logic, 004, Automatic Complexity Analysis, Logic in Computer Science (cs.LO), Static Program Analysis, Complexity theory and logic, Logic and verification phrases Static Program Analysis, FOS: Mathematics, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Logic (math.LO), 2012 ACM Subject Classification Automated static analysis, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
