SHF: Small: Bilinear Constraint Solving and Optimization for Program Verification and Synthesis Problems

SHF：小型：程序验证和综合问题的双线性约束求解和优化

• 批准号: 1527075
• 负责人: Sriram Sankaranarayanan
• 金额: $ 35万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1527075&HistoricalAwards=false
• 关键词: SHF; Small; Bilinear; Constraint; Solving

Bilinear constraints arise from numerous formal verification and synthesis problems for programs and hybrid control systems. However, bilinear constraints are also hard to solve. Existing approaches suffer from high computational complexity and the lack of guarantees due to numerical errors. Progress in solving bilinear constraints is an important step towards developing provably safe cyber-physical systems. This project investigates special structural properties of bilinear constraints to yield efficient solver implementations. The impact on program verification and synthesis problems is studied through specialized client applications. This infrastructure is disseminated online as open-source software. The research in this project is directly tied to educational materials in the form of video lectures and assessments for an existing open, online course on linear, integer programming and their applications. The overall goal of this project is to develop bilinear solvers targeted to verification and synthesis applications for programs and hybrid systems by exploiting key properties such as separability and the presence of sparse solutions. The main approaches are being investigated towards this goal: (a) relaxing bilinear constraints to simpler convex optimization problems, while recovering feasible solutions for the original constraints, (b) symbolic approaches that linearize the constraints and employ exact solvers for linear arithmetic constraints, and (c) iterative techniques that eliminate infeasible solutions incrementally to arrive at feasible solutions. These approaches are implemented inside prototype solvers with specialized clients for various formal verification and synthesis applications.

双线性约束产生于程序和混合控制系统的许多形式验证和综合问题。然而，双线性约束也很难解决。现有的方法存在计算复杂度高和数值误差等问题。解决双线性约束的进展是朝着开发可证明安全的网络物理系统迈出的重要一步。本计画研究双线性约束的特殊结构性质，以产生有效的求解器实作。通过专门的客户端应用程序的程序验证和综合问题的影响进行了研究。这一基础设施作为开放源码软件在网上传播。 该项目的研究直接与现有的线性整数规划及其应用的开放式在线课程的视频讲座和评估形式的教育材料相关。该项目的总体目标是开发双线性求解器，通过利用关键属性，如可分性和稀疏解的存在，针对程序和混合系统的验证和综合应用。目前正在研究实现这一目标的主要方法：（a）将双线性约束放宽为更简单的凸优化问题，同时恢复原始约束的可行解，（B）将约束线性化并采用线性算术约束的精确解算器的符号方法，以及（c）逐步消除不可行解以达到可行解的迭代技术。这些方法在原型求解器内部实现，具有用于各种形式验证和合成应用的专门客户端。

项目成果

Formal Techniques for Verification and Testing of Cyber-Physical Systems

• DOI: 10.1007/978-3-030-13050-3_4
• 发表时间: 2019
• 期刊: Design Automation of Cyber-Physical Systems
• 作者: Jyotirmoy V. Deshmukh;S. Sankaranarayanan