José F. Ruiz

This presentation will talk about hybrid verification, an innovative approach to demonstrating the functional correctness of a program using a combination of automated proof and unit testing.

SPARK 2014 comprises a subset of Ada 2012, excluding those features not amenable to sound static verification. SPARK 2014 uses the contract-based programming provided by the latest Ada 2012 version, and uses the Ada 2012 aspect notation to strengthen the specification capabilities of Ada by the addition of new contracts for data dependencies, information flows, state abstraction, and data and behavior refinement.

Once the functional behavior or low-level requirements of a program have been captured as SPARK 2014 contracts, the verification tool-set can be applied to prove that the implementation is correct and free from run-time exceptions automatically. Only where verification cannot be completed by themselves is it necessary to write unit tests, with the same contracts used to check the correct run-time behavior of the relevant subprograms.

This talk presents the design and usage of a dimensionality checking system in Ada 2012.

The purpose of dimensional analysis is to verify dimension consistency within physical relations, preventing errors such as the loss of the Mars Climate Orbiter because one module used metric units and another one imperial units. The presentation will describe how to perform compile-time checks to verify the dimensional consistency of physical computations, allowing the user to define his own system of units.

This presentation explains and demonstrates how Ada code can be embedded into Android devices.

The talk will be an introduction to programming Android devices in Ada. The Android framework can be used to develop a part of the application (such as the user interface), but you can still benefit from Ada's reliability and advanced software engineering principles for the application logic (for example, control algorithms or image processing). The presentation will describe and demonstrate how easy it is to follow this development approach with Ada.

This presentation explains and demonstrates how Ada is effectively used to control a Segway-like self-balancing robot.

LEGO MINDSTORMS are affordable and attractive robotics kits that can be used as teaching material, or as funny and interesting hobby. We have used this kit to design a Segway-like robot, where the control system is written in Ada and built with the GNAT compiler. The concurrency and real-time capabilities of the Ada Ravenscar profile are used to implement the dynamic interaction with the physical environment, respecting very stringent timing constraints.

A presentation of Ada's features in the parallel/multicore area, given in such a way that people can start experimenting and doing "interesting stuff".

Ada had built-in support for parallel programming from the start, and the successive standards keep improving that support, up to most recently for the new multiprocessor architectures. An overview of the support that already existed in Ada 83 and Ada 95 will be given, with practical examples so participants can try out some simple things first. Ada 2012 comes with interesting additions for using multiprocessors effectively. Embedded systems can use an extension of the Ravenscar profile to achieve analyzable real-time behavior on multicore platforms. Ada's dispatching domains achieve flexible allocation schemes for high-performance computing.