4 ms·
ACL2 doesn't get a lot of love from the side of the verification community that focuses on the proof systems that are more academically popular (HOL family, CIC
by porcoda 10mo ago
ACL2 doesn't get a lot of love from the side of the verification community that focuses on the proof systems that are more academically popular (HOL family, CIC family, etc.). A lot of interesting industrial work has been done with ACL2 and related systems.
- Animats 10mo agoYes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.
- porcoda 10mo agoI assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.