Computer Science | Grinnell College

On Wednesday, November 20, in Noyce 3821, Professor Aaron Stump of the University of Iowa will give a lunchtime talk on the use of program verification tools in software development:

Usually programmers try to ensure code quality by testing. In this talk, I will describe an emerging new approach to creating high-quality software, using theorem-proving tools. These tools allow you to write a program and then prove mathematically that the program satisfies some desired specification. Formalized mathematics is not easy, but once you have completed your proof, you are guaranteed beyond a shadow of a doubt that your code is bug-free, at least with respect to the specification you have formulated. I will demonstrate verified programming — and maybe a little computer-formalized mathematics — using the Agda theorem prover, and speculate about how these new technologies could impact the future.

Professor Stump's talk, “Writing bug-free code using theorem provers,” will begin at noon. Pizza and soda will be served.