4 ms·

I have written safety-critical code and nobody has a test suite that could do what Astrée does. It can be used to proves the absence of errors with the abstract

I have written safety-critical code and nobody has a test suite that could do what Astrée does. It can be used to proves the absence of errors with the abstract interpretation that catches all divisions by zero, data races, and deadlocks, and does static taint checking. You want a test suite, but it's never better or good enough. Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html

gavinhoward 3y ago
> all divisions by zero, data races, and deadlocks, and does static taint checking. That is a wild claim. But how many false positives does it have? Too bad it's not FOSS; I would pay for that is the false positive rate was not too high.
- Nokinside 3y ago
  It's true claim, no potential error is ever omitted. It may be hard to get code pass because there are false alarms, but when it passes it holds. We are talking code without dynamic memory allocation, recursive function calls, no system and library calls, of course. Like some embedded aerospace, automation, healthcare and military applications. You can use it to verify some libraries if you can't do full coverage. Application domain abstractions are also available. NASA has open source tool called IKOS based on same abstract interpretation concept, but I don't know it's features.