Special Lecture January 19, 2018 4:30pm — 5:30pm Location: Reddy Conference Room 4405 - Gates Hillman Centers Speaker: ROB SIMMONS https://www.cs.cmu.edu/~rjsimmon/ The First 15-122 Lecture, But With A Theorem Prover One of the first examples in 15-122 is proving a exponentiation function correct by documenting preconditions, postconditions, and loop invariants. But this proof, like all 122-style proofs, still has to be written and checked by students, TAs, or professors, all of whom can make mistakes.There are a number of systems that allow 122-style reasoning about programs to be checked by computers, greatly increasing our confidence in its correctness. In this presentation, I'll describe one of these systems, the Verified Software Toolchain project. I'll also give a demonstration of what it looks like to prove a C function correct using VST and the Coq theorem prover.—Dr. Rob Simmons was an Assistant Teaching Professor at Carnegie Mellon from 2013-2016. He now lives in Raleigh, NC where he does freelance independent computer science education and curriculum creation. Occasionally he still proves theorems for fun, and he is available to prove theorems for profit.
