Fabien Chouteau, AdaCore

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Dr. Yannick Moy, AdaCore

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Dr. Carl Brandon, Vermont Technical College, Vermont, United States

Under the direction of Dr. Carl Brandon, students and staff of the University of Vermont’s CubeSat Lab built a1U CubeSat (10 cm x 10 cm x 10 cm, 1 kg) that was launched by NASA's ELaNa IV program on an Air Force Minotaur 1 rocket on November 19, 2013. Besides the 15 classified Air Force satellites aboard, there were two NASA CubeSats and 12 university CubeSats. Neither NASA CubeSat worked, 8 of the university CubeSats were never heard from, 2 had partial contact for one day, and one worked for four months. The VTC CubeSat, worked for two years and two days until it burned up in reentry over the Pacific. All the other CubeSats were programmed in C and ours in SPARK/Ada. This was our first CubeSat and 80% of the software was written by an undergrad with no prior SPARK/Ada experience. Dr. Brandon will describe the experience and the additions to the CubeSat software called CubedOS.

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Prof. Luis Miguel Pinho - Polytechnic Institute of Porto & INESC TEC, Porto, Portugal

Developing real-time systems applications requires programming paradigms that can effectively handle the specification of concurrent activities and timing constraints, as well as controlling their execution on a particular platform. This difficult task is increasingly more complex due to the prevailing trend for high performance, and the use of fine-grained parallel execution. This talk will analyze the state-of-the-art and challenges for the development of real-time parallel applications, discussing how the parallel capabilities foreseen in the Ada 2022 standard support real-time parallel programming, and which open issues still remain, comparing with competing initiatives for real-time parallel support, such as the ones proposed for OpenMP.

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Olivier Henley, AdaCore

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Prof. Mohamed Ali Ibrahim, Ph.D., P. Eng., University of Ottawa, Canada

The University of Ottawa’s Software Engineering program is currently collaborating with AdaCore on a Capstone project to give its students real-world, industrial integration project experience. In collaboration with Olivier Henley, an experienced AdaCore engineer, Prof. Ibrahim is supervising a team of four students in designing and implementing an oscilloscope based on the STM32F429I-DISCO microcontroller using Ada and SPARK programming languages. The project started in January 2023. It will pick up again next semester and continue until the end of December 2023. This presentation will share progress made during the first four months of the project, including work that has been completed and work that remains to be done.

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Dr. Ran Ettinger, Ben-Gurion University of the Negev, Israel

This talk presents the adoption of SPARK alongside Dafny in an elective course given to third-year CS and SE students at Ben-Gurion University of the Negev. Being based on Rustan Leino's "Program Proofs" with example programs following Carroll Morgan's "Programming from Specifications", this course focuses on the detection of proof obligations for the formal verification of iterative and recursive code. This talk aims to show how SPARK and GNATprove are complementing the use of Dafny, demonstrating to students the industrial applicability of the learned approach. In this talk, as in the course, I show how manual annotation of a program with loop invariants, assertions, and ghost procedures for lemmas, with or without full proof, may justify the functional correctness of a developed program, both to the automated verifier and (as importantly) to the human reader. Adoption of open-source SPARK programs as a starting point for assignment exercises is discussed. Finally, one proof-authoring construct that I enjoy in Dafny is highlighted, hoping to inspire its addition to SPARK.

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia

Using adareducer to minimize a program that says 'hello'

Learning concurrency, as a concept, precursor to programming concurrent artifacts, is difficult for students. In fact, it stays difficult beyond that age. Helping students learn how to “think concurrent” is a challenge. Teaching achieves its purpose when the learner learns, not when teacher’s transmission ends. That moment shines as a kind of intellectual epiphany, in the literal sense of revelation. In this talk I will illustrate the ingredients that I have used with most success in causing such epiphany, in the form of a concurrent programming problem that Ada solves magnificently.

with Prof. Tullio Vardanega, University of Padova, Italy

In this talk, we will review our experience of teaching SPARK/Ada for software system modeling and design in undergraduate programmes at the University of Southampton. In particular, we focus on the link between system-level design using the Event-B formal method and software-level verification using SPARK for developing dependable systems. Finally, we discuss our ongoing work in building an automatic translator from Event-B to SPARK.

with Dr. Son Hoang, University of Southampton, UK

When security is mentioned most students think about network security and protecting the operating system and transmission between computers, e.g. passwords, virus protection and encryption. While important, that leads students to neglect what is happening within a program. This presentation describes a course at Roger Williams University that focuses on the program level. It explains the development of the course and its outcomes. It discusses the students’ background and the influence that plays in how the course is executed. It describes why Ada/SPARK was selected, but why this is not considered a “programming” course. It will also provide some of the experiences over three offerings of the course with using the IDE, student perspectives, and future plans.

with Prof. Anthony Ruocco, Roger Williams University, Bristol, Rhode Island, US

ISAE-SUPAERO is an engineering program focusing on the aerospace industry in which students are exposed to a variety of scientific courses (aerodynamics, mathematics, airplane design, etc.) and only become specialized in their third and last year of study. This presentation highlights two experiments aimed at introducing students to formal methods through SPARK. The first one is a classic lecture introducing deductive methods through SPARK for the third-year students specializing in Computer Science. The second one is a 2-month research project on SPARK proof robustness for 2 second-year students. Both experiments demonstrate how students with no previous knowledge of formal methods or theoretical Computer Science may learn deductive methods efficiently using bottom-up approaches in which they are quickly confronted with tools and practical sessions.

with Prof. Christophe Garion, ISAE-Supaero, France and Dr. Claire Dross, AdaCore.

with Dr. Yannick Moy, AdaCore

with Fabien Chouteau, AdaCore

AdaCore's GNAT Pro Assurance development toolsuite for Ada, C, and C++ is the premier solution for software certification and projects where safety issues, security vulnerabilities, and other software modifications must be handled over the long term while minimizing costs.

The FACE™ (Future Airborne Capability Environment™) approach to portable military avionics software is gathering momentum, with FACE conformance increasingly appearing as a selection criterion in US Department of Defense procurements. The language best suited to meet both the portability requirements of the FACE Technical Standard and the assurance requirements of domain-specific standards such as MIL-HDBK-516C or DO-178C is Ada. In this session, you will learn how AdaCore can help you develop FACE conformant Ada software that meets one of the Safety profiles. A demo will take you through the steps of the conformance verification process using a “stubbed run-time library” approach that AdaCore has devised and which the FACE Consortium is currently considering.

Software safety certification standards assure that critical software is safe, secure, and reliable across the most demanding industries, including avionics, rail, space, industrial automation and automotive. However, meeting certification requirements can be challenging and costly. This presentation will demonstrate how AdaCore tools and technologies, from both a feature functionality and safety assurance perspective, can provide a cost-effective approach to meeting today's most demanding certification requirements.

This session will introduce the QGen Auto Code Generator for Simulink(r)/Stateflow(r) and explain the advantages provided by a TQL-1 Qualification, in terms of reduced time and effort to certify a Simulink-based application. The talk will identify the DO-178C and DO-331 objectives that are covered by the QGen code generator, meaning that your team can avoid many of the most labor-intensive steps involved in achieving certification, even at the highest level of criticality. The talk is aimed at both engineers and managers for such critical systems development activities and will cover the features of the QGen code generator, as well as other tools with which it is integrated, including a model-level debugger and testing tools for Simulink-based applications running in embedded targets.