4 ms·
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 AC
by 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 agoThat'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. :)