Recent advances in LLMs have transformed AI coding assistants from simple autocompletion tools into conversational partners that support a wide range of development tasks through natural language interaction. While this shift promotes closer human-AI collaboration, this also places a burden on developers to craft precise prompts and integrate sufficient context to accomplish their task.
To address this, there is growing interest in proactive AI systems that can anticipate developer intent and surface timely, contextually relevant suggestions - potentially revealing insights developers might not have considered.

However, existing research on proactive coding assistance has largely been confined to controlled, experimental settings, leaving open questions about its effectiveness and integration in real-world development environments.

In this work, we design and implement a proactive AI assistant within JetBrains Fleet, a polyglot enterprise IDE. Our system signals AI activity via in-editor cues and delivers context-aware code improvement suggestions via a chat interface. We adopt heuristics based on IDE activity to determine when it is timely to intervene, during various stages across the development workflow: formulating needs, idea execution and committing changes.
Lastly, we conducted a five-day in-the-wild study with 18 professional developers to evaluate its impact on user experience and engagement patterns.

Our findings demonstrate that timing is a critical aspect influencing perceived value of proactive AI assistance.
Suggestions delivered at natural workflow boundaries (e.g. post-commit) achieved the highest engagement, while mid-task interventions were often dismissed.
The consistent engagement trends (and voluntary continued use) indicate strong potential for integrating proactive AI into everyday software engineering workflows.
Our study not only underscores the feasibility and practical value of proactive assistance in enterprise development environments, but also provides actionable design insights for future tools.
While challenges remain - such as improving suggestion relevance and supporting diverse user preferences - these highlight important directions for advancing adaptive, intent-aware proactive systems that can further enhance developer workflows.

Formal verification of software can provide a more rigorous guarantee of correctness compared to conventional software testing methods. However, doing this by hand requires substantial effort and is often impractical. To combat this, various verification tools have been developed in recent decades to at least partially automate this process. In this paper we explore Why3, a tool for deductive program verification, by implementing and verifying the A* algorithm. We find that Why3's expressive language allows for easy implementation and verification of A*. However, we also find that it has a significant learning curve and requires some knowledge on formal verification to use. In spite of this, we find it is a useful tool for automated verification.

Large Language Models (LLMs) are increasingly used for code-centric tasks. However, their training data often exhibits data smells that may hinder downstream quality. This research focuses on the “Uneven Natural Languages” smell and the presence of non-English text in source code and investigates its effect on LLM-based code generation and summarisation. We construct a three-stage (Detection, Generation, Evaluation) pipeline that annotates every character in a file with its predicted language using Tree-sitter, FastText, and pycld2; masks target spans via causal masking and Fill-in-the-Middle (FIM) and prompts using three chosen models (SmolLM2, StarCoder 2, and Mellum-4B). The Heap dataset is used for the pipeline; however, this research only focuses on the Java subset of the Heap.

In 3.35 million Java files, we find that English tokens account for more than 90\% of comments, strings, and identifiers, while Chinese, Spanish, Portuguese, and French form a long-tailed minority. Despite this skew, LLMs achieve marginally higher BLEU, METEOR, ROUGE, and Exact Match scores when non-English elements are present or masked. Mellum consistently yields the most fluent continuations; StarCoder 2 retains broader token recall; SmolLM2 lags on both axes, reflecting its smaller capacity.

Our publicly available code enables reproducible assessment of multilingual data smells and lays the groundwork for cleaner, language-aware pre-training corpora and more robust multilingual code assistants.

Formal verification promises stronger correctness guarantees than conventional testing, yet it is often perceived as too costly or specialised for everyday software development. This thesis investigates whether SPARK — Ada’s provable subset — can deliver industrial- strength verification for representative algorithms and concurrent systems. Two separate questions guided the work: how well does SPARK work with (RQ1) sequential algorithms; and (RQ2) concurrent systems.
We implemented and formally proved insertion sort, quick-sort, and a generic statically-allocated hash-map to SPARK’s highest assurance level, achieving full functional correctness, as well as two concurrent case studies: a Publisher / Subscriber channel and a novel IO multi-reactor pattern runtime task scheduler, where we combined SPARK with TLA+ model checking to capture liveness and safety properties that SPARK cannot express directly. Across all sequential examples, proof overhead averaged ratios of 6–10 lines of specification, while for the concurrent case-studies, the TLA+ models averaged ratios of 1.7 lines, per every line of executable code.
The study shows that (i) SPARK is practical for non-trivial sequential algorithms, unless they make use of the heap; (ii) concurrency still requires external formalisms, but the combination remains tractable; and (iii) careful specification design, not solver performance, is the dominant cost driver. These findings confirm that correctness-by-construction is attainable within undergraduate project scope and provide quantitative benchmarks for future work.

Formal verification is a stricter way of ensuring correctness of a program, but sitting down
and writing the proof yourself is often time-consuming. SMT solvers try to automate parts of this
process. This paper aims to explore Dafny, a programming language and verifier that uses an SMT
solver underneath to do this verification. This paper will go over its logical foundations, and how
it can be used to verify an in-place selection sort algorithm as well as a key-value store. It will
also explore a feature of Dafny that allows the user to compile to other languages, and will discuss
its usefulness in the industry. Verifying the sorting algorithm was very straightforward while the
key-value store posed some problems. However, Dafny itself seems to be very straightforward
to program in. Its ability to compile to other languages leaves a lot to be desired. While the
compiled code is fully functional, the code is barely readable and less than ideal to work with. A
further study discussing Dafny’s ease of use compared to other tools could be conducted to see if
the lacking compiler could outweigh having a native verifier specifically designed for a high-level
programming language.

Formal software verification is an important task for ensuring software correctness, especially in safety-critical systems. One method of formal verification is automated theorem proving, where one defines their program as a set of axioms and its correctness criteria as conjectures. We investigated the suitability of Vampire, an automated theorem prover, for formal verification by analyzing the logical foundations and performing case studies. In these case studies, we implemented Selection Sort and a Key-Value Store to observe what could be represented and proven. We were unable to prove the correctness of Selection Sort, but were able to prove most properties of a Key-Value Store. We discuss the capabilities and limitations of Vampire for formal software verification, namely that it is able to prove many properties of the functions we defined, unless they are heavily reliant on inductive definitions or too general with respect to the axioms. We believe that Vampire's inductive capabilities are currently insufficient for our use case. We reflect on the experience of using Vampire from the perspective of the average computer scientist and give suggestions for further documentation. We then discuss related work, including using Isabelle, another ATP and proof assistant, to reason about sorting algorithms and a Key-Value Store. Finally, we give suggestions for future work, such as rewriting the Key-Value Store in SMT-LIB, a language used as input for SMT solvers.

KeY prover has been used to verify parts of the OpenJDK library and Norwegian election software, making it one of the most capable tools for formally verifying Java programs. However, an intuitive explanation of its theoretical foundations, capabilities and limitations is not available and the tool itself has a steep learning curve. This greatly increases the amount of effort to understand the tool sufficiently well to evaluate its suitability for ones needs. Here we implement two case studies to develop an intuition for the working of the tool in practice, exploring what properties can or cannot be expressed as specifications and what verifying correctness with KeY means. We find that the learning curve for KeY is even steeper than expected and conclude that it can be used to verify very complex functional and even some non-functional properties of sequential Java 7 code, conditioned on the capabilities of the user.

In the realm of software development, commit messages are vital for understanding code changes, enhancing maintainability, and improving collaboration. Despite their importance, generating high-quality commit messages remains a challenging task, with existing methods often facing issues such as limited flexibility and high training costs. This paper addresses the research gaps in automated commit message generation (CMG) by exploring the capabilities of large language models (LLMs) in this domain. We specifically investigate the potential of the prompt engineering method to enhance LLM performance compared to state-of-the-art (SOTA) techniques such as RACE.

Our research begins with a comprehensive literature review of CMG methodologies, focusing on the effectiveness of various message formats and the limitations of existing approaches. To fill the gap, we introduce a unified commit message formats dataset and evaluate the previous LLM-based method on the dataset, utilizing the GPT model as a representative example of LLMs. By comparing the LLM zero-shot method with previous retrieval-based and hybrid methods, we provide a detailed analysis of the strengths and weaknesses of LLM-based approaches.

We further explore the impact of different retrieval augmented generation (RAG) configurations on CMG performance and investigate what constitutes a good demonstration of the LLM RAG method for the CMG task. That is followed by proposing a new prompt engineering method called Adaptive Retrieval Augmented Generation With Commit Type Classification And Partitioned Retrieval (ARC-PR), which incorporates a classification module and a database partitioning module to the LLM RAG system. Validating through comprehensive testing on the unified message format dataset, our experiments demonstrate that the proposed method shows significant improvements in message effectiveness compared to the previous LLM-based methods and in the aspects of informativeness, message format consistency and the balance between precision and recall, our method surpasses the state-of-the-art methods in the field. Further generalizability study illustrates the robustness of our proposed method. With the introduction of human evaluation, we further confirmed the superiority of our proposed method over the state-of-the-art methods in terms of informativeness and expressiveness.

In summary, this study makes several key contributions: it provides a thorough comparison of previous LLM-based methods with existing techniques, proposes an enhanced LLM prompt engineering approach specifically tailored for commit message generation (CMG) tasks that address the issue of low informativeness and expressiveness seen in past state-of-the-art methods and demonstrates performance that surpasses other LLM-based methods.

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.

While most large language models (LLMs) are powerful, they are primarily designed for general purposes. Consequently, many enterprises and institutions have now focused on developing domain-specific models. In the realm of education, an expert LLM can significantly enhance students' ability to find information more effectively and reach their learning goals. Nevertheless, the training of such expert models in education remains largely unexplored. This study explores this research gap by developing a framework to transform semi-structured educational web data into structured datasets and perform instruction tuning on foundation models. Additionally, we conduct a comprehensive performance analysis to determine how various training factors affect model performance.

We first employed a systematic and cost-effective approach involving web data extraction, data cleaning, validation, task design based on student surveys, and automated instruction instance generation using LLMs. Human evaluations confirmed the quality, especially the relevance and accuracy of these datasets.

This study then investigates the impact of various training techniques on domain-specific educational large language models (LLMs) performance. Our experiments reveal that further pre-training enhances model performance, especially with domain-specific terminology, although the performance gains decrease as the dataset size increases. Furthermore, multi-task training also improves model relevance, accuracy, and clarity, but less correlated tasks and datasets can present challenges. These challenges include increased complexity and potential degradation in performance due to the model having to switch between diverse tasks. Lastly, this study conducts a comparative analysis of different models and it highlights trade-offs between computational resources and performance.

The findings demonstrate that a structured approach to dataset generation and strategic training can effectively develop domain-specific LLMs in education. This research benefits the development of educational LLMs and provides a foundation for future researchers to build more specialized models in various domains.

Large Language Models (LLMs) have gained a lot of popularity for code generation in recent years. Developers might use LLM-generated code in projects where the security of software matters. A relevant question is therefore: what is the prevalence of code weaknesses in LLM-generated code, and can we use LLMs to detect them? In this research, we generate prompts based on a taxonomy of code weaknesses and run them on multiple LLMs with varying properties. We evaluate the results on the existence of insecurities both manually and by the LLMs themselves. We can conclude that even when LLMs are not provoked and asked benign realistic requests, they often generate code containing known software weaknesses. We find a correlation between model parameter size and the percentage of secure answers. However, they are exceptionally successful in recognizing these insecurities themselves. Future work should focus on a wider set of models and a larger set of prompts, to get more results on this subject.

In recent years, Large Language Models (LLMs) have significantly advanced, demonstrating impressive capabilities in generating human-like text. This paper explores the potential privacy risks associated with Large Language Models for Code (LLMs4Code), which are increasingly used in various sectors. These models, while beneficial for tasks such as code generation and understanding, may inadvertently expose sensitive information contained in their training datasets. We investigate the specific types of personally identifiable information (PII) that can be leaked and explore targeted and untargeted attacks with diverse prompting styles under which these leaks occur. Our analysis reveals that LLMs4Code can leak PII with the targeted attacks, emphasizing the need for robust privacy-preserving measures. This research contributes to the ongoing discourse on AI ethics and privacy, providing insights into the safety of various prompting conditions under targeted and untargeted attacks. Future work should focus on running the experiment with more diverse parameters, implementing more advanced PII detection techniques, and testing a broader range of models to enhance the generalizability of the findings.

The advent of transformer architectures revolutionized natural language processing, particularly with the popularity of decoder-only transformers for text generation tasks like GPT models. However, the autoregressive nature of these models challenges their inference speed, crucial for real- time applications and resource-constrained environments. Memory bandwidth is a significant bottleneck, especially in autoregressive decoding, where constant loading of large key and value tensors dominates. The Multi-Query Attention (MQA) architecture was proposed to reduce memory access by shrinking the key-value cache, enhancing infer- ence speed at the cost of generation quality. Grouped-Query Attention (GQA) was introduced to mitigate this quality decline, serving as an interpolation between Multi- Head Attention (MHA) and MQA. We explore the trade- offs between inference speed and quality in decoder-only models by experimenting with various proportions of query groups relative to attention heads during pre-training. Additionally, we investigate the impact of reducing the size of key and value vectors compared to GQA and explore a hybrid method combining GQA with shortened key-value vectors. This study aims to expand the list of possible trade-offs and help select an optimal architecture based on specific needs.

Effective onboarding in software engineering is critical yet challenging due to the rapid evolution of technologies, languages, frameworks, and tools. Traditional exploration, documentation and workshop-based onboarding methods tend to be expensive, time-consuming and can get outdated very fast in large, complex projects.

In this thesis, we introduce a novel solution: the Onboarding Buddy system which uses large language models (LLMs) and retrieval augmented generation (RAG), enhanced by an automated approach for chain-of-thought (CoT) that improves onboarding for new and existing developers. It integrates natural language explanations available in the development environment with relevant information, code explanations, and project-specific guidance. The system architecture is agent-centric, including contextualization, onboarding agents, instruction step processors and message enhancement agents that cooperate in delivering comprehensive, customized support with minimal reliance on human mentors.

While effective in supporting the completion of tasks and reducing stress related to onboarding, feedback also revealed some areas for improvement, like better context awareness, explicit instructions, improved technical stability, and UX adjustments. In general, Onboarding Buddy is an excellent promise to smoothen the onboarding process and therefore increase developer productivity and job satisfaction.

The experimental results demonstrated the system's effectiveness: participants spent an average of 175 minutes actively engaged in the IDE, completed tasks with nearly 100\% accuracy, and gave high helpfulness ratings (3 out of 4). Task completion times averaged 50 minutes, with simpler tasks taking around 28 minutes and complex ones requiring 67 minutes. User feedback showed high satisfaction (3.35/4 for understanding, 3.15/4 for accuracy) and strong interest in such solutions (7.75/10). Interestingly, more experienced developers spent more time on tasks, suggesting a deeper exploration of the codebase. A strong positive correlation (0.70) between system usage frequency and perceived helpfulness indicated that increased engagement led to better outcomes.

In other words, while there are areas for improvement, such as context awareness and processing complex tasks, this research proves that LLM-based onboarding solutions are feasible and can have significant positive impacts on the software engineering onboarding process, thus laying the foundation for future progress in automated developer support and knowledge sharing for software development.