Forschungstreffen 21453
Static Analyses of Program Flows: Types and Certificate for Complexity
( 07. Nov – 12. Nov, 2021 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/21453
Organisator
- Clément Aubert (Augusta University, US)
Kontakt
- Heike Clemens (für administrative Fragen)
Externe Veranstaltungsseite
Impacts
- mwp-Analysis Improvement and Implementation : Realizing Implicit Computational Complexity : article in FSCD 2022 - Aubert, Clement; Rubiano, Thomas; Rusch, Neea; Seiller, Thomas - Wadern : LZI, 2022. - pp. 1-23 - (Leibniz International Proceedings in Informatics ; 228).
- Formally Verified Resource Bounds through Implicit Computational Complexity : article in SPLASH Companion 2022: Companion Proceedings of the 2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity - Rusch, Neea - New York : ACM, 2022. - 4 pp..
- Distributing and Parallelizing Non-canonical Loops : article in VMCAI 2023: Verification, Model Checking, and Abstract Interpretation - Aubert, Clement; Rubiano, Thomas; Rusch, Neea; Seiller, Thomas - Berlin : Springer, 2023. - 24 pp. - (Lecture notes in computer science ; 13881 : article).
- pymwp : A Static Analyzer Determining Polynomial Growth Bounds : article in ATVA 2023 : Automated Technology for Verification and Analysis - Aubert, Clement; Rubiano, Thomas; Rusch, Neea; Seiller, Thomas - Berlin : Springer, 2023. - pp. 263–275 - (Lecture notes in computer science ; 14216 : article).
The StATyCC ("Static Analyses of Program Flows: Types and Certificate for Complexity") project aims at providing new static analysis tools based on theoretical results from implicit computational complexity.It revolves around certified, compositional analysis of source code or intermediate representation, insuring that computer programs have a reasonable (i.e., polynomial) growth with respect to their input's size. A first implementation has been established, our main goal will now be to port it to intermediate representations of certified compilers, providing one of the first certified and compositional static analysis tool.
This research is supported by the Thomas Jefferson Fund (https://face-foundation.org/higher-education/thomas-jefferson-fund/) of the Embassy of France in the United States and the FACE Foundation (https://face-foundation.org/)
Creative Commons BY 3.0 DE
Clément Aubert
