1 Search Results for "Rubiano, Thomas"

Document
DOI: 10.4230/LIPIcs.FSCD.2022.26
mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

Authors: Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

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 [Jones and Lars Kristiansen, 2009] 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.
Cite as

Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aubert_et_al:LIPIcs.FSCD.2022.26,
  author =	{Aubert, Cl\'{e}ment and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
  title =	{{mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{26:1--26:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.26},
  URN =		{urn:nbn:de:0030-drops-163071},
  doi =		{10.4230/LIPIcs.FSCD.2022.26},
  annote =	{Keywords: Static Program Analysis, Implicit Computational Complexity, Automatic Complexity Analysis, Program Verification}
}
  • Refine by Author
  • 1 Aubert, Clément
  • 1 Rubiano, Thomas
  • 1 Rusch, Neea
  • 1 Seiller, Thomas

  • Refine by Classification
  • 1 Software and its engineering → Automated static analysis
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Automatic Complexity Analysis
  • 1 Implicit Computational Complexity
  • 1 Program Verification
  • 1 Static Program Analysis

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact