Implementing a cost-aware evaluator for ACL2 expressions

One of ACL2’s most interesting features is that it is executable, so users can run the programs that they verify, and debug them during verification. In fact, the ACL2 implementors have gone well out of their way to make sure ACL2 programs can be executed efficiently. Nevertheless, ACL2 does not provide a framework for reasoning about the cost of function invocations. This paper describes how such a framework can be added to ACL2, by using ACL2 macros and supporting code to access the prover state. The approach is illustrated with a cost analysis of red-black tree operations. Categories and Subject Descriptors C.4 [Computer Systems Organization]: Performance of Systems General Terms Evaluators, function cost Keywords ACL2 evaluator

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Ruben Gamboa, John R. Cowles
• Keywords: ACL2, ACL2 2006, ACL2 Implementors, Computational Linguistics, Sure Acl2 Programs