ACL2 Support for Automated and Interactive Proof

These slides are for an invited talk presented by Matt Kaufmann at 14th KeY Symposium 2015, Gothenburg, Sweden, July 27, 2015.