Theorem Proving with ACL2 for Industry Artifacts

Theorem Proving with ACL2 for Industry Artifacts

Dmitry Nadezhin

14 June 2016

This is a set of slides to be presented at PSSV 2016, a workshop in St Petersburg, Russia. The slides present a small part of our formal verification work on SPARC processors and Java programs.


Venue : PSSV 2016, a workshop in Russia.