Dependability Computation using HOL4/ACL2 Link

A two-way link between HOL4/ACL2 is developed by M. Gordon and Matt Kaufmann to enable HOL users to employ ACL2 as a trusted oracle. However, both HOL4 and ACL2 have several releases since this link was made. This project serves two purposes: (i) Upgrading the link to latest versions of HOL4 and ACL2 tools; and (ii) Utilizing the link to compute the dependability of real-world systems using ACL2 computation abilities.

Currently, I’m visiting UT Austin, Tx, USA and working with Matt Kaufmann in his Formal Method Research Group. The long term goal of this project is to develop an easy framework that enables HOL4 user to make use of ACL2 for verifying FOL properties.