3 ms·
SPARK is a real-world system that allows some degree of formal proofs in the programming language and related tools: https://learn.adacore.com/courses/intro-to
by thesuperbigfrog 5y ago
SPARK is a real-world system that allows some degree of formal proofs in the programming language and related tools:
https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html
https://docs.adacore.com/spark2014-docs/html/lrm/introduction.html https://docs.adacore.com/spark2014-docs/html/lrm/introductio...
- dandotway 5y agoI've tried SPARK. Compared to Frama-C, SPARK is not as powerful. Frama-C can prove the correctness of arbitrary heap manipulation algorithms. SPARK can handle singly linked lists but not doubly linked lists (last I checked). Although, usually the people who use SPARK use it because it is certified for their industry (such as aerospace).