This talk discusses current extensions on the theory algebra from the NASA/PVSlibrary on formal developments for the Prototype Verification System (PVS). It discusses the approach to formalizing theorems of the ring theory and how they are applied to infer properties of specific algebraic structures. As cases of study, we will present recent formalizations on the theories of Euclidean Domains and Quaternions. Moreover, we will show how a general verification of Euclid’s division algorithm can be specialized to verify this algorithm for specific Euclidean Domains, and how the abstract theory of Quaternions can be parameterized to deal with the structure of Hamilton’s Quaternions.

Parallel island models are used to increase accuracy and performance (speed-up) of meta-heuristics. Such models provide gains by the exchange of information between islands through the migratory process. The key to obtaining gains with parallel island models is the manipulation of migration parameters, since depending on how these parameters are handled the gains vary. Based on this assumption, this work uses three meta-heuristics: genetic algorithm, self-adjusting particle swarm optimization and social spider algorithm. From each metaheuristic, parallel island models were proposed, diversifying the number of natives on the islands, and the behavior of these models were studied. The assessment confirmed the impact of variations migration parameters on accuracy and performance as well as the importance on the number of natives located on the islands. The best solutions were obtained with island models from genetic algorithm and self-adjusting particle swarm optimization, and the best speedups were achieved with island models from social spider algorithm.

Designing efficient parallel island Genetic Algorithms (GA) is a difficult task: several decisions are needed related to the adequate structure of the islands, how they are connected, how many individuals should migrate, and how often they should migrate. The impact of these choices has not yet been fully understood since they might vary for different problems. In previous work, a variety of island model GAs to solve Reversal Distance Problem (RDP) over uni-crhomosomal genomes were proposed from which adequate choices were pointed out that provided results with an excellent balance among accuracy and performance. In this work, another evolutionary problem is considered in order to analyze how general were the decisions taken for island model GAs over RDP. The problem is translocation distance over multi-chromosomal genomes, which involves the interchange of gene between different chromosomes. Despite the fact that this problem falls also in the category of evolutionary distance problems, it is different from the RDP. Regarding accuracy, island models using a dynamic communication topology for exchange of individuals between islands provided the best solutions; while regarding performance, models using a static topology reached the highest speedup. Comparing with previous work on RDP, it was observed that islands models that did not provided good accuracy in RDP provided good quality solutions for translocation distance problem, while the best island models for RDP did not repeat the same success for translocation distance problem. The only invariant is that all the island model GAs in addition to competitive speedups provided better results than the corresponding sequential GA.

Sorting unsigned permutations by reversals is anNP-hard optimization problem with applications in computational molecular biology. Several approximation and metaheuristic algorithms were proposed, among them, in a previous work, a competitive genetic algorithm and its parallel version using island models were proposed. In this paper, focusing on improving accuracy, new island models are proposed by diversifying the distribution of genetic material between islands through static and dynamic communication topologies. In static topologies, communication between islands is predefined and maintained during the computation, while in dynamic topologies the communication is continuously modified. The proposed island models use parallelism in a global and a local level, in which respectively, the exchange of individuals between islands and the fitness computation occurs. Results from the experiments performed with randomly generated synthetic permutations show that parallel island models using both dynamic and static communication topologies outperform parallel approaches found in the literature in terms of run-time as well as accuracy.

Translocation is a useful operation on strings with challenging questions in combinatorics of permutations and interesting applications in analysis of sequences. A translocation operation essentially is the interchange of prefixes and suffixes among two substrings of a string. For the case of genomes represented as strings, symbols that represent genes and chromosomes are modeled as substrings of the genomes; thus, translocation is an operation that models the interaction between chromosomes inside a genome. The translocation distance between two genomes is defined as the minimum number of translocations to convert one genome into another and has been proved to be a meaningful manner of modeling the evolutive distance between organisms. The particular case of unsigned genomes, those in which the orientation of the genes are not considered, is particularly difficult, while the signed case, in which the orientation of genes is considered, has been proved to be polynomially decidable. This paper presents an innovative Genetic Algorithm (GA) approach to solve the unsigned translocation distance problem. A distinguishing feature of the proposed GA is that it uses as fitness function the translocation distance for randomly generated signed versions of the input (that is an unsigned genome). Experiments over randomly generated strings (synthetic genomes) showed that the proposed GA approach computes answers that are better than those computed by an L5+ε-approximation algorithm, the latter also implemented as part of this work.