Sponsored Academic Programs
AdaCore
The GNAT Academic Program (GAP)
Dedicated to building a community of academic professionals, AdaCore has created the GNAT Academic Program. Its primary objective is to provide a collaborative platform where educational materials, knowledge, resources and fresh ideas can be developed and shared.
AdaCore provide the community with The GAP Package; a comprehensive toolset and support package designed to give educators the tools they need to teach Ada. It includes an integrated binary distribution of the GNAT and SPARK tool sets and a variety of add-ons and libraries. Instructors also receive direct help and support for all academic versions of GNAT including: assistance in using the system, suggestions for workarounds when system issues arise and help in understanding Ada.
For more information about joining the GNAT Academic Program, please contact: gap-contact@adacore.com
Altran Praxis
The SPARK Language and Tool Set
SPARK is an annotated subset of Ada that is appropriate for the development of high-integrity software systems. The language is designed to have an unambiguous semantics and the annotations add design-by-contract information that enables unprecedented depth and efficiency of analysis and verification to be performed.
The SPARK Toolset implements subset checking, static semantic analysis, information flow analysis, verification condition generation and theorem proving facilities in an industrial strength environment.
For educators, SPARK offers a small language that can be used to teach the principles of design-by-contract, static analysis, formal verification and safety- and security-critical software development. SPARK is also well-suited to the development of real-time and embedded systems. For researchers, SPARK can be used as a basis for advanced verification and analysis technologies, such as software model checking and proof planning. The full professional SPARK toolset is available with support at no cost to university faculty. An excellent textbook, by renowned author John Barnes, is available that explains the SPARK language and technology.
For further information about the SPARK Academic
Program please contact:
gap-info@adacore.com
Artisan Software
The ARTiSAN Academic License Program
ARTiSAN is committed to creating strong links between academia and industry and has joined AdaCore’s GNAT Academic Program to further this goal. Academic professionals and students will be able to access leading industry toolsets, materials and resources enabling them to share ideas and develop their engineering and programming skills to meet the demanding requirements of industry. We look forward to working with AdaCore and establishing new academic relationships as a result." Jeremy Goulding, CEO.
The ARTiSAN Academic License Program allows accredited universities to equip a classroom, or the whole establishment, with the market leading UML modeling tool: Real-time Studio. Having access to Real-time Studio not only enables students to gain experience in using a powerful object-oriented software engineering tool, but it also allows them to put into practice the UML and object-oriented analysis and design techniques they have learnt equipping them for the challenges they will face upon entering industry.
For further information about ARTiSAN’s Academic Program please send email to education@artisansw.com
IPL
Academic Licence Package
Since the mid-nineties, IPL has offered special licenses to academic institutions to help with undergraduate teaching and postgraduate research (limited to non-commercial projects). They firmly believe that offering their products to academic institutions on favorable terms is of long-term benefit to IPL; it leads to graduates, and ultimately an IT workforce, who understand the value and practice of software testing. Their special academic licence allows students and researchers to benefit from testing tools used by many high profile projects ranging from telecommunications, medical instruments, air-traffic control, avionics, rail transport, automotive, space, defense, nuclear energy, financial to digital broadcast systems. Cantata++ and AdaTEST95 are industry-strength testing tools, used to meet safety critical and high integrity standards such as DO-178B level A, CENELEC, IEC 61508, MISRA. IPL and AdaCore have been working together for many years to ensure that their respective products are properly integrated, and should be appealing to use at both the undergraduate and researcher levels.
For further information about IPL’s Academic Program
please visit:
http://www.ipl.com/products/academic/pa000.uk.php
Tidorum
Static analysis of worst-case execution time
The development and verification of real-time software requires knowledge of the execution time of the critical software functions. The execution time is often variable, depending on the input data and program state; what is then required is an upper bound on the worst-case execution time (WCET). Measuring execution times from test cases or profiling runs usually underestimates the WCET. In contrast, a static WCET analysis adds up the WCETs of the instructions on all possible execution paths and uses mathematical optimization methods to compute an upper bound on the total WCET — the longest execution path. Tidorum supplies a tool called Bound-T that uses static analysis of machine code to compute bounds on WCET and stack usage. Bound-T is mainly aimed at the smaller 8- and 16-bit microcontrollers but also supports some 32-bit processors such as the ERC32 (SPARC V7). Tidorum grants no-cost academic licenses for Bound-T and works with academic research groups to develop the tool and WCET analysis in general.
For more information about Tidorum’s academic program please visit:
http://www.bound-t.com/academic.html
