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

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

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.