Next-generation Constraint Solvers for Software Engineering and Security

点击翻译按钮获取中文摘要

Constraint solvers, programs that automatically solve mathematical constraints, are used in myriad applications in engineering and science. Solvers can be likened to swiss-army knives, used in applications such as planning a robot's movement, configuring a car or automatically finding bugs in software. Engineers model their problem using mathematical constraints, and then use solvers to automatically solve them. As little as a decade ago, scalable automatic bug-finding of commercial software like word processors and operating systems was considered practically infeasible. Thanks to impressive gains in solver performance (due to many researchers including myself), not only has automatic bug-finding become feasible but is mandatory in companies like Microsoft. While the gains to-date are important, the demand for ever-more powerful and expressive solvers continues to grow unabated as engineers tackle even harder applications such as software synthesis. Hence, I propose a long-term research program to develop new solver techniques that are orders of magnitude faster and more expressive than today's, aimed at software engineering tools for software reliability and security. More precisely, my research program has the following three thrusts: i) I will explore new techniques based on machine learning (ML). There has been a veritable revolution in ML theory and techniques. We can use ML and stochastic inference techniques to learn subtle meta-level patterns in large constraints that enable faster solving (similar to how humans identify deep concepts from data), ii) techniques that leverage ubiquitous and cheap multi-core processors to build scalable parallel solvers, and iii) solver techniques that leverage domain-specific knowledge as keys to unlock solutions to constraints. The proposed research will have deep fundamental scientific, technical, and commercial impact. The foundational results will provide theoretical underpinning for solver heuristics through ideas from parametric complexity and ML. The technical and commercial impact will be a set of new scalable and extensible solvers which have the potential to transform software reliability and security.