• The Muen Separation Kernel

    HSR University of Applied Sciences Rapperswil Switzerland

    The Muen Kernel, developed at The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland), enforces a strict and robust isolation of components to shield security-critical functions from vulnerable software running on the same physical system. To achieve the necessary level of trustworthiness, the Muen team used the SPARK language and toolset to formally prove the absence of run-time errors.

    Continue Reading »
  • Lunar CubeSat

    Vermont Technical College

    Vermont Technical College successfully launched a lunar cube satellite into earth orbit, where it will remain for about three years to test the systems that will be used for the eventual lunar mission. The CubeSat’s navigation and control software was developed in SPARK/Ada using AdaCore’s GNAT Programming Studio (GPS) IDE and GNAT Pro compiler and exploiting Altran’s SPARK toolset to prove the absence of run-time errors.

    Read the Press Release »
  • High-Reliability Vehicle Component Research Project

    TOYOTA ITC

    TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.

    Read the Press Release »
  • Cross Domain Guard for Military Tactical Systems

    Rockwell Collins

    Rockwell Collins successfully used SPARK Pro and GNAT Pro High-Security in the development of the SecureOne™ Guard, a high assurance cross domain guard for military tactical systems.

    Read the Press Release »
  • iFACTS - Air Traffic Management System

    NATS

    iFACTS ― the interim Future Area Controls Tools Support ― provides tools for trajectory prediction, conflict detection and monitoring aids. The iFACTS system includes over 200 KLOC of SPARK source code, from which over 120,000 verification conditions are generated to prove exception-freedom.

    Read the Press Release »
  • Multi-Level Security Workstation

    Secunet

    To develop a robust multi-level security workstation, Secunet Security Networks chose the SPARK Pro development environment. The security station concurrently handles information of different security domains, maintains confidentiality and integrity of all processed data, and enforces Multiple Independent Levels of Security (MILS) on a single hardware platform.

    Read the Press Release »