On June 21, 2022, we hosted our first annual GAP Workshop, where GNAT Academic Program (GAP) Members shared information regarding successful teaching methods and research projects using the Ada and SPARK programming languages. Our own AdaCore engineers also provided updates on Ada, SPARK, related resources, and our community efforts. Below is a summary of the workshop agenda. Simply click on the topic titles to view the related presentation recordings.
To learn more about GAP please visit our overview page. To register for GAP membership click here.
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 | Introducing Students to Formal Methods through SPARKProf. Christophe Garion, ISAE-Supaero, France 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. |
| 9:45-10:25 | 3:45-4:25 | The Beauty of Epiphanies in the Learning of ConcurrencyProf. Tullio Vardanega, University of Padova, ItalyLearning 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. |
| 10:25-10:30 | 4:25-4:30 | Break |
| 10:30-11:10 | 4:30-5:10 | SPARK/Ada in Formal Software System Modeling and DesignDr. Son Hoang, University of Southampton, UKIn 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. |
| 11:10-11:50 | 5:10-5:50 | Developing a Secure Programming CourseProf. Anthony Ruocco, Roger Williams University, Bristol, Rhode Island, USWhen 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. |
| 11:50-12:00 | 5:50-6:00 | Break |
| 12:00-12:15 | 6:00-6:15 | Technical Update on Ada, SPARK, Libadalang, and Visual Studio CodeDr. 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 |
Our Presenters
Prof. Christophe Garion is an Associate Professor in Computer Science at the Department of Complex Systems Engineering (DISC) of the Aeronautics and Space Institute (ISAE-SUPAERO) of Toulouse, France. His teaching activities concern the SUPAERO Graduate Program. He holds a Ph.D. (2002) and an engineering degree (1999) from SUPAERO .
Dr. Claire Dross is a Software Engineer at AdaCore and one of the lead developers of the formal verification SPARK 2014 toolset. She is involved in the design and implementation of the tool and the underlying language, as well as in customer support, and teaching and training activities. She has a Ph.D. in deductive verification of programs using a satisfiability modulo theory solver from the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications.
Prof. Tullio Vardanega is currently an Associate Professor with the Department of Mathematics at the University of Padua, Italy, which he joined in January 2002. Prior to this, he was a staff member with the European Space Agency Research and Technology Center. He received his Ph.D. degree in computer science from the Technical University of Delft, Delft, The Netherlands. His research interests include high-assurance real-time systems and software engineering methods to develop them.
Dr. Son Hoang is a Lecturer in the Cyber-Physical Systems Group, a part of School of Electronics and Computer Science at the University of Southampton. He was awarded a first-class honors degree in Computer Engineering from the University of New South Wales (UNSW), Sydney, Australia in 2001. Subsequently, he studied for a PhD (also at UNSW) and was awarded his Ph.D. in 2006 for his thesis on "The Development of a Probabilistic B-Method and a Supporting Toolkit". He has been teaching software system modelling and formal methods for several years to first- and second-year students at Southampton.
Prof. Anthony Ruocco has been a Professor and Computer Science Program Coordinator at Roger Williams University in Bristol, Rhode Island since Since 2002. He took over the program and developed it into the only ABET/CAC accredited BS program in the state. Prior to this, he served as Associate Professor of Computer Science, and Assistant Chair of Computer Science at the United State Military Academy at West Point New York. He received his doctorate from George Mason University. He also served as a commissioned officer for 24 years in the US Army achieving the rank of Lieutenant Colonel, and was a member of the Operations Directorate (J3) of the United States European Command in Stuttgart Germany.
Dr. Yannick Moy is a Senior Software Engineer at AdaCore leading the company’s static analysis efforts as well as the development 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.
