Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2

TL;DR

This paper demonstrates how the partial-encapsulate feature in ACL2 facilitates the implementation of floating-point operations, highlighting its utility in formal verification tasks.

Contribution

It introduces the use of partial-encapsulate in ACL2 for implementing floating-point operations, showcasing its effectiveness.

Findings

Partial-encapsulate simplifies floating-point implementation in ACL2.

The approach enhances the modularity of floating-point operation verification.

It demonstrates practical benefits in formal methods applications.

Abstract

We illustrate the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2.