In recent decades, formal methods have produced many successes in proving properties of hardware and software artifacts. However, the lack of general efficient methods to verify designs that involve nonlinear arithmetic -- arithmetic that involves integer multiplication -- has been a major impediment to the effectiveness of verification methods in a broad array of applications. Among many other applications, computations that depend on nonlinear arithmetic are at the heart of CPU designs, cryptography, and structures for efficient storage of data for easy retrieval. This project is focused on achieving efficient verification of hardware and software designs that include nonlinear arithmetic.
This project explores methods for extending the most widely effective class of current verification methods, which at their heart use Boolean satisfiability (SAT) solvers, to handle designs that include integer multiplication. The investigators have shown that certain properties of integer multiplication circuits that have been conjectured to be representative of the difficulty of verifying nonlinear arithmetic can be efficiently verified in systems of inference that capture the capabilities of state-of-the-art SAT solvers. This project leverages and extends these theoretical insights to develop practical methods that will succeed in a broad range of verification tasks for software and hardware artifacts that use nonlinear arithmetic. The research results will be widely disseminated in open source tools for people to use for verification leading to software and hardware with a higher level of trustworthiness, including in safety-critical applications that people rely on every day.
