The last several years have witnessed a rapid development of powerful
mathematical techniques for reasoning about the existence of
asymptotically fast algorithms.
We believe the time is right to develop systematic methods to harness
the computational knowledge provided by these techniques.
Our efforts proceed along several fronts.
Complexity theory and constructive mathematics join forces to tackle
important issues in algorithm engineering and software synthesis.
We study the feasibility of emergent tools for the automatic generation
of provably correct and practical algorithms.
Optimization and structural graph theory combine to produce original,
robust techniques to leverage raw computing power.
We investigate the potential for graph width metrics to guide without
intervention the search for novel, general-purpose strategies and
efficient implementations.
In all these tasks we seek to provide new mechanisms to extract,
synthesize and automate, with the overall goal that of software
correctness by construction.
Recent
papers, slides and codes
detail our progress.
