Grants and Contributions:

Grant or Award spanning more than one fiscal year (2017-2018 to 2018-2019).

Advances in computing algorithms and computer hardware have made it possible to test models of cyberx000D
physical systems using formal techniques. This has been computationally intractable in the past. For somex000D
industrially-relevant engineering models, we now can prove that a model meets stated requirements. However,x000D
there is still much work to do to make this possible for a large enough set of models such that the techniquesx000D
and tools will be adopted by industry. This project will tackle some of those problems by focusing on a set ofx000D
models and requirements that are currently intractable. The underlying mathematical problems cannot bex000D
solved quickly enough or at all without further insight. The work proposed in this project will help advance thex000D
state-of-the-art in formal methods testing. The cyber physical systems that are being researched andx000D
prototyped today will have a tremendous impact on society in the near future. Self-driving cars and otherx000D
vehicles, smart buildings, smart power grids, and personal physiological monitoring are all poised to changex000D
central aspects of our lives. But one of the biggest challenges they present is how to ensure they are safe andx000D
secure, and we propose to provide tools for testing and verifying these systems. The industry partner isx000D
Quantum Research Analytics (QRA). QRA carries out formal testing of real world systems. We propose tox000D
develop the mathematics and software necessary to expand the range of systems that QRA can test. Inx000D
particular, we will expand the number of mathematical theories that can be solved using satisfiablity modulox000D
theories that occur in actual industry problems that QRA will supply. Graduate students and undergraduatex000D
students will also contribute to this research. We will begin by taking actual industry problems that can not bex000D
solved by current methods, and we will work to solve these problems by adding new theories, or mathematics,x000D
to the current solvers. This will yield an new software with expanded functionality that can be used to formallyx000D
verify new systems.