# J Moore: Machines Reasoning about Machines

Please watch the video Machines Reasoning about Machines of an EPFL talk by J Strother Moore, a professor at the University of Texas, Austin.

Then, answer the following questions:

- What is the name of the theorem prover presented in the video? ACL2.
- Which programming language is it based on? Lisp.
- State in English the lemma needed to prove the first sorting routine (the prover finds and proves it automatically)? If we insert an element in a sorted list, we get a sorted list.
- State in English the key property which was missing from the first specification of the sorting algorithm? The result must be a permutation of the input (careful: having the same set of elements is not enough because we want to maintain duplicates).
- Which company has been using this theorem proven for hardware verification? AMD
- What is the difference between software and hardware verification, according to the speaker? Hardware verification is usually finite state.
- What number should you return to simulate the factorial function on the JVM to be correct more than half of the possible inputs to the function? 0.