The 14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017) was held May 22-23, 2017, followed by the first ACL2 Developer's Workshop held on May 24 - 25 at The University of Texas at Austin in the Gates Dell Complex.

The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.

ACL2-2017 was a two-day workshop. It was the 14th in the series of ACL2 workshops, which occur approximately every 18 months. The workshop featured technical papers, keynote talks, and rump sessions discussing ongoing research.