Gems in categories Formal Methods

  • Gem #148 : Su(per)btypes in Ada 2012 - Part 3

    In the previous two Gems of this series, we saw how the aspects Static_Predicate and Dynamic_Predicate can be used to state properties of objects that should be respected at all times. This Gem is concerned with the Type_Invariant aspect.

    Continue Reading in Ada Answers »

    Yannick Moy
    AdaCore
  • Gem #147 : Su(per)btypes in Ada 2012 - Part 2

    In the previous Gem in this series, we saw how the aspect Static_Predicate can be used to state properties of scalar objects that should be respected at all times. This Gem is concerned with the Dynamic_Predicate aspect.

    Continue Reading in Ada Answers »

    Yannick Moy
    AdaCore
  • Gem #146 : Su(per)btypes in Ada 2012 - Part 1

    The new revision of Ada is full of features for specifying properties of types. In this series of three Gems, we describe three aspects that can be used to state invariant properties of types. This first Gem is concerned with the Static_Predicate aspect.

    Continue Reading in Ada Answers »

    Yannick Moy
    AdaCore
  • Gem #80: Speedy Shift and Rotate in SPARK

    Ada Gem #80 — This Gem covers a topic that I recently encountered while working on a crypto algorithm in SPARK: how to use Ada's predefined shift and rotate functions with modular types from a SPARK program. Continue Reading in Ada Answers »

    Rod Chapman
    Altran
  • 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
  • Gem #69: Let's SPARK! - Part 2

    Ada Gem #69 — Welcome back! We hope you had a great summer. Now let's get back to where we left off.
    In this Gem and the previous one, we give you a simple walkthrough of SPARK's capabilities and its integration with GPS. In the previous Gem, we showed how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors. In this Gem, we show how to prove that your SPARK programs respect given contracts. Continue Reading in Ada Answers »

    Yannick Moy
    AdaCore
  • Gem #68: Let's SPARK! - Part 1

    Ada Gem #68 — Please note that this is the final Gem before we break for summer. The series will resume on September 7, 2009.

    In this Gem and the next one, we present a simple walk-through of SPARK's capabilities and its integration with GPS. In this first Gem, we show how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors.

    Continue Reading in Ada Answers »

    Yannick Moy
    AdaCore