Qualification of Proof Assistants, Checkers, and Generators: Where Are We and What Next?

Mario Gleirscher, Robert Sachtleben, Jan Peleska

Cyber-physical systems, such as learning robots and other autonomous systems, employ high-integrity software in their safety-critical control. This software is developed using a ra…