A Case Study in Analytic Protocol Analysis in ACL2

Max von Hippel
(Northeastern University)
Panagiotis Manolios
(Northeastern University)
Kenneth L. McMillan
(University of Texas at Austin)
Cristina Nita-Rotaru
(Northeastern University)
Lenore Zuck
(University of Illinois Chicago)

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 ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. One key component in our RTO computation analysis was proving in ACL2s that for all alpha in [0, 1), the limit as n approaches infinity of alpha raised to n 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) 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.

In Alessandro Coglio and Sol Swords: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023), Austin, TX, USA and online, November 13-14, 2023, Electronic Proceedings in Theoretical Computer Science 393, pp. 50–66.
Published: 14th November 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.393.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org