Harnessing Computational Knowledge to Provide Correct, Efficient and Cost-Effective Software

Principal Investigator:
Michael A. Langston, Department of Computer Science, University of Tennessee
Co-Principal Investigators:
William J. Cook, Department of Industrial and Systems Engineering, Georgia Institute of Technology
G. Neil Robertson, Department of Mathematics, Ohio State University
Paul D. Seymour, Department of Mathematics, Princeton University
Robin Thomas, Department of Mathematics, Georgia Institute of Technology
Overview:
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.