Abstract:
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in the interactive theorem prover ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. Note that ACL2s is a flavor of ACL2, with a type system, termination analysis based on context-calling graphs, and counterexample generation. One key component in our RTO analysis was proving in ACL2s that for all a ∈ [0, 1), the limit as n→∞ of aⁿ is zero. Whereas the most obvious proof strategy involves the logarithm, whose codomain includes irrationals, by default ACL2 only supports rationals, which forced us to take a non-standard approach. In this paper, we explore different approaches to proving the above result in ACL2(r), a flavor of ACL2 that supports real numbers, and ACL2s, from the perspective of a relatively new user to each. We also contextualize the theorem by showing how it allowed us to prove important asymptotic properties of the RTO computation. Finally, we discuss tradeoffs between the various proof strategies and directions for future research.
The presentation will not assume any prior knowledge about real analysis or the ACL2 prover ecosystem.
Bio:
Max von Hippel is a 5th year PhD student in Computer Science and NSF GRFP fellow at Northeastern University, advised by Cristina Nita-Rotaru. His research focuses on the verification of, and automated synthesis of attacks against, network protocols. Before graduate school, Max completed a BS in pure mathematics at the University of Arizona, with a minor in CS; and before that, a bilingual IB diploma at the United World College Costa Rica, with a Shelby Davis scholarship. Max grew up in Anchorage, Alaska.