• Accessible Formal Methods: A Study of the Java Modeling Language

      Rawding, Michael; Andriamanalimanana, Bruno; Advisor; Spetka, Scott; Reviewer; Vishwanathan, Roopa; Reviewer (2017-04-17)
      While formal methods offer the highest level of confidence that software behaves as intended, they are notoriously difficult to use. The Java Modeling Language and the associated OpenJML tool aim to make formal specification and verification more accessible to Java developers. This report gives an overview of JML and assesses its current status and usability. Though many common Java features have been implemented, lack of standard library support is identified as an obstacle to using JML effectively. To help address that problem, this report documents the process of adding support for a new library to OpenJML.
    • Image Processing In F#

      Odoi, Kaia; Andriamanalimanana, Bruno; Advisor; Novillo, Jorge; Reviewer; Sengupta, Sam; Reviewer (2017-05-01)
      Image searching is an essential feature of many software applications. Histograms can be used to represent the pixel color intensities of images. Measuring the similarities between images by comparing the histograms can be performed through the use of information-theoretic measures, such as the Kullback-Leibler divergence and cross-entropy. In this project, a query image is selected from a collection of images and it is compared to the other images to determine which image is most similar to the query image. This process is carried out by creating histograms of each image, and then using measures such as the Kullback-Leibler divergence and cross-entropy to compare the histograms. The .NET functional language, F#, is used in the implementation of this project. The C# language, another .NET language, was also used for coding the graphical user interface.