Next-generation Constraint Solvers for Software Engineering and Security

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

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

约束求解器，自动解决数学约束的程序，在工程和科学的无数应用中使用。求解器可以被比作瑞士军刀，用于规划机器人的运动、配置汽车或自动查找软件中的错误等应用。工程师使用数学约束来建模他们的问题，然后使用求解器自动解决它们。就在十年前，商业软件（如文字处理器和操作系统）的可扩展自动错误查找被认为是不可行的。由于求解器性能的显著提高（由于包括我在内的许多研究人员），自动错误查找不仅变得可行，而且在像微软这样的公司中是强制性的。虽然迄今为止取得的进展很重要，但随着工程师处理软件合成等更难的应用，对更强大和更具表现力的求解器的需求持续增长。因此，我提出了一个长期的研究计划，开发新的求解器技术，数量级更快，更有表现力比今天的，旨在软件工程工具的软件可靠性和安全性。