Accompanies The Calculus of Computation: Decision Procedures with Applications to Verification
Pi is a simple imperative programming language for writing verified programs. Its name abbreviates Prove it, which is what the language asks you to do. (For example: Does your program sort arrays? Prove it.) πVC is a verifying compiler for Pi programs. πVC supports exercises in our textbook The Calculus of Computation: Decision Procedures with Applications to Verification. Using πVC properly requires that you have learned or are learning the material of the book.
To use πVC,
Development of πVC was supported by the National Science Foundation under Grant Nos. CSR-0615449 and CNS-0411363, by Navy/ONR contract N00014-03-1-0939, and by a Sang Samuel Wang Stanford Graduate Fellowship. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation or the Navy/ONR.