Gems in categories Open Source

  • Gem #93: High Performance Multi-core Programming - Part 1

    This Gem introduces an Ada implementation of "Chameneos-Redux," a benchmark program that compares the performance of threaded applications on a multi-core machine. In this series we explore the design and implementation techniques used to make a high-performance version of the program in Ada.

    Continue Reading in Ada Answers »

    Pat Rogers
    AdaCore
  • Gem #76: Tokeneer Discovery - Lesson 6

    Ada Gem #76 — In the previous Gem in this series, we saw how to deal with overflow errors, based on source code from Tokeneer. In this Gem, we show how to ensure secure information flow.
    This Gem brings us to the end of this series on Tokeneer, and we would like to say a big thank you to the SPARK team at Altran for providing these resources.
    We will now take a break for the holiday period and will return with more Gems on January 11, 2010. Very happy holidays to all Gem readers, wherever you are!
    Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran
  • Gem #75: Tokeneer Discovery - Lesson 5

    Ada Gem #75 — In the previous Gem in this series, we saw how the SPARK Toolset can verify application-specific safety and security properties, based on source code from Tokeneer. In this Gem, we show how to deal with overflow errors. Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran
  • Gem #74: Tokeneer Discovery - Lesson 4

    Ada Gem #74 — In the previous Gem in this series, we saw how to validate input in SPARK, based on source code from Tokeneer. In this Gem, we show how the SPARK Toolset can verify application-specific safety and security properties. Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran
  • Gem #73: Tokeneer Discovery - Lesson 3

    Ada Gem #73 — In the previous Gem in this series, we saw how to identify ineffective statements in SPARK, based on source code from Tokeneer. In this Gem, we show how to validate input. Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran
  • Gem #72: Tokeneer Discovery - Lesson 2

    Ada Gem #72 — In the previous Gem in this series we saw how to deal with improper initialization in SPARK, based on source code from Tokeneer. In this Gem, we show how to identify ineffective statements. Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran
  • Gem #71: Tokeneer Discovery - Lesson 1

    Ada Gem #71 — In previous Gems, we saw how to create a SPARK project in GPS, and how to run the Examiner and Simplifier tools to verify various properties of a simple linear search function. In this series of Gems on SPARK, we will explore SPARK capabilities in greater depth, using source code from Tokeneer, an NSA-funded, highly secure biometric software system.
    In this Gem, we show how to deal with improper initialization. Continue Reading in Ada Answers »

    Dean Kuo
    Altran
    Angela Wallenburg
    Altran