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:

1. What is the name of the theorem prover presented in the video? ACL2.
2. Which programming language is it based on? Lisp.
3. 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.
4. 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).
5. Which company has been using this theorem proven for hardware verification? AMD
6. What is the difference between software and hardware verification, according to the speaker? Hardware verification is usually finite state.
7. 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.