The proposed project will result in increase of both speed and capacity when formally verifying complex software. The techniques will also be applicable when formally verifying hardware, proving the correctness of radiation-hardening transformations for digital circuits, mapping of software for execution on reconfigurable architectures such as FPGAs, logic synthesis, power and timing analysis of circuits, scheduling, planning, and solving of constraint optimization problems. The non-NASA customers will have the same benefits from the technology as NASA. The commercialization will target the major semiconductor, software, and Electronic Design Automation (EDA) companies, as well as NASA prime contractors, aerospace and weapons manufacturers, and all companies that develop embedded systems.
More »