πVC: The Pi Verifying Compiler

New version available

Accompanies The Calculus of Computation: Decision Procedures with Applications to Verification
Home  |  Download  |  Tutorial  |  Pi Programs  |  Book

A verifying compiler compiles specified programs, which contain normal program text and additional text specifying desired properties of the program. A verifying compiler attempts to prove that the specified properties hold for all possible inputs to the program. For example, a partially specified implementation of Bubble Sort, BubbleSort.pi, contains the typical implementation and a specification that the returned array is sorted.

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,

  1. obtain and begin reading a copy of the book;
  2. download and install the software;
  3. prove some programs;
  4. and write, specify, and prove your own programs.
We welcome new Pi programs from users and will post particularly interesting ones as new examples or exercises.

Home  |  Download  |  Tutorial  |  Pi Programs  |  Book

© 2007, Aaron Bradley and Zohar Manna
Direct questions, comments, and cool Pi programs to arbrad{Shift+2}cs.stanford.edu.

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.