Formal Executable object code VERification - FEVER

This project seeks to explore the possibility of using automated formal techniques to verify Executable Object Code. If the feasibility study shows that it is, then D-RisQ and Lemma 1 will develop the technology for commercial release. This technology is attractive to the market because the cost of verification is rising dramatically as complexity increases and is particularly attractive to the Robotics and Autonomous Systems market because it will enable the demonstration that the software does only what is required and crucially, never does what is forbidden. The cost of providing such evidence to support a safety case is currently very high. With automated techniques, the cost basis will change substantially and will enable a more rapid, assured development of many types of software systems.