Enhancing mathematical theory coverage in satisfiability modulo theory solvers

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

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.