With the introduction of autonomous vehicles on public roads, their performance in emergency situations has become a strong focus. Collision Imminent Control (CIC) concerns the planning and control of aggressive evasive maneuvers for collision avoidance of automated vehicles. CIC is implemented using adaptive Nonlinear Model Predictive Control (NMPC), which considers obstacles and road barriers for combined trajectory re-planning and control. To achieve real-time performance, the prediction model complexity is often reduced, which can lead to an under-utilization of the control potential. The aim of CIC is to use as much of the control potential of the vehicle as possible while remaining real-time viable.

In this research, CIC is implemented using objective-based collision avoidance based on the distance to obstacles and road boundaries. Different collision avoidance formulations were derived and compared on accuracy and real-time performance. The control potential of the vehicle was further exploited by a computationally efficient vehicle model that employs differential braking. The NMPC problem is solved using Sequential Quadratic Programming (SQP) with Real Time Iterations (RTI). Different techniques that reduce the computation time were compared. Sparse solvers and variable timesteps were found to be most significant.

The robustness of the controller was improved by friction estimation. The controller is furthermore demonstrated to work on highly curved roads and in scenarios with dynamic obstacles. The controller is implemented on the hardware of a real autonomous vehicle and simulated on a closed-loop embedded system. Combining all these elements results in a CIC controller that can apply more control potential and reach control frequencies upwards of 100 Hz, increasing the level of safety in vehicle collision avoidance.

Reusable tools for engineering software languages can bridge the gap between formal specification and implementation, lowering the bar for engineers to design and implement programming languages. Among such tools belong NaBL2 and its successor Statix, which are meta-languages for declaratively specifying the static semantics of programming languages and generating typecheckers accordingly.

Although Statix intends to cover the domain of static semantics specification to a greater extent than NaBL2, less is known about how the meta-languages compare in terms of their practical usability.

In this thesis, we perform a case study in which we apply Statix to define the semantics of IceDust, an incremental computing DSL for modeling data with relations, and compare it to a prior NaBL2 specification.

We compare the novel and prior specification in order to determine how the meta-languages, when applied to the case of IceDust, compare in terms of high-level characteristics: expressiveness, readability, implementation effort and runtime performance. We perform four evaluations to this end: a qualitative in-depth comparison of the specifications, a measurement of specification sizes, an evaluation of correctness and a runtime performance benchmark of the resulting type checkers.

Our findings suggest that although Statix has a larger coverage of possible language definitions, in the case of IceDust it is a less expressive formalism for defining the static semantics and generates a slightly less performant type checker when compared to NaBL2. We find areas of interest for future work aiming to improve the practical usability of Statix, namely the definition of type compatibility relations, the way data in the scope graph are stored and retrieved and the integration with the compiler back-end.

Algebraic effects and handlers have become a popular abstraction for effectful computation, with implementations even in mainstream programming languages, such as OCaml. The operations of an algebraic effect define the syntax of the effect, while handlers define the semantics. This provides modularity, because we can choose which handler to apply to a computation. However, we cannot write handlers for many higher-order operations; operations that take effectful computations as parameters. Such higher-order operations can therefore not enjoy this modularity. Hefty algebras provide an additional layer of abstraction in the form of elaborations to make implementations of higher-order operations modular as well. Several languages, such as Koka, natively support algebraic effects and handlers. However, until now, no languages have been created with native support for higher-order effects. In this thesis, we introduce Elaine, a language featuring both handlers for algebraic effects and elaborations for higher-order effects. Additionally, we introduce implicit elaboration resolution; a type-directed procedure which infers the appropriate elaborations from context. We conjecture that hefty algebras are the semantics for Elaine. We provide a specification for Elaine, including its syntax definition, typing judgments and reduction semantics. This specification is implemented in a publicly available prototype which can type check and evaluate the set of example programs included with this thesis.

Intrusion detection systems (IDSs) are essential for protecting computer systems and networks from malicious attacks. However, IDSs face challenges in dealing with dynamic and imbalanced data, as well as limited label availability. In this thesis, we propose a novel elastic gradient boosting decision tree algorithm, namely Elastic CatBoost Uncertainty (eCBU), that adapts to concept drifts and copes with label scarcity by using a novel sequential uncertainty estimation method. We compare our method with state-of-the-art techniques on synthetic and real-world datasets and show that it achieves comparable accuracy and higher robustness to limited label availability in intrusion detection tasks.

With the ever-increasing digitalisation of society and the explosion of internet-enabled devices with the Internet of Things (IoT), keeping services and devices secure is becoming more important. Logs play a critical role in sustaining system reliability. Manual analysis of logs has become increasingly difficult, accelerating the development of automated methods for log-anomaly detection. Despite significant progress in automating log analysis, current state-of-the-art methods face challenges dealing with unstable log data, which means that the content of log messages evolves over time.

We show that LogBERT, a state-of-the-art technique based on Bidirectional Encoder Representations from Transformers (BERT), cannot deal with unstable log data. On the three most prevalent publicly available log datasets, Mathew's Correlation Coefficient (MCC) score (which measures the correlation between a model's output and the correct labels) of LogBERT dropped by 90% after increasing log data instability from 1% to over 80% normal sequences containing logkeys in the test set. Log data instability was increased by only reassigning samples between the train and test set. Furthermore, we show that the high performance of LogBERT reported in the original paper was achieved because the model relied on a simple heuristic that only worked under specific conditions.
To address this issue, we propose a novel sequence anomaly detection technique based on BERT: Vocabulary-Free BERT (VoBERT). VoBERT uses a novel pre-training task we designed specifically for anomaly detection: Vocabulary-Free Masked Language Modeling (VF-MLM). We adapted traditional MLM and removed the fixed vocabulary constraint, which allows VF-MLM to classify out-of-vocabulary logkeys correctly.
We highlight that VoBERT is more stable than LogBERT and outperforms the latter in certain situations where log data is very unstable. For the public datasets, the MCC score of the specific train-test split used in the LogBERT paper dropped by 90% after reassigning the train-test split, increasing log data instability. In addition to sequence-level anomaly predictions, we evaluated all approaches on element level, providing a more granular performance assessment.
To assess the generalisation of the experimental results to real-world scenarios, we conducted a case study evaluating the anomaly detection models on real-world security event data collected at a large bank (50,000+ employees). We found that the simple heuristic did not work for this real-world data, having a negative correlation with the correct results. VoBERT showed performance on par with LogBERT on this real-world security event dataset.
We urge future researchers to evaluate their methods on real-world data, as we showed that the commonly used public datasets do not represent real-world scenarios. Furthermore, it is important to assess how difficult it is to detect anomalies in datasets used for evaluation. When a simple heuristic can perform well, such datasets might not be well suited to evaluate a complex anomaly detection model.
This thesis is a proof of concept for the novel pre-training task VF-MLM and paves the way for future work to refine this technique further, as well as to develop additional robust and adaptable solutions for log and security event anomaly detection.

How convenient would it be to have an AI that relieves us programmers from the burden of coding? Program synthesis is a technique that achieves exactly that: it automatically generates simple programs that meet a given set of examples or adhere to a provided specification. This is often done by enumerating all programs in the search space and returning the first program that satisfies the requirements. However, these algorithms frequently enumerate redundant programs because of symmetries in the search space. We propose a new constraint discovery system that is able to detect these symmetries in a language and systematically generate symmetry-breaking constraints for them. To test these constraints, we implemented a novel, re-usable framework for program synthesis called Herb.jl. The generated constraints are shown to cut down search spaces to less than 25% of the original size and reduce the enumeration time by a factor of 3. Furthermore, this approach is extended to automatically discover semantic specifications without needing an expert. The effectiveness of these specifications is evaluated with an existing specification-based synthesizer, which shows that adding these specifications is an effective way to cut the synthesis time in half for domains where expert-defined specifications are not available. Together, these approaches demonstrate the effectiveness of extracting additional information from a language and applying it during enumeration.

Phylogenetic networks are a specific type of directed acyclic graph (DAG), used to depict evolutionary relationships among, for example, species or other groups of organisms. To solve computationally hard problems, treewidth has been used to parametrize algorithms in phylogenetics. In the hope of simplifying the algorithmic design process, Berry, Scornavacca and Weller recently proposed a new measure of tree-likeness that takes into account the directions of the arcs: scanwidth. They showed that the corresponding decision problem of this parameter - which can be seen as a variant of directed cutwidth, using a tree instead of a linear ordering - is NP-complete. This thesis aims to widen the structural knowledge of scanwidth and to find efficient ways of computing it on general DAGs, both by exact and heuristic algorithms.

With the help of reduction rules, we construct an explicit dynamic programming algorithm that computes scanwidth exactly, along with its corresponding tree extension, in O(k * n^k * m) time for rooted DAGs of scanwidth k. This slicewise polynomial algorithm proves that computing the scanwidth is in the complexity class XP. The algorithm also functions as an FPT algorithm for networks of level-l, with the complexity bounded by O(2^4l-1* l * n + n²). It performs well in practice, being able to compute the scanwidth of networks up to 30 reticulations and 100 leaves within 500 seconds.

On the heuristic side, an algorithm that repeatedly splits at a specific type of smallest cut is proposed. Enhanced with simulated annealing, this heuristic shows promising results, obtaining an average approximation ratio of 1.5 for large synthetic networks of 30 reticulations and 100 leaves. Applied to a real-world dataset of networks, the heuristic performs near-optimal. Although we prove that the scanwidth is always greater than or equal to the treewidth, experiments show that they are close to each other in practice. This further motivates the use of scanwidth over treewidth as a parameter in algorithms.

The Statix meta-language has been developed in order to simplify the definition of static semantics in programming languages. A high-level static semantics definition of a language in Statix can be used to generate a type-checker, hence abstracting over the shared implementation details. Statix should be able to express the static semantics of itself as well. The process of defining a language using itself is called bootstrapping. In this thesis we discuss the bootstrapping of the Statix meta-language within the Spoofax language workbench. The bootstrapping of a type-system domain specific language hasn't previously been discussed in existing work. It acts as an interesting case study on the use of Statix to define semantics for a constraint-based declarative language as well as the use of Statix throughout a full compiler pipeline. In addition bootstrapping grants Statix a more expressive type system, which enables the future development of the language.

Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.

The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench.

Sequential decision-making problems are problems where the goal is to find a sequence of actions that complete a task in an environment. A particularly difficult type of sequential decision-making problem to solve is one in which the environment has sparse rewards, a large state space, and where the goal is to complete a complex task. In this research we create a controller that can be used to solve these types of environments in cases where the task needs to be optimized for multiple objectives. We create MOPRL, an approach that combines techniques from planning, formal methods, and reinforcement learning to synthesize such a controller. W

Reinforcement learning (RL) has grown tremendously over one and a half decades and is increasingly emerging in many real-life applications. However, the application of RL is still limited due to its low training efficiencies and surplus training cost. The sampling and computation complexity normally depends on the size of the state space and splitting the state space can distribute computation and accelerate learning. State abstraction as a form of data-centric method shrinks the state space and reduces learning time, however, it is challenged by the fact that abstraction throws away information and might result in a sub-optimal solution. In this thesis, we propose the hierarchical clustering-based state grouping (HCSG) method to split the ground state space into clusters and train multiple agents for each cluster without changing the dimension of the state space. This approach allows us to distribute computation and improves training efficiency without losing the overall performance, and was also shown to outperform baseline and other state-of-art data-centric methods.

Dependently typed languages such as Agda have the potential to revolutionize the way we write software because they allow the programmer to catch more bugs at compile time than classical languages. Nonetheless, dependently typed languages are hardly used in practice. One of the reasons is the lack of mature compilers for them.
This paper describes the implementation of a new Agda compiler that targets the Higher-Order Virtual Machine (HVM). Firstly we outline the theoretical benefits of using an optimal functional language such as HVM. Secondly, we present the problems we faced and the solutions we devised in the implementation of the agda2hvm compiler. Lastly, we compare our implementation to the current best Agda compilers by running benchmarks and analyzing both time and space performance. We obtained results ranging from our compiler being exponentially faster than the state-of-the-art to being exponentially slower.

Agda is a functional programming language with built-in support for dependent types. A dependent type depends on a value. This allows the developer to specify strict constraints for the types used in an application. Writing code with dependent types results in fewer type-related errors slipping through the compilation process.
When executing Agda code, it is first compiled into a different programming language. This process is called code extraction. This step is applied since most of the typed code becomes unnecessary after type-checking and can therefore be removed. Currently, the Agda compiler supports only Haskell and JavaScript as target languages. However, exploring Rust as a target language could potentially lead to better performance, and it would allow access to the Rust library ecosystem.
Overall, the agda2rust backend could be a viable alternative to what is currently available. While it is not fully feature-complete and will not outperform any existing backends yet, agda2rust provides a way to seamlessly integrate algorithms and data structures implemented and proven in Agda into an existing Rust codebase.

Agda, a promising dependently typed function language, needs more mainstream adoption. By the process of code extraction, we compile proven Agda code into a popular existing language, allowing smooth integration with existing workflows. Due to Agda’s pluggable nature, this process is relatively straightforward. We implement a solution in Haskell and perform an empirical benchmark analysis. We show that LLVM’s Intermediate Representation language is a usable and promising target, although some optimizations are necessary before broader application. More indirect paths towards LLVM IR appear more suitable, because of the large translation gap.

Dependently typed languages such as Agda can provide users certain guarantees about the correct- ness of the code that they write, however, this comes at the cost of excess code that is not used at run time. Agda code is currently compiled to another language before it is run, there are not many target languages in popular use, so it is unclear if there are other potential target languages that could do a better job. The purpose of this paper is to investigate the efficacy of Forth as a target language for Extraction from Agda, in the hopes that Forth may prove to have the potential to be a better target language than the currently used target languages, Haskell and Javascript. Forth is a stack-based, imperative language, meaning that values are pushed and popped from a stack through the use of ’words’ instead of passing and returning values with functions, as is the case in most languages. Agda is a dependently typed, purely functional language. A dependent type is a type whose definition depends on another value, which allows for types with very specific information, such as a ’Vec n’ representing an array of length ’n’. These dependent types are used to write code with more certainty about its correctness and behaviour. Overall, Forth can be used as a target language to compile Agda code, however many of the advantages of Forth are squandered by executing code written and structured with Agda in mind, making it a rather ineffective target language when compared to other solutions such as Haskell.

Cognitive processes have been used in recent years for context sensing and this has shown promising results. Multiple sets of features have shown good performance but no set of features has been determined the best for classifying gaze data. This paper looks at different feature sets and the heterogeneity of gaze signals from subjects and hardware to determine what impacts the performance of the classifiers and what returns the best results. These results are compared with deep learning classifiers using the same data set to determine which performs better.

For the different feature sets, saccade features show great positive influence on the accuracy (88\% accuracy) but fixation features show a significant lower ability to classify correctly (63% accuracy), a combination of some fixation and saccade features show the best results(95% accuracy). The way the data is split, has a huge impact on the performance, splitting the data on every activity gives an accuracy of 95%, while the splitting on subjects only reaches a maximum of 60% accuracy. Deep learning algorithms perform only slightly better at 97% accuracy but dropping down massively (38%) when splitting the data over subjects.

The main conclusions from this research revolve around feature selection and subject bias. Saccade features have the most impact on the classification of activity recognition using eye tracking data. Each subject performs each task in a significantly different way which drastically decreases performance when completely new subject data is tested on a trained classifier. Deep learning classifiers show similar results and back up the importance of the heterogeneity of the data. The evaluation of different types of hardware has not been accomplished in this research due to time constraints.

Classification of sedentary activities using gaze tracking data can be of great use in fields such as teaching, human-computer interaction and surveilling. Conventional machine learning methods such as k-nearest neighbours, random forest and support vector machine might be used to classify such activities, but this requires knowledge about the domain to extract features. Deep learning methods such as a long-short term memory neural network do not require manual feature extraction and are therefore more accessible. To test the feasibility of using these deep learning models, this paper answers the question: Can a long short-term memory neural network (LSTM) be used for gaze-based activity recognition? It was found that a LSTM is highly suitable for user-dependent testing data with an average accuracy of 96.61%. For user-independent testing data the LSTM is less suitable with an average accuracy of 43.34%.

This research proposes a novel method to classify cognitive behavior based on eye-movement data. Most state-of-the-art approaches use conventional machine learning techniques needing manual feature extraction. This experiment explores the possibility of applying deep learning algorithms to cognitive activity recognition for feature extraction and classification of eye-movement data. Convolutional neural networks will be explored in particular. Two neural networks are proposed and optimized using hyperparameter tuning. This research shows that convolutional neural networks can indeed perform cognitive activity recognition. Some neural networks significantly outperform the state-of-the-art methods for known subjects. However, further research is needed to improve performance in classifying activities for unknown subjects.

Sedentary activity recognition is an important research field due to its various positive implications in people’s life. This study builds upon previous research which is based on low level features extracted from the gaze signals using a fixation filter and uses a dataset of 24 participants performing 8 different sedentary activities. The main research question are related to extracting features from the raw data and selecting the most relevant ones which improve the classification accuracy. The novelty of this paper is using dynamic thresholds in the fixation filter to ensure the fixation-specific measurements reported by literature as well as contributing to the human activity recognition (HAR) field by developing an additional low-level gaze feature in combination with the fixation dispersion area. The machine learning (ML) models, Random Forest, k-NN (k-Nearest Neighbour) and SVM (Support Vector Machine), used for the classification task are evaluated using the within dataset evaluation protocol, with cross validation and hyperparameter tuning. The overall recognition accuracy of the Random Forest model is 0.94 (f1-score).

In the current economy, there is an increasing focus on sustainability. Green transport solutions, like rail freight, are becoming more and more popular. We will look into the shunting operations at Kijfhoek shunting yard. This yard functions as the central hub for DB Cargo Nederland and connects the Port of Rotterdam with the hinterland. About 2000 cars are sorted at this yard each week. At the yard, there are 43 parallel classification tracks.
Shunting problems come in many shapes and sizes but are generally hard to solve. To that end, we will use both exact algorithms and heuristics to solve the shunting problem at Kijfhoek within reasonable time. In practice, it is not known at the beginning of the planning horizon which cars will arrive. To that end, we will create general solutions which will be updated over time when new information becomes available. We test how well the solutions perform and/or can be reoptimized with the latest information using a simulator.
We find that our solution approaches can generate solutions for instances with 28 classification tracks of similar quality as solutions found for the same instances with 43 classification tracks with complete information at the beginning of the planning horizon. Furthermore, with incomplete information, we find good solutions with 32 classification tracks.

Inaccurate truck cycle time (TCT) prediction in earthworks impacts construction projects because more equipment and human resources must be added to complete the project. It also increases fuel consumption and emissions from the machinery. However, the current method gives inaccurate prediction because of subjectivity and human error.
This research aims to utilize the historical data for improving the accuracy of TCT prediction in earthworks. Two historical data are explored, such as manual and automated data provided by BAM, using a machine learning approach in which regression techniques: Multi Linear Regression (MLR), Support Vector Regression (SVR), and Artificial Neural Network (ANN).
The result concluded that automated data could develop predictive models because of its quality and variance. ANN develops most predictive models with feature combination one or two, where is distance is the important feature. The benefits of the predictive model are analyzed by comparing them with the traditional method in predicting truck cycle time. The models are more accurate in predicting truck productivity and have lower inefficient truck cycle time than the traditional method. The reduction of inefficient truck cycle time can reduce the cost for fuel and drivers, fuel emission. Models also have intangible benefits to stakeholders, such as gaining partners trust and a better strategic plan to complete the project.
In conclusion, the historical data can improve the prediction accuracy of TCT and give benefits to stakeholders. And practitioners are suggested to raise awareness about the importance of data and improve earthmoving documentation for better predictive models.