Replaced Astree with Saturn as most won't be able to afford Astree. Do test Softbound, SAFEcode, and CPI on various libraries and vulnerabilities to find what works or doesn't. Academics need feedback on that stuff and help improving those tools. There's a serious performance hit for full, memory safety like Softbound+CETS but knocking out that many vulnerabilities might easily be worth some extra servers. Have fun. :)
Thanks for that. Looks like only SPARK is available in the operating system that I use. That is one big problem with research software and software research, it is often disconnected from the programmer community.
BTW, what do you think of this tool?
https://github.com/TrustInSoft/tis-interpreter