The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which model-level control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.
The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems. State-of-the-art theorem provers, however, suffer from a significant lack of automation.
