Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition.

This thesis investigates the potential of basing a program synthesis system on a de-
pendent type theory. This is an attractive research direction because it allows a very
flexible range of specification to be expressed within the same framework. We im-
plement a prototype of a search algorithm driven by unsolved constraints typically
generated during dependent type checking. We encode a range of synthesis prob-
lems from literature in our system, showcasing how it can be used for expressing
the specification and synthesizing programs that manipulate data. We empirically
establish the effect of constraint-directed aspect of our approach on performance,
based on the encoded problems.

This thesis investigates the enhancement of sentence decomposition in Large Language Models (LLMs) through the integration of linguistic features, including constituency parsing, dependency parsing, and abstract meaning representation. Traditional decomposition methods, which often rely on rule-based approaches, struggle with highly intricate sentences. By incorporating detailed linguistic features and employing reasoning steps and supervision in prompts, we aim to improve the comprehension and decomposition capabilities of LLMs. Experimental results show that integrating these linguistic features has the potential to improve decomposition performance. However, these enhancements also introduce new error types and increase computational costs. This study identifies several error types in the programs generated by LLMs, including format, decomposition, and conversion errors, emphasizing the need for further refinement in model training and prompt design. This research lays a step toward more accurate and efficient processing of complex sentences in LLMs, encouraging ongoing development and optimization in this field.

LLM (Large Language Model) powered AI (Artificial Intelligence) assistants are a popular tool used by programmers, but what impact do they have? In this thesis we investigate two such tools designed by JetBrains: AI Assistant and FLCC (Full Line Code Completion).
We collected over 40 million actions - including editing, code executions, and typing - in the form of metric data spread out over 26 thousand users. With this data, we look at how user behavior changes when assisted by AI Assistant or FLCC.

Users spent more time in their IDEs (Integrated Development Environment) and typed more when assisted. In most cases, we see a decline in (manual) testing, or at best an equivalent level. And how do multi-programming language benchmarks reflect acceptance rates by users for these respective languages? There seems to be no real correlation between these benchmark results and what users accept in their generations, but the available benchmarks are also limited.

In the end, more research is required to put these results in perspective, for now, it is still up in the air whether the changes in user behavior are positive or negative. But relating this to existing works the impact seems mostly positive on users of AI Assistant and FLCC.

It is possible to improve the performance of planners by modifying the PDDL domain of a problem. The goal of this research is to implement this to the domain of the Train Unit Shunting Problem (TUSP). The research question we attempt to answer is: To what extent can we improve planner performance by optimizing the PDDL domain of TUSP? The main contributions of this research are: a formalization of the TUSP and its constraints in PDDL terminology, a comprehensive evaluation of the performance of planners on the PDDL domain of TUSP, provide general approaches and techniques that can be used to optimize a PDDL domain, and provide insights into the relationship between the performance of planners and PDDL domain properties. To answer the research question, we measure the performance of the planners in terms of execution time, plan quality, and problem solvability. We modified the domain by combining actions such that the number of computations is decreased and by introducing action costs. With these modifications, we found a decrease in planner execution time and an increase in plan quality. We found no difference in problem solvability. Therefore, we can conclude that we can indeed improve the performance of planners by implementing these modifications to the domain of TUSP.

The increased heat on an integrated circuit is a limiting factor for the performance and lifetime of a chip. The increased power density on chips resulted in increased heat and the formation of non-uniform hotspots. Earlier research has shown that the package design and layout of package components in flip-chip design can influence the thermal heat distribution on a chip. Especially the copper pillars play a role in the distribution of heat on a chip. These pillars can reduce the maximal temperature of a hotspot when placed correctly. Designing a pillarmap that adheres to manufacturing rules can be lengthy and complex. Therefore, pillarmaps are currently not optimised for thermal behaviour. The default strategy is to place them in a grid. This research aims to automatically optimise pillarmaps for thermal heat distribution with the use of artificial intelligence. Pillarmaps are optimised using the theoretical behaviour of heat in packages combined with Stochastic Hill Climbing and Squeaky Wheel Optimisation techniques. The layouts are automatically re-simulated in a finite elements simulation tool when needed. The optimisation strategies are tested on experimental setups with single and dual hotspots. The optimisation strategies are also evaluated on an actual product, but limitations on pillar placement reduced the effect of the optimisation techniques. Also, the influence of different pillar diameters on an optimisation strategy is discussed. The optimisation techniques can reduce hotspots and improve the heat distribution in a scenario with multiple hotspots. The success of the optimisation techniques is subject to the amount of freedom they have to change pillar locations and where the hotspots are on the chip.

The increasing global food demand, accompanied by the decreasing number of expert growers, brings the need for more sustainable and efficient solutions in horticulture. Consultancy company Delphy aims to face this challenge by taking a more data-driven approach, by means of autonomous growing inside the greenhouse. The controlled environment of greenhouses enable data collection and precise control. Delphy's current solutions focus on the needs of the crop, but a grower also needs to consider the economic aspect of taking certain decisions on the greenhouse climate. A potential method for solving this complex problem is Constraint Programming (CP). In this work, the applicability of CP for the greenhouse economic optimal control problem will be studied. The contributions of this work are threefold; First, the greenhouse climate is modelled with Long Short-Term Memory (LSTM) and Temporal Convolutional Network (TCN) machine learning models. Secondly, an LSTM model is embedded into a CP model. Lastly, the profit of the grower is optimised through this CP decision support system (DSS). The performed experiments show that both types of time-based machine learning models can model greenhouse temperature and humidity deficit with reasonable accuracy, while light and CO₂ are harder to predict. The correctness of the LSTM-in-CP embedding is validated. The implemented DSS is not yet practically applicable, as the search space is too large to come to reasonable results for realistic instances. For small instances however, the DSS is able to improve the decisions of the grower, demonstrating the potential of using CP for economic greenhouse decision making.

In this thesis, we have defined a symbolic execution technique to automatically generate test suites for programs written in functional programming languages that can find the behavioural differences between a reference implementation and a set of potentially different implementations. Our symbolic execution technique uses a constraint solver in order to find a model that satisfies all constraints that together represent an execution path through the program. Furthermore, our technique utilises manually defined budget constraints to guide the symbolic execution to more interesting areas of the programs. These budget constraints define an initial budget that dictates when the symbolic execution terminates, and a set of costs associated to certain operations such as calling (specific) functions or performing (specific) pattern matches. This allows the symbolic execution to deplete budgets faster when it explores functions or branches of a program that are deemed "unlikely to be interesting". This results in less system resources being used on exploring these uninteresting execution paths, and instead allows for exploration of deeper paths in more interesting areas of the programs. Our budget constraint optimisation strategy works alongside other well-known optimisation strategies for symbolic execution such as early branch pruning and reusing intermediate results, more commonly known in the field of symbolic execution as compositioning.

In order to perform our symbolic execution on functional programs, we have defined a variation of Control Flow Graphs (CFG) for functional programming languages which allow modelling the execution flow between the different expressions that form the body of functions in functional programming. Additionally, our technique uses a constraint solver in order to find what paths through the program are feasible and to generate inputs that will lead to the execution of said paths. To allow us to specify these constraints on a higher-level, we have defined an intermediate Domain Specific Language (DSL), which can be transformed into a lower-level language understood by the constraint solver. We refer to this DSL as our Intermediate Constraint Language (ICL). Our ICL supports working seamlessly with type systems that allow inheritance, rather than only supporting Algebraic Data Types (ADT).

Furthermore, we have developed a symbolic execution engine for programs written in a pure and functional subset of the Scala programming language. This symbolic execution engine implements our proposed symbolic execution technique alongside the other described optimisation techniques. We have used this implementation in order to measure the effectiveness of our symbolic execution technique. In order to do this, we have used our technique in a scenario to automatically generate test suites for real student submissions of introductory assignments to functional programming. We have performed a comparison between the obtained branch coverages and mutation scores with our technique and the manually written test suites that have been used for multiple years. Finally, we have reflected on the feasibility of using this approach in practice by looking at the execution time and the number of inquiries to the constraint solver, required to generate test suites that are able to find an adequate number of errors.