4 ms·

Isn‘t it possible to formally check Simulink autogenerated code using Polyspace? Or are you thinking of something else?

• phkahler 9y ago
  Oh god. You can check any C-code with Polyspace, I've done that. Most of the warnings Polyspace generates (at the time I did it) are not more significant than style - like checking for MISRA compliance doesn't guarantee a lack of bugs. To me formal verification has always meant proving correctness in a mathematical sense against some sort of formal specification. None of that really matters though because AFAIK you can't prove a neural net has been trained "correctly" and doesn't contain errors.
  • makintunde 9y ago
    "None of that really matters though because AFAIK you can't prove a neural net has been trained "correctly" and doesn't contain errors." Progress is being made in this area. Here is an "old" paper: https://arxiv.org/abs/1702.01135 https://arxiv.org/abs/1702.01135
  • naveen99 9y ago
    Halting problem is even more general.