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.

AdaCore and Wind River discuss the features of the Helix and VxWorks 7 Cert platforms and how AdaCore solutions enable legacy software investments to be migrated with reduced time to market and minimized integration risks.

A challenge that every code base will phase over time are code smells. AdaCore provides tooling to find smells in code, like GNATcheck and CodePeer. Newly applied to a code base the number of findings of this tools can be big. Bigger than one can solve with limited resources. We will present an approach based on LibAdaLang to fix code smells automatically saving you many hours of rewriting code manually. This approach is pattern based and can thus be applied to generic transformations of a code base.

As the regulatory framework in the United States and Europe evolves to address increasingly growing cybersecurity threats, AdaCore is enlarging the scope of its offering to help you meet these challenges. In addition to its longstanding commitment to formal proof and static analysis, AdaCore is now upgrading its product security procedures and preparing a dynamic analysis solution. This presentation will give an insight into our roadmap in both areas, and showcase the upcoming fuzzing technology.

Presented by S. Tucker Taft - AdaCore

This session will introduce the QGen Auto Code Generator for Simulink®/Stateflow® 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.

Implementation and verification are traditionally viewed as two separate activities. Even in test-driven environments, the test platform is distinct from the implementation one. This talk will present an alternative approach where the verification and development activities are engineered together, creating effectively a “self-verified” program combining at the same place an implementation and the means to verify its correctness.

4 key takeaways
- Developing verification at the same time as the code allows for more efficient coding processes and mitigates errors at the end of the process.
- Formal proofs and testing can be combined to increase the level of safety and decrease overall development costs.
- There are alternatives to the C programming language that allows more effective verification.
- There is a way to redirect software developers energy from worrying about low-level coding errors to concentrate on more valuable aspects of software engineering.

Presented by Quentin Ochem at ScaleUp OSS.5 Europe Day.