Building High Integrity Applications with SPARK

This is the first introduction to the SPARK 2014 language and the tools to verify programs for safety- and security-critical applications.