Automata learning is a powerful technique for obtaining system models from observed behavior and is often used in software testing, verification, and reverse engineering. However, most algorithms used today either require interaction with that system or suffer from poor scaling due to memory limitations. A relatively new approach in automata learning algorithms has been to store the dataset in a database and interact with it through custom database queries. This thesis uses this approach to develop a novel algorithm based on regular expression queries and custom data structures. Upon evaluation on generated datasets of binary sequences and the Abbadingo benchmarks, this approach was found to scale linearly to much larger dataset sizes than EDSM and to use orders of magnitude fewer queries than L*. It is also accompanied by a formal proof of correctness. Ultimately, this work provides a highly scalable algorithm and a self-contained, comprehensive theoretical framework. ... Read more

Learning a Deterministic Finite Automaton (DFA) from a language sample is an essential problem in grammatical inference, with applications in various fields, such as modeling and analyzing software systems. In this work, we propose approaches to create an ensemble of DFAs learned with the Evidence Driven State Merging algorithm. To produce varying models from the given data, we introduce two algorithms for manipulating the sequence orders. Additionally, we propose a similarity metric that allows for reducing the ensemble size by discarding similar models. The proposed approaches were analyzed and empirically evaluated using the dataset used during the StaMinA competition. Experimental results demonstrate that the methods for obtaining ensembles of DFAs presented in this work provide a number of advantages over the single DFA learned from the classical prefix tree acceptor using EDSM. ... Read more

Deterministic finite automata (DFA) are interpretable models used for classification and prediction tasks based on sequence data. They often act as surrogate models for software systems. Plenty of methods exist for the purpose of DFA learning. Examples include optimal algorithms such as SAT-based encoding and various heuristic methods as the likes of the BlueFringe framework of the EDSM algorithm. By definition, optimal algorithms can guarantee a minimal DFA consistent with the training data, but this does not exclude the possibility of heuristics also finding the optimal solution. However, it is generally believed that optimal methods could always require strictly less data to learn such a minimal model than their counterparts. In our research, we provide mathematical proofs and counter-examples that show the above statement to be false. We further demonstrate that, unless formally defined, there exist numerous languages and settings where heuristics outperform optimal methods on data efficiency benchmarks. Finally, we prove that optimal methods are equal to the BlueFringe framework in terms of optimistic learning efficiency. ... Read more

Learning deterministic finite automata (DFAs) from labeled traces is a key problem with applications in software analysis and system modeling. SAT-based methods are effective but can be slow when dealing with large datasets. To address this, we propose a sampling method that selects a smaller, but still representative set of traces. Our approach groups traces with similar suffixes and uses edit distance to choose diverse examples. The proposed sampling performs better than random uniform sampling and significantly better than heuristic algorithms. ... Read more

This paper investigates a hybrid approach to deterministic finite automata (DFA) identification by combining heuristic (EDSM) and exact (reduction to SAT) methods. The hybrid strategy implies first partially identifying the DFA heuristically and then minimizing it with an exact method. Two implementations of the hybrid approach are tested - one using binary search on the number of states of the intermediate model, and one that adjusts the SAT offset to control its search space. The results obtained on datasets from the STAMINA competition show that while the hybrid approach reduces the size of the inferred models compared to EDSM, this does not necessarily translate to better test performance. Nevertheless, the methods used in this work demonstrate how a hybrid approach can be applied to infer more compact models in DFA identification. ... Read more

Learning Deterministic Finite Automata (DFA) from given input data has been a central task in the field of Grammatical Inference, and progress in this area is of great interest from both theoretical and practical points of view. To address this challenge, several algorithms have been proposed and evaluated using established benchmarks. One such competition-winning algorithm, Evidence Driven State Merging (EDSM), uses a heuristic to learn a DFA from given data. However, improvements leveraging ensemble techniques from machine learning have yet to be explored. In this paper, we investigate ways to adapt the EDSM algorithm to fit into the ensemble learning framework and analyze the performance of such obtained models when applied to unseen data. To this end, we compare the performance of the ensembles to that of a standard EDSM-learned model, evaluating both their output quality and the diversity within each ensemble. The results indicate significant improvements in scenarios where the data is sparse. ... Read more

Deterministic Finite Automata (DFA) learning is the problem of reconstructing a DFA from its traces. For the development of methods for this problem, randomly sampled data is often used to train and test the performance of models. The choice of sampling technique can result in data sets with unforseen properties. The technique used in the STAMINA competition is such that that the number of final states and the size of alphabet were thought to potentially effect the test performance of resultant models. This was tested experimentally, by comparing the test performances of minimal models identified on traces from differently constructed DFAs. It was found that, although an increase in alphabet size results in overall longer traces that vary more with length, test performance still struggled. This shows that a DFA with a larger alphabet will need more traces than an equivalent smaller DFA. Additionally, it was found that the number of final states had a significant effect in the resulting test performance, and had a significant effect on the length of sampled traces. It was found that increased node count did not have an effect on sampled word length, and resulted in worse test performance. ... Read more

Software is everywhere, and going back to a life without software is unimaginable. Unfortunately, software does not always behave as expected, even though during the development cycle, software is usually tested to verify its correctness. To aid in testing, methods such as fuzzing or symbolic execution are used for automatic verification software systems. These methods are able to quickly find inputs to the systems that cover large portions of the code base. However, both of these methods struggle to find inputs that cover code which requires many iterations through loops.

In symbolic execution, loops are a large contributing factor to the path explosion problem and therefore the overall runtime. For loops containing conditional branches, each iteration is a new decision point. This leads to an exponential number of possible paths through a loop in comparison to the number of iterations.

In this work, we investigate the use of loops in symbolic execution to reach portions of the code which require numerous iterations through loops with conditional branches. We propose a novel technique for symbolic execution that uses the effects of one or more iterations through a loop to reach new parts of the code. By implementing this technique and applying it to a set of challenges designed to stress current tools and methods for software verification, we show that our technique is able to efficiently reach new parts of these challenges. These areas are not reached by state-of-the-art methods within the same time budget.

Another method for verifying software behavior is active learning, where simple models are learned from a system. These models capture the behavior of the system at a high level, allowing easier analysis to verify the behavior of a system. During the automatic learning of these models, loops are not handled separately. This leads to models where the behavior of a system is not captured fully, leading to incomplete analysis. We propose new methods for finding changes in behavior after executing these loops numerous times. We have compared our techniques to existing methods and show that this produces more complete models of a system. ... Read more