piVC

piVC is a verifying compiler designed to be used with The Calculus of Computation, a textbook by Aaron Bradley and Zohar Manna. It compiles annotated (otherwise known as specified) programs written in a C-like languaged called pi. Specified programs contain the standard program text, as well as additional text that is used to specify properties of the program at various points in its execution. piVC uses this additional text to attempt to prove that the specified properties hold for all possible inputs to the program. piVC can also be used to prove total correctness of a program. Total correctness asserts that, given input constraints specified by the user, the program meets the given specification properties and is guaranteed to terminate. Questions or comments? Email jasonaue(at)cs.stanford.edu or jgalenson(at)cs.stanford.edu.