Computer-Aided Programming is a research area at the interface of Programming Languages and
The goal of this field is to use the power of automatic reasoning, coupled with large amounts of computing power, to simplify the task
In this vision, powerful algorithms are used to manage the low-level details of programming, leaving the human
designer to focus on the creative, higher-level aspects of program
For instance, rather than
manually analyzing the corner-case behavior of a program, the programmer uses a program
verifier that automatically generates proofs of program correctness and finds bugs in programs.
Rather than coding up executable programs, the programmer specifies,
using a variety of notations, a hypothesis about the structure of the program
and the properties that it should satisfy.
An algorithm for program synthesis is now used to generate correct executable code.
All this may sound too good to be true, as even theoretically, program verification and synthesis are
But over the last few decades, our field has developed many algorithms and tools that either solve these problems
or alternately solve them exactly for important classes of programs. Some of these tools are now routinely used by program designers.
So what do we do while working in this area, on a day-to-day basis? Here's what:
language design: In Computer-aided Programming, we let the computer handle what it does best — low-level calculations
are large-scale search —
and rely on humans
for high-level algorithmic insights and domain knowledge.
But in that case, programmers should
able to communicate these insights to the
machine, and this demands the design of ultra-high-level, domain-specific programming languages. At this time, our group
such languages for users who want to program robots, design auctions, or teach students introductory programming.
Algorithmic reasoning about programs:
Much of the research in our group involves the design of powerful
algorithms for program verification and/or synthesis. Typically, such algorithms
establish complex logical relationships between program variables,
or systematically explore a program's state space.
For instance, work in our group has come up with algorithms for
formally proving that a program responds robustly to noisy inputs,
for finding optimal parameters for programs, and
for modular reasoning about
complex branching behaviors of programs.
Algorithms for reasoning about programs must perform a variety of
mathematical tasks, for example
solving complex constraints
and finding fixpoints and optima of mathematical functions. Some of these tasks can be solved using off-the-shelf solvers like
Z3, but many cannot. Part of the mission of our group is
to engineer new solvers for these tasks.