Computer-Aided Programming @ Rice

The vision of Computer-Aided Programming is to use the power of automatic reasoning to simplify the task of programming. Here, rather than manually reasoning about programs, the programmer uses a program verifier to automatically find proofs of program correctness or incorrectness. Rather than directly coding up executable programs, the programmer writes a specification of the structure and function of a program, letting an algorithm for program synthesis generate correct low-level code.

All this may sound too good to be true, as program verification and synthesis are easily seen to be as hard as the Halting Problem for Turing machines. However, over the last few decades, our field has developed many algorithms and tools that either solve these problems approximately, or alternatively, solve them exactly for important classes of programs. Some of these tools are now routinely used by program designers.


Principal investigator

Swarat Chaudhuri

Ph.D. students

Postdoctoral researchers

Masters students

  • John Feser

Research programmer

Collaborators at Rice

Chris Jermaine; Lydia Kavraki; Vivek Sarkar; Moshe Vardi


Srinivas Nedunuri (postdoc 2012-14, now at Cycorp); Roberto Lublinerman (Ph.D. 2012, now at Google); Edwin Westbrook (postdoc 2011-13, now a researcher at Kestrel Institute)


We are hiring! Funding is now available for Ph.D. advisees as well as postdocs). Send Prof. Chaudhuri email (swarat at rice edu) if you are interested.



Look no further than here!

The Computer-Aided Programming group is funded by the National Science Foundation (NSF) and the Defense Advance Research Projects Agency (DARPA).