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

Research programmer

Collaborators at Rice

Chris Jermaine;
Lydia Kavraki;
Vivek Sarkar;
Moshe Vardi

Alumni

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)

Vacancies

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.

  • Reasoning about uncertain computation.
    See
    [CACM12],
    [POPL10],
    [FSE11],
    [ATVA13],
    and
    [POPL14-a].

  • Program smoothing and probabilistic reasoning about
    programs
    .
    See [PLDI10], [CAV11],
    [CAV12],
    and
    [POPL14-b].

  • Statistical reasoning about program
    databases

  • Probabilistic programming

  • Synthesis for
    robotics

  • Computer-aided mechanism design; synthesis for
    multi-agent systems

  • Constraint-based program synthesis.
    See [PLDI11] and
    [POPL14-c].

  • Logical methods for real computation.
    See [LICS13].

  • Language-based
    approximate computation

  • Procedure-modular reasoning about programs.

    See [TOPLAS11],
    [CAV06],
    [POPL06], and
    [POPL08].

  • Declarative isolation in
    parallel programs
    .

    See
    [OOPSLA09],
    [OOPSLA11],
    and
    [OOPSLA13].

Look no further than here!

Source Article