Enhancing mathematical theory coverage in satisfiability modulo theory solvers

计算算法和计算机硬件的进步使使用形式化技术测试计算机物理系统的模型成为可能。在过去，这在计算上一直很难处理。对于一些与工业相关的工程模型，我们现在可以证明一个模型满足规定的要求。然而，要使足够大的一组模型能够实现这一点，以便工业采用这些技术和工具，仍有许多工作要做。这个项目将通过关注一组目前难以解决的模型和需求来解决其中的一些问题。如果没有进一步的洞察，根本的数学问题就不能足够快地解决，或者根本不能解决。该项目中提出的工作将有助于推动形式化方法测试的最先进水平。今天正在研究和制作原型的网络物理系统在不久的将来将对社会产生巨大的影响。自动驾驶汽车和其他交通工具、智能建筑、智能电网和个人生理监测都将改变我们生活的中心方面。但它们带来的最大挑战之一是如何确保它们的安全，我们建议提供工具来测试和验证这些系统。行业合作伙伴是量子研究分析公司(QRA)。QRA对现实世界的系统进行正式测试。我们建议开发必要的数学和软件，以扩大QRA可以测试的系统的范围。特别是，我们将扩大QRA将提供的实际行业问题中出现的可使用可满足性模理论解决的数学理论的数量。研究生和本科生也将为这项研究做出贡献。我们将从当前方法无法解决的实际行业问题开始，并将努力通过在现有解算器中添加新的理论或数学来解决这些问题。这将产生一个具有扩展功能的新软件，可用于正式验证新系统。

Advances in computing algorithms and computer hardware have made it possible to test models of cyberphysical systems using formal techniques. This has been computationally intractable in the past. For someindustrially-relevant engineering models, we now can prove that a model meets stated requirements. However,there is still much work to do to make this possible for a large enough set of models such that the techniquesand tools will be adopted by industry. This project will tackle some of those problems by focusing on a set ofmodels and requirements that are currently intractable. The underlying mathematical problems cannot besolved quickly enough or at all without further insight. The work proposed in this project will help advance thestate-of-the-art in formal methods testing. The cyber physical systems that are being researched andprototyped today will have a tremendous impact on society in the near future. Self-driving cars and othervehicles, smart buildings, smart power grids, and personal physiological monitoring are all poised to changecentral aspects of our lives. But one of the biggest challenges they present is how to ensure they are safe andsecure, and we propose to provide tools for testing and verifying these systems. The industry partner isQuantum Research Analytics (QRA). QRA carries out formal testing of real world systems. We propose todevelop the mathematics and software necessary to expand the range of systems that QRA can test. Inparticular, we will expand the number of mathematical theories that can be solved using satisfiablity modulotheories that occur in actual industry problems that QRA will supply. Graduate students and undergraduatestudents will also contribute to this research. We will begin by taking actual industry problems that can not besolved by current methods, and we will work to solve these problems by adding new theories, or mathematics,to the current solvers. This will yield an new software with expanded functionality that can be used to formallyverify new systems.