On June 21st, we will host our 2nd annual GAP Workshop. This workshop is designed to allow GNAT Academic Program (GAP) Members to share information with each other regarding successful teaching methods and research projects, even student projects. AdaCore engineers will also provide updates on Ada, SPARK, related resources, and our community efforts.
More information on the 2023 agenda and guest speakers is below. We also encourage you to check out last year’s presentations found here.
Note that Workshop attendance is limited to active GAP Members. To learn more about GAP or to register for membership click here. Current GAP members are welcome to register for the workshop at any time.
Agenda
| ET | CEST | Title |
|---|---|---|
| 9:00-9:05 | 3:00-3:05 | Welcome AddressJessie Glockner, GAP Coordinator, AdaCore |
| 9:05-9:45 | 3:05-3:45 | Assertive Programming with SPARKDr. 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. |
| 9:45-10:25 | 3:45-4:25 | Design and Implementation of a Networked, Embedded OscilloscopeProf. Mohamed Ali Ibrahim, Ph.D., P. Eng., University of Ottawa, Canada Olivier Henley, AdaCore 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. |
| 10:25-10:30 | 4:25-4:30 | Break |
| 10:30-11:10 | 4:30-5:10 | Real-Time Parallel ProgrammingProf. 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. |
| 11:10-11:50 | 5:10-5:50 | SPARK/Ada for High Integrity Spacecraft SoftwareDr. 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. |
| 11:50-12:00 | 5:50-6:00 | Break |
| 12:00-12:15 | 6:00-6:15 | Update on AdaCore Technologies for AcademiaDr. Yannick Moy, AdaCore |
| 12:15-12:30 | 6:15-6:30 | Update on the Ada Community and Alire Package ManagerFabien Chouteau, AdaCore |
| 12:30-1:00 | 6:30-7:00 | General Discussion/Q&A/Closing Statement |
Dr. Ran Ettinger is a Senior Engineer at NVIDIA, developing tools and methodologies for the formal verification of software, combining bounded model checking with deductive verification for proving correctness of sequential and concurrent programs. In teaching, as an adjunct lecturer at Ben-Gurion University of the Negev and in the Israel Academic College of Ramat Gan he is employing formal method techniques both in elective programming courses (at BGU using Dafny and SPARK) and more recently in required courses (at IAC using Dafny) on the foundational subjects of Logic and Set Theory as well as Formal Languages and Automata Theory. A passionate proof engineer and an experienced programmer with a history of research on static analysis of programs and on tools for software maintenance (IBM Research, Sun Microsystems Laboratories), Rani holds a Doctor of Philosophy degree from the University of Oxford (2008) and a Bachelor of Science degree in Mathematics and Computer Science from BGU (2000).
Prof. Mohamed Ali Ibrahim has been a regular part-time professor at the University of Ottawa, Faculty of Engineering, School of Electrical Engineering and Computer Science (EECS) since 2014. He received his Ph.D. in Electrical Engineering in the field of real-time kernels for embedded systems and a master’s degree in electrical engineering from the University of Sherbrooke, Sherbrooke, Quebec. He also holds a graduate diploma in computer science and a bachelor's degree in computer engineering from the University of Quebec at Chicoutimi (UQAC), Chicoutimi, Quebec. He has over eight years of industrial experience as a software developer.
Prof. Luis Miguel Pinho is a Professor at the Department of Computer Engineering - School of Engineering of the Polytechnic Institute of Porto, and a Senior Researcher at the INESC TEC Associated Laboratory. He promotes and leads activities in, among others, real-time parallel programming models, reliable software, and edge computing. He has published more than 150 papers in international conferences and journals in the area of real-time embedded systems, and has been general/program chair of several international conferences. He is a member of ISO/IEC JTC1/SC22/WG9, and a senior member of ACM and IEEE. He was Editor-in-Chief of the Ada User Journal, and is currently Technical Editor of ACM SIGAda Ada Letters.
Dr. Carl Brandon has been a Professor at Vermont Technical College since 1977 and is currently the Director of the CubeSat Laboratory - a collection of students and faculty building CubeSat technology spacecraft. Since 2004, VTC has received 33 grants, one of which resulted in the construction of a CubeSat that was launched in an Air Force Minotaur 1 rocket in November 19, 2013. VTC's CubeSat was in orbit and operational for 2 years and two days and was the only successful satellite of any kind launched by a college in the Northeast of the United States until 2018. He is now working on a grant with Peter Chapin and students to develop a satellite version of the JT65 weak signal protocol that will allow a university satellite to communicate with a university ground station from Jupiter. Carl received his undergraduate degree in Physics from Michigan State University, a year and a half of physics grad school and holds a Masters's degree in Zoology (seagull soaring flight aerodynamics) and a Ph.D. in Zoology (bat flight aerodynamics and functional anatomy) from UMass Amherst. He was one of three people who designed the world's first memory chip in 1968 for IBM’s Components Division in Fishkill, NY. Carl has been a commercial pilot and flight instructor since 1969.
Olivier Henley is a User Experience Engineer at AdaCore. His role is exploring new markets through technical stories. He is also leading AdaCore’s new Capstone program. Prior to joining AdaCore, Olivier was a consultant software engineer for Autodesk. Prior to that, Olivier worked on AAA game titles such as For Honor and Rainbow Six Siege in addition to many R&D gaming endeavors at Ubisoft Montreal. Olivier graduated from the Electrical Engineering program at Polytechnique Montreal. He is a co-author of patent US8884949B1, describing the invention of a novel temporal filter implicating NI technology. An Ada advocate, Olivier actively curates GitHub’s Awesome-Ada list.
Dr. Yannick Moy is Head of the Static Analysis Unit at AdaCore, leading the company’s static analysis efforts, and a developer of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes, and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud
GAP Workshop Registration Form
Attendance is limited to current GAP Members. To learn more about GAP or to register for membership click here.