4 ms·

I've been wondering for a while, and since this thread seems to have attracted people who may have answers… Can you (or anyone) provide any insight as to why A

I've been wondering for a while, and since this thread seems to have attracted people who may have answers… Can you (or anyone) provide any insight as to why ACL2 doesn't get mentioned much in discussions of formal methods? I'm interested in formal methods and ACL2 seems like a nice tool, but at least on HN all I usually see is Coq this and Coq that, with occasional mentions of TLA+ and Isabelle.

nickpsecurity 11y ago
I'm not sure why it doesn't get mentioned a lot. I do know that both LISP and best use of ACL2 (i.e. hardware verification) both get little mention in general. A variant of one to do the other should be similar. The best work I've seen in ACL2 comes from Rockwell-Collins and their SHADE verification suite. They've verified raw hardware, microcode, processor ISA, security policies, crypto systems... you name it. They give plenty of detail in their papers in how they do that albeit some are paywalled. The resulting AAMP7G processor is used in commercial applications needing reliability and security. I haven't done a straight survey on ACL2 in a while, though. Might be worth a reader doing and posting in case something interesting was overlooked. Rockwell's stuff seems to be best use of it, though.
- OopsCriticality 11y ago
  Not sure if you'll see this, but I did run across a preprint with a few Rockwell authors that might be of interest, "Development of a Translator from LLVM to ACL2" (http://arxiv.org/abs/1406.1566 http://arxiv.org/abs/1406.1566)
  - nickpsecurity 11y ago
    That's interesting work. Hardin is the name that was on the other ones. No surprise they dragged LLVM intermediate form into ACL2 to leverage their prior work. Good that it's fast but I'm more interested in what analysis they can do and how easily. Wish it had more of that. Still added it to my collection as it might come in handy for future ACL2 work. :)

nickpsecurity 11y ago

I'm not sure why it doesn't get mentioned a lot. I do know that both LISP and best use of ACL2 (i.e. hardware verification) both get little mention in general. A variant of one to do the other should be similar. The best work I've seen in ACL2 comes from Rockwell-Collins and their SHADE verification suite. They've verified raw hardware, microcode, processor ISA, security policies, crypto systems... you name it. They give plenty of detail in their papers in how they do that albeit some are paywalled. The resulting AAMP7G processor is used in commercial applications needing reliability and security. I haven't done a straight survey on ACL2 in a while, though. Might be worth a reader doing and posting in case something interesting was overlooked. Rockwell's stuff seems to be best use of it, though.

OopsCriticality 11y ago
Not sure if you'll see this, but I did run across a preprint with a few Rockwell authors that might be of interest, "Development of a Translator from LLVM to ACL2" (http://arxiv.org/abs/1406.1566 http://arxiv.org/abs/1406.1566)
- nickpsecurity 11y ago
  That's interesting work. Hardin is the name that was on the other ones. No surprise they dragged LLVM intermediate form into ACL2 to leverage their prior work. Good that it's fast but I'm more interested in what analysis they can do and how easily. Wish it had more of that. Still added it to my collection as it might come in handy for future ACL2 work. :)