[pl-seminar] DeepSpec 2017: Formally Verified Software

Monday, October 2, 2017 -
12:00pm to 1:00pm
CS 4310

Speaker Name: 

Stephen Lee




The Coq theorem prover is a powerful tool for verifying that program specifications satisfy various properties. In this presentation, I will introduce Coq using an example of verifying insertion sort. I will define a simple imperative language, a stack-machine language similar to Java bytecode, and a compilation process between them. The correctness of the compilation will then be proved. This demonstrates a very common technique in Coq, which has also been used to verify properties of LLVM bitcode and of operating systems.