ACL2
2006
ACM
14 years 6 months ago
2006
ACM
Several users have had problems using equivalence-based rewriting in ACL2 because the ACL2 rewriter caches its results. We describe this problem in some detail, together with a pa...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
We describe a new procedure for verifying ACL2 properties about finite state machines (FSMs) using satisfiability (SAT) solving. We present an algorithm for converting ACL2 conj...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
Biologists studying the evolutionary relationships between organisms use software packages to solve the computational problems they encounter. Several of these problems involve th...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
Support for congruence-based rewriting is built into ACL2. This capability allows ACL2 to treat certain predicate relations ”just like equality” under appropriate conditions a...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
We describe an embedding of the ACL2 logic into higherorder logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers. Categori...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
We introduce the logical story behind file input in ACL2 and discuss the types of theorems that can be proven about filereading operations. We develop a low level library for re...
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
We have written a new records library for modelling fixedsize arrays and linear memories. Our implementation provides fixnum-optimized O(log2 n) reads and writes from ad
ACL2
2006
ACM
14 years 6 months ago
2006
ACM
ACL2 is used to systematically study domains whose elements can be “uniquely” factored into products of “irreducible” elements. The best known examples of such domains are...