GAP Member Projects

The following are some examples of how Ada is being used in Academic projects by GAP members around the world.

  • Flight Software for Lunar IceCube Satellite

    Vermont Technical College

    The Lunar IceCube project is a major hardware/software development effort that will use the GNAT Pro and SPARK language toolsets to help achieve the high reliability required for space missions. Sponsored by NASA through their NextSTEP initiative (“Next Space Technologies for Exploration Partnerships”), Vermont Tech’s flight software development is part of a lunar exploration program that is being administered by Morehead State University. Lunar IceCube is a follow-on to an earlier NASA-sponsored Vermont Tech project, also developed using GNAT Pro and SPARK, that has been successfully transmitting data from an earth-orbiting CubeSat since its launch in November 2013.

    Continue Reading »
  • Verified Robot Control Software

    Bristol University (Bristol, UK)

    At the University of Bristol and at the Bristol Robotics Laboratory we want to trust our robots. We develop their control software in Ada/SPARK and verify it using the latest technology from AdaCore. Within the RIVERAS project (Robust Integrated Verification of Autonomous Systems) we aim to create systems that behave predictable even in the face of unpredicted events.

    Continue Reading »
  • 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 orbit. 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.

    Continue Reading »
  • Trusted Key Manager for IKEv2

    HSR University of Applied Sciences Rapperswil Switzerland

    IPsec relies on the correct operation of the Internet Key Exchange (IKE) protocol to meet its security goals. The implementation of IKE is a non-trivial task and results in a large and complex code base. This makes it hard to gain a high degree of confidence in the correct operation of the code.

    Continue Reading »
  • SPARK in Formal Verification Research

    Kansas State University, Manhattan, Kansas (US)

    Prof. John Hatcliff and his team at Kansas State University’s Static Analysis and Transformation of Software (SAnToS) Laboratory have found the SPARK language technology to be an ideal research vehicle for exploring novel techniques in formal program verification.

    Continue Reading »
  • Peer-to-Peer Epi-Transport Protocol

    University of Udine

    The DSP group at the University of Udine is developing PPETP (Peer-to-Peer Epi-Transport Protocol), a new streaming protocol based on a peer-to-peer approach that will allow to distribute efficiently live multimedia material to a large number of users. 

    Continue Reading »
  • Undergraduate Ada Projects - Gliding in Space

    The Australian National University

    At The Australian National University, students from the 2011 class in Concurrent and Distributed Systems provide an example of the high performance code they developed in undergraduate courses.

    Continue Reading »
  • Real-Time Software Development with GNAT for Mindstorms

    University of Adelaide Australia

    Final year students, Leighton Earl & Oliver Francis Roch, from The University of Adelaide undertook a project to create a system with both safety-critical and real-time components using GNAT Ada and Lego Mindstorms NXT.

    Continue Reading »
  • Ironsides Secure DNS Server

    United States Air Force Academy

    Dr. Martin C. Carlisle, the director of the Academy Center for Cyberspace Research at the United States Air Force Academy has developed a secure DNS server using Ada and the SPARK formal methods tool set.

    Continue Reading »
  • Real-Time control of a Model Railway System

    Western Washington University (Bellingham, Washington, US)

    At Western Washington University, students are using Ada in senior capstone projects on real-time control of a model railway system. 

    Continue Reading »
  • Real-Time System Development in Ada using LEGO MINDSTORMS NXT

    Universidad Politécnica de Madrid (Madrid, Spain)

    Universidad Politécnica de Madrid finds the LEGO MINDSTORMS kit and the GNAT GPL Edition for MINDSTORMS an ideal platform to allow students of embedded & real-time systems analyze, develop and implement a real-time system in Ada.

    Continue Reading »
  • Battling Robots: European Robotics Cup

    Telecom ParisTech (Paris, France)

    Telecom Robotics’ mission is to provide a robotics-focused forum where students can learn, share knowledge, and innovate. To help realize this goal, the group competes in the European Robotics Cup.

    Continue Reading »
  • ECHO: A Practical Approach to Formal Verification

    University of Virginia (USA)

    At the University of Virginia, Ada lies at the core of a comprehensive approach to creating software for safety-critical applications. Dr. John Knight and his student, Xiang Yin, have created a practical approach to formal verification called Echo.

    Continue Reading »
  • Serafina Autonomous Mini Submersible

    The Australian National University (Canberra, Australia)

    At the Australian National University (ANU), Ada plays an integral part in teaching and research, at both the undergraduate and graduate levels. Dr. Uwe Zimmer has been using Ada, with the GNAT technology on Linux, Windows, Mac, and Embedded MPC5554, in two major courses.

    Continue Reading »
  • Arctic Sea Ice Buoy and CubeSat Projects

    Vermont Technical College (USA)

    Under the direction of Professors Carl Brandon and Peter Chapin, students at Vermont Technical College are using AdaCore’s GNAT development environment along with Praxis’ SPARK tools on two NASA-sponsored programs with large software components.

    Continue Reading »
  • Dasher! – A Racing Robot in Ada

    Mälardalen University (Västerås, Sweden)

    Under the direction of Professor Lars Asplund, graduate students at Mälardalen University are designing, building and programming the Dasher robot in a project that is pushing the limits of robotics technology. The software is being developed with AdaCore’s GNAT toolset on Wind River Systems’ VxWorks real-time operating system.

    Continue Reading »