The announcement itself is pretty sparse on the proposed approach, but given the research interests of Swarat Chaudhuri [1] and Moshe Vardi [2], I would guess they will attempt to combine recent advancements in program synthesis, program verification, and code mining.<p>Program synthesis: There has been a lot of interest in the formal methods community to automatically generate programs (for small instances) with the target specification coming from input-output examples (e.g., Excel Flash Fill [3]), program templates or holes (called Sketches [4]), reactive models of adversarial environments, formal invariants etc. Also the solution techniques used vary considerably: from game theoretic solving, SAT solvers, model checkers, to version-space algebras and others. The community has not yet fixated on a specification language, or a solving technology. The industrial nature of the tools being leveraged (e.g., model checkers and SAT solvers from the hardware community) gives hope for promising developments. A Berkeley course [5] covers a good spectrum of the current developments.<p>If I were to guess, maybe the Rice researchers are approaching the code completion/correction problem as mining for fragments of large codebases that are incomplete/incorrect and applying program synthesis to fill those fragments. Of course that would mean that they would also need to mine the specification requirements for those fragments. All of this is easier said than done, and it would be an ambitious project. Swarat has also done some really cool work on "probabilistic reasoning for programs" and "verification of probabilistic programs", so that might be part of it too. (Of course, I may be completely off-base! After all, we are commenting on a non-technical funding announcement here.)<p>[1] Swarat's publications: <a href="http://www.cs.rice.edu/~sc40/pubs/" rel="nofollow">http://www.cs.rice.edu/~sc40/pubs/</a><p>[2] Moshe's publications: <a href="http://www.cs.rice.edu/~vardi/papers/index.html" rel="nofollow">http://www.cs.rice.edu/~vardi/papers/index.html</a><p>[3] Excel's FlashFill from Sumit Gulwani, researcher@MSR: <a href="http://research.microsoft.com/en-us/um/people/sumitg/flashfill.html" rel="nofollow">http://research.microsoft.com/en-us/um/people/sumitg/flashfi...</a><p>[4] The Sketch program synthesizer: <a href="https://bitbucket.org/gatoatigrado/sketch-frontend/wiki/Home" rel="nofollow">https://bitbucket.org/gatoatigrado/sketch-frontend/wiki/Home</a><p>[5] Ras Bodik/Emina Torlak: Berkeley course material on Program Synthesis: <a href="http://www.cs.berkeley.edu/~bodik/cs294fa12" rel="nofollow">http://www.cs.berkeley.edu/~bodik/cs294fa12</a>