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

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

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.