Formally Verified Resource Bounds through Implicit Computational ComplexityIn Person
Automatic complexity analysis has not reached mainstream adoption due to outstanding challenges, such as scalability and usability, and no formally verified analyzer exists. However, the need to evaluate resource usage is crucial: even a guaranteed correct program, whose memory usage exceeds available resources, is unreliable. The field of Implicit Computational Complexity (ICC) offers a potential avenue to resolving some of these outstanding challenges by introducing unique, machine-independent, and flexible approaches to program analysis. But since ICC techniques are mostly theoretical, it is unclear how strongly these assumptions hold in practice. This project defines a 3-directional plan—focused on practical analysis, compiler-integration, and formal verification—to assess the suitability of ICC to address outstanding challenges in automatic complexity analysis.
Tue 6 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mTalk | Towards a Verified Cost Model for Call-by-Push-ValueIn Person Doctoral Symposium Zhuo Chen University of Melbourne DOI | ||
11:00 30mTalk | Formally Verified Resource Bounds through Implicit Computational ComplexityIn Person Doctoral Symposium Neea Rusch Augusta University DOI | ||
11:30 30mTalk | Proving Obliviousness of Probabilistic Algorithms with Formal VerificationIn Person Doctoral Symposium Pengbo Yan University of Melbourne DOI |