Upcoming Webinars in categories Formal Methods

No results found in categories Formal Methods

Webinars/Demos in categories Formal Methods

  • SPARK Pro 11 demos

    Robin Messer highlights the new features released in SPARK Pro 11 including:

    • Enhanced Support for Generic Subprograms
    • SPARKbridge
    • Counter Example Generator: Riposte
    • Improvements to the use of Functions in Proof Contexts
    • New Proof Statement: Assume
  • Introducing SPARK 10.1

    The InSight webinar series continues with a presentation on the new features of the AdaCore/Altran joint offering – SPARK Pro 10.1. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK 10.1 includes the following enhancements:

    • Generics Phase 1 - Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
    • Dynamic Flow Analyser and VCG Heaps
    • Unicode characters now allowed in strings
    • Improved use of types and subtypes in FDL
    • Improvements to Simplifier tactics and performance
    • Auto-generation of refinement rules
    • Improvements to SPARKBridge
    • New SPARKClean utility

    This webinar will include a demo and Q&A session with the developers of the SPARK Pro toolset.

  • Introducing SPARK 10

    The InSight webinar series continues with a presentation by Robin Messer on the new features of the AdaCore/Altran joint offering – SPARK Pro 10. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK Pro 10 is a major release including many new features – automatic selection of flow analysis mode, language profile for SCADE KCG, support for explicitly derived numeric types, addition of the SPARKBridge preview for Windows, library additions, and improvements to the SPARK proof tools.
  • Introducing SPARK 9.1

    The InSight webinar series continues with a presentation by Angela Wallenburg on the new features of the AdaCore/Altran joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK Pro 9.1 is a major release including many new features – the use of full range array subtypes, the relaxation of aliasing rules for record fields, the ability to specify VC generation on a per-file basis in metafiles, the introduction of new SPARK libraries, the introduction of the SPARKbridge feature.
  • Introducing SPARK 9.0

    The InSight webinar series continued with a presentation by Robin Messer on the new features of the AdaCore/Altran joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivaled support systems.

    SPARK Pro 9 is a major release including many new features – new information-flow verification for safety and security policies, a new SPARK2005 language profile, the new ZombieScope tool, cross referencing annotations in GPS, function return annotations are now treated more like procedure post-conditions, a new output format for POGS, and a new Examiner switch that checks consistency of casing within code and annotations.
  • Getting started with SPARK

    The InSight webinar series continues with a presentation by Rod Chapman on SPARK GPL – the high assurance toolset dedicated to the academic and Free Software communities. SPARK GPL combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment. SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. The SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.

    This webinar presents the concepts behind the Correctness-by-Construction methodology, includes a demo of the SPARK toolset and will look at current and potential research topics for the academic community.
  • Introducing SPARK Pro

    The InSight webinar series continued with a presentation by Rod Chapman on the AdaCore/Altran new joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivaled support systems. SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. The SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.

    This webinar presents the concepts behind the Correctness-by-Construction methodology and includes a demo of the SPARK Pro toolset.