  This volume contains the proceedings of the Fourteenth International Workshop
on the ACL2 Theorem Prover and Its Applications, ACL2 2017, a two-day workshop
held in Austin, Texas, USA, on May 22-23, 2017. ACL2 workshops occur at
approximately 18-month intervals, and they provide a technical forum for
researchers to present and discuss improvements and extensions to the theorem
prover, comparisons of ACL2 with other systems, and applications of ACL2 in
formal verification.
  ACL2 is a state-of-the-art automated reasoning system that has been
successfully applied in academia, government, and industry for specification
and verification of computing systems and in teaching computer science courses.
Boyer, Kaufmann, and Moore were awarded the 2005 ACM Software System Award for
their work on ACL2 and the other theorem provers in the Boyer-Moore
theorem-prover family.
  The proceedings of ACL2 2017 include the seven technical papers and two
extended abstracts that were presented at the workshop. Each submission
received two or three reviews. The workshop also included three invited talks:
"Using Mechanized Mathematics in an Organization with a Simulation-Based
Mentality", by Glenn Henry of Centaur Technology, Inc.; "Formal Verification of
Financial Algorithms, Progress and Prospects", by Grant Passmore of Aesthetic
Integration; and "Verifying Oracle's SPARC Processors with ACL2" by Greg
Grohoski of Oracle. The workshop also included several rump sessions discussing
ongoing research and the use of ACL2 within industry.
