Extended Abstract: Mutable Objects with Several Implementations
Matt Kaufmann, Yahya Sohail, Warren A. Hunt Jr
TL;DR
This paper introduces the attach-stobj feature in ACL2, enabling multiple executable implementations of a single abstract stobj without recertification, enhancing flexibility and efficiency in formal verification workflows.
Contribution
It presents a new ACL2 feature, attach-stobj, allowing different executable implementations for an abstract stobj without recertification, improving modularity and reuse.
Findings
attach-stobj supports multiple implementations
no recertification needed after implementation changes
enhances flexibility in ACL2 formal verification
Abstract
This extended abstract outlines an ACL2 feature, attach-stobj, that first appeared in ACL2 Version 8.6 (October, 2024). This feature supports different executable operations for a given abstract stobj, without requiring recertification of the book that introduces that stobj or theorems about it. The paper provides background as well as a user-level overview and some implementation notes.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.