Enhancing mathematical theory coverage in satisfiability modulo theory solvers

计算算法和计算机硬件的进步使得使用形式化技术测试网络物理系统模型成为可能。这在过去的计算中是难以处理的。对于一些工业相关的工程模型，我们现在可以证明模型满足规定的要求。然而，仍然有很多工作要做，使这成为可能的一个足够大的一组模型，这样的技术和工具将被行业采用。这个项目将通过关注一组目前难以处理的模型和需求来解决其中的一些问题。根本的数学问题不可能很快解决，或者根本不可能解决，除非有进一步的洞察力。在这个项目中提出的工作将有助于推进状态的最先进的形式化方法测试。今天正在研究和原型化的网络物理系统将在不久的将来对社会产生巨大的影响。自动驾驶汽车和其他车辆、智能建筑、智能电网和个人生理监测都将改变我们生活的核心方面。但它们所面临的最大挑战之一是如何确保它们是安全的，我们建议提供测试和验证这些系统的工具。行业合作伙伴是Quantum Research Analytics（QRA）。QRA对真实的世界系统进行正式测试。我们建议开发必要的数学和软件，以扩大QRA可以测试的系统范围。特别是，我们将扩大数量的数学理论，可以解决使用可满足性modulotheories发生在实际的行业问题，QRA将供应。研究生和本科生也将为这项研究做出贡献。我们将开始采取实际的行业问题，不能bessolved由目前的方法，我们将努力解决这些问题，通过添加新的理论，或数学，以目前的解决方案。这将产生一个具有扩展功能的新软件，可用于正式验证新系统。

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.