Skip to main content
Cornell University
We gratefully acknowledge support from the Simons Foundation, member institutions, and all contributors. Donate
arxiv logo > cs > arXiv:2311.08855

Help | Advanced Search

arXiv logo
Cornell University Logo

quick links

  • Login
  • Help Pages
  • About

Computer Science > Logic in Computer Science

arXiv:2311.08855 (cs)
[Submitted on 15 Nov 2023]

Title:A Case Study in Analytic Protocol Analysis in ACL2

Authors: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)
View a PDF of the paper titled A Case Study in Analytic Protocol Analysis in ACL2, by Max von Hippel (Northeastern University) and 4 other authors
View PDF
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 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.
Comments: In Proceedings ACL2-2023, arXiv:2311.08373
Subjects: Logic in Computer Science (cs.LO); Mathematical Software (cs.MS)
Cite as: arXiv:2311.08855 [cs.LO]
  (or arXiv:2311.08855v1 [cs.LO] for this version)
  https://doi.org/10.48550/arXiv.2311.08855
arXiv-issued DOI via DataCite
Journal reference: EPTCS 393, 2023, pp. 50-66
Related DOI: https://doi.org/10.4204/EPTCS.393.6
DOI(s) linking to related resources

Submission history

From: EPTCS [view email] [via EPTCS proxy]
[v1] Wed, 15 Nov 2023 10:46:33 UTC (770 KB)
Full-text links:

Access Paper:

    View a PDF of the paper titled A Case Study in Analytic Protocol Analysis in ACL2, by Max von Hippel (Northeastern University) and 4 other authors
  • View PDF
  • TeX Source
  • Other Formats
license icon view license
Current browse context:
cs.LO
< prev   |   next >
new | recent | 2023-11
Change to browse by:
cs
cs.MS

References & Citations

  • NASA ADS
  • Google Scholar
  • Semantic Scholar
a export BibTeX citation Loading...

BibTeX formatted citation

×
Data provided by:

Bookmark

BibSonomy logo Reddit logo

Bibliographic and Citation Tools

Bibliographic Explorer (What is the Explorer?)
Connected Papers (What is Connected Papers?)
Litmaps (What is Litmaps?)
scite Smart Citations (What are Smart Citations?)

Code, Data and Media Associated with this Article

alphaXiv (What is alphaXiv?)
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub (What is DagsHub?)
Gotit.pub (What is GotitPub?)
Hugging Face (What is Huggingface?)
Papers with Code (What is Papers with Code?)
ScienceCast (What is ScienceCast?)

Demos

Replicate (What is Replicate?)
Hugging Face Spaces (What is Spaces?)
TXYZ.AI (What is TXYZ.AI?)

Recommenders and Search Tools

Influence Flower (What are Influence Flowers?)
CORE Recommender (What is CORE?)
  • Author
  • Venue
  • Institution
  • Topic

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)
  • About
  • Help
  • contact arXivClick here to contact arXiv Contact
  • subscribe to arXiv mailingsClick here to subscribe Subscribe
  • Copyright
  • Privacy Policy
  • Web Accessibility Assistance
  • arXiv Operational Status
    Get status notifications via email or slack