AdaCore and Altran partnered together to present the SPARK User Group 2012 at the High Assurance Software Symposium. The day included a series of talks by experts on tools and strategies for developing safe and secure software, including the introduction of SPARK 2014, the next generation of the SPARK language, which provides powerful verification through testing and proof. Major enhancements include:

  • Verification by automated proof and unit testing
  • Advanced information flow analysis for secure systems
  • Convergence with Ada 2012 syntax
  • A bigger language subset
  • Selectable language profiles
  • More support for object-oriented programming
  • A formal container library
  • A generative mode for information flow
  • Future Directions of the SPARK Technology - SPARK 2014
    Stuart Matthews, Altran
  • Integrating Proof and Testing in Verification Strategies
    Cyrill Comar, AdaCore
  • Directions in Secure Software Development
    Rod Chapman, Altran
  • Certifying Formal Methods with ED-12C (DO-178C)
    Duncan Brown, Aero Engine Controls
  • Verification of Dependable Software using SPARK & Isabelle
    Stefan Berghofer, secunet Security Networks AG.