Next-generation Constraint Solvers for Software Engineering and Security

用于软件工程和安全的下一代约束求解器

• 批准号: 435967-2013
• 负责人: Ganesh, Vijay
• 金额: $ 1.82万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=651491
• 关键词: Next; generation; Constraint; Solvers; Software

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.**************************************************************

约束求解器是自动解决数学约束的程序，用于工程和科学的众多应用。可以将求解器比作瑞士军刀，这些刀具用于诸如计划机器人运动，配置汽车或在软件中自动查找错误之类的应用。工程师使用数学约束对其问题进行建模，然后使用求解器自动求解它们。大约十年前，文字处理器和操作系统等商业软件的可扩展自动发现实际上是不可行的。得益于求解器绩效的令人印象深刻的收益（由于我包括我在内的许多研究人员），不仅可以自动发现发现是可行的，而且在Microsoft等公司中是必不可少的。尽管迄今为止的收益至关重要，但随着工程师处理诸如软件合成之类的更艰难的应用程序，对越来越强大且表现力的求解器的需求持续不断。因此，我提出了一项长期研究计划，旨在开发新的求解器技术，该技术比当今更快，更具表现力的订单，旨在用于软件可靠性和安全性的软件工程工具。**更确切地说，我的研究计划具有以下三个推力：i）我将基于机器学习（ML）探索新技术。 ML理论和技术有一场名副其实的革命。我们可以使用ML和随机推理技术在很大的约束下学习微妙的元级模式，这些模式可以更快地解决（类似于人类从数据中识别深度概念），ii）ii）利用无处不在且廉价的多核处理器来构建可扩展的平行的技术求解器和iii）求解器技术利用特定领域的知识作为解锁约束解决方案的关键。拟议的研究将具有深厚的基本科学，技术和商业影响。基本结果将通过参数复杂性和ML的思想为求解器启发式法提供理论基础。技术和商业影响将是一组新的可扩展和可扩展的求解器，有可能改变软件可靠性和安全性。************************************************************************* ****************************************