Formal Methods and Program Correctness

We will talk about the use of SPARK/Ada to verify program correctness using automated tools.

Tools / notes from meeting

1. Ada compiler in Fedora is GNAT
2. JGrasp visualization tool . We used this tool to view the Ada 95 tutorial programs. JGrasp will not parse SPARK directives.
3. Ada 95 tutorial.
4. Alire is the virtual evironment development tool.
5. Presentation resources: slides, examples, references, addtional notes.