On Friday, 6 February 2015 at 05:16:56 UTC, Vlad Levenfeld wrote:
safety-critical systems. What's this kind of programming
called? And can you recommend any resources for learning about
the subject from square one?
I haven't actually used SPARK, so my knowledge on what it can do
is only superficial, but it is a step in the right direction to
allow critical parts of your program to be better secured than
the less critical parts. There is a tutorial here:
http://docs.adacore.com/spark2014-docs/html/ug/tutorial.html
The books on verification I have are from the '90s and heavy to
read, so you probably should look elsewhere.
The terminology differs, off the top of my head:
- program verification
- verifiable programming
- partial correctness
- formal specification techniques
- formal methods
...
http://en.wikipedia.org/wiki/Formal_verification
http://en.wikipedia.org/wiki/Correctness_(computer_science)
