Automated Static Analysis Tools (ASATs) generate a massive volume of non-actionable warnings. To address this, this thesis investigates the performance and resource trade-offs between classical Machine Learning (ML) models and Large Language Models (LLMs) for generating actionability probability scores. Utilizing the NASCAR dataset of over 1.2 million Java warnings, we evaluate optimized classical models (Random Forest and Logistic Regression) against the Claude 4.x LLM family using classification metrics (F1-score, AUC) and probabilistic calibration (Brier scores), supplemented by a qualitative user study of 15 industry professionals. Empirical results demonstrate that an optimized Random Forest yields superior predictive performance (F1-score: 76.85\%, AUC: 0.87) and reliable uncertainty calibration (Brier score: 0.1549), rendering the massive computational overhead of miscalibrated LLMs unnecessary. However, the user study identifies a human-AI feature disconnect: while the Random Forest relies heavily on historical metadata, developers universally demand source code context and severity indicators. Ultimately, an optimized Random Forest provides a significantly more efficient framework for scoring ASAT warnings, provided the scores are tightly coupled with the structural evidence required to sustain human trust. ... Read more

Embedding AllDifferent within Circuit is standard practice for routing problems in Constraint Programming, but in a Lazy Clause Generation (LCG) solver this creates a tension: stronger propagators prune more but produce larger, more situation-specific explanations, yielding learned clauses that generalise poorly. AllDifferent and Circuit have only ever been studied separately, under incomparable conditions, leaving practitioners without an evidence-based choice of AllDifferent propagator inside Circuit in LCG. We close this gap with a systematic experimental evaluation of four propagator variants of increasing strength: a decomposed baseline, a matching-based conflict detector, a full GAC propagator, and a circuit-aware extension of GAC, implemented in the Pumpkin LCG solver and tested on structured geographic and unstructured random-graph benchmarks under fixed and activity-based search. Full GAC (V2) is the strongest choice overall, cutting runtime by up to two orders of magnitude by eliminating conflicting branches before the solver enters them; the theoretically stronger circuit-aware variant fails to improve on it because its extra pruning condition rarely fires in practice. V2's runtime advantage holds even where explanation quality favours weaker propagators, but narrows sharply on unstructured graphs as its clause reusability degrades, showing that propagation strength alone cannot predict LCG performance. We recommend full GAC as the default AllDifferent propagator for Circuit in LCG solvers. ... Read more

Constraint Programming with Lazy Clause Generation (LCG) relies on effective propagation to reduce the search space. We study the integration of strong bridge detection into a circuit propagator, where strong bridges identify edges that must be present to maintain strong connectivity in the graph induced by current domains. Compared to a baseline that only prevents subcycles, this approach substantially reduces search effort, with reductions of up to three orders of magnitude in the satisfaction setting and one order of magnitude in the optimization setting. These gains often translate into runtime improvements, particularly for satisfaction. The extension also produces shorter nogoods, while its effect on LBD is mixed, reflecting more global explanations. Overall, the results demonstrate that identifying necessary edges is an effective way to strengthen propagation and significantly reduce the explored search space. ... Read more

Constraint Programming (CP) solvers rely on propagation algorithms to reduce the search space of combinatorial problems. For graph constraints such as the circuit constraint, infeasibility often depends on global connectivity properties that are difficult to capture using local propagation alone. In this paper, we investigate articulation-based graph reasoning for the circuit constraint in a Lazy Clause Generation (LCG) solver. We introduce propagation techniques based on articulation points and strong articulation points, using connectivity bottlenecks and strongly connected component structure to detect infeasible states and derive additional pruning. We further describe explanation-generation methods that allow these propagations to participate in clause learning within the LCG framework. To evaluate the practical usefulness of this reasoning, we implement the proposed propagators in an LCG solver and compare them against a baseline cycle-prevention propagator on graph instances with varying sizes and densities. The experiments show that articulation-based reasoning substantially reduces search effort and often improves runtime performance on sparse and moderately dense benchmark instances. These results demonstrate that global connectivity reasoning can provide practical benefits beyond traditional cycle-prevention propagation in modern LCG solvers. ... Read more

cDFAs offer a more natural encoding of counting regular patterns—a prevalent problem in timetabling and sequencing—than widely-used DFAs. A cDFA-based propagator for finite domain constraint solving has been shown to solve satisfaction problems faster and make more propagations than the decomposition of a DFA-based regular constraint. This paper extends that algorithm with explanations for lazy clause generation and shows that it often solves satisfaction problems faster than a DFA-based regular constraint both decomposed and propagated, even though the explanations are simple and nogood quality is worse. Additionally, this paper showcases a generator for cDFAs and DFAs that are equivalent to each other to aid comparison of the constraints ... Read more

The regular constraint enforces that a sequence of variables forms a word accepted by a finite automaton, and is widely used in constraint programming (CP) for rostering, timetabling, and puzzle solving. While non-deterministic finite automata (NFAs) offer more compact representations than deterministic finite automata (DFAs), their relative performance within Lazy Clause Generation (LCG) remains underexplored. We adapt existing NFA and DFA-based LCG propagators, using a decomposition-based propagator as a baseline, and evaluate all three under identical solver conditions across instances stratified by DFA-to-NFA state blowup. At low blowup, NFA and DFA solve times are closely matched. At medium blowup, NFA remains faster by a factor of approximately three, and at high blowup it is approximately 22× faster than DFA, with DFA never clearly preferable. Although both compute the same filtering under generalised arc consistency, they can justify prunings differently, and thus are not guaranteed to explore identical search trees. Despite this potential for divergence, clause metrics are identical between NFA and DFA across every blowup bin, a result that may generalise more broadly but warrants further investigation. We also show that the currently used greedy explanations are close to optimal, within one percent of the exact minimum overall and within a few percent for any individual problem type measured. We thus provide the first direct evidence that NFA’s compactness advantage carries over to propagation performance under LCG, establishing it as the default representation for the regular constraint in CP with LCG. ... Read more

Automated test generation is a critical area of research in software engineering, aiming to reduce manual effort while improving software reliability. While substantial work has focused on statically typed languages, dynamically typed languages such as JavaScript remain underexplored despite their widespread use and unique challenges. This thesis investigates the current status of JavaScript test generation by systematically evaluating state-of-the-art search-based and large language model-based tools.

We first analyze existing benchmarks to assess their coverage of representative language features, identifying gaps that limit the ability to fairly compare tool performance. We then construct a curated dataset of real-world JavaScript projects and evaluate the LLM-based tool TestPilot and the search-based tool SynTest using a combination of quantitative metrics (e.g., code coverage, pass rates) and feature based correlation analysis. Our results reveal that TestPilot tends to generate higher coverage (median 27.9\% vs 11.2\% branch coverage) and more readable tests but produces a larger number of failing or low-value test cases, while SynTest generates more stable and focused test suites yet can struggle with complex or dynamic code constructs. Our similarity analysis shows that each approach achieved unique coverage, suggesting complementary strengths.

This study highlights the need for standardized, language-aware benchmarks and introduces a curated dataset and evaluation framework for evaluating JavaScript test generation tools. By systematically comparing search-based and LLM-based approaches, this thesis offers insights into their respective strengths, limitations, and opportunities for hybrid strategies, advancing the state of automated testing for dynamically typed languages. ... Read more

In large-scale engineering environments, efficient issue tracking is essential for timely problem resolution and knowledge reuse. However, manual classification and association of issue reports present scalability challenges, further complicated by inconsistent annotations and the absence of semantic linking mechanisms. This project investigates the application of Natural Language Processing and Artificial Intelligence to automate multi-label classification and discover meaningful semantic associations between technical issues. Over 70 model configurations were evaluated on a real-world industrial dataset, comparing classical models with transformer-based and deep learning approaches. DistilBERT achieved the highest Recall@5 (0.93), indicating strong performance in identifying relevant categories. Classical methods, such as TF-IDF combined with Logistic Regression, also performed well, offering a computationally efficient and interpretable option. For association discovery, approaches including lexical retrieval, embedding-based similarity, clustering-based filtering, and topic modelling were assessed using both quantitative metrics and expert review. Lexical (BM25) and embedding-based (SBERT + Cosine Similarity) methods offer complementary strengths, retrieving overlapping yet distinct sets of associations. Associations identified by both models were rated as useful in over 70% of cases by domain experts, suggesting that agreement between methods may serve as an indicator of relevance. While Copilot provided consistent relevance assessments, its ratings were often higher than those provided by human evaluators and did not always reflect their detailed assessments. These findings highlight the potential of combining lexical and semantic methods with human-in-the-loop validation to support scalable and accurate industrial applicability. ... Read more

Federated Space Public Key Infrastructure (PKI) can offer a scalable foundation for secure and interoperable communications in collaborative space missions. Yet, its deployment faces challenges stemming from resource-constrained assets, architectural complexity, and the transition to post-quantum (PQ) cryptography. Current CCSDS space guidelines rely on the Internet X.509 profile, whose extensive feature set—if left unrestricted—can increase implementation complexity, certificate size (especially under PQ algorithms), and the risk of interoperability issues. In parallel, the IETF C509 Certificates draft emerges as a streamlined subset of X.509 with a compact encoding specifically tailored for constrained environments. This paper provides an empirical comparison between X.509 and C509 to inform space mission designers about the associated advantages and costs of each, specifically when PQ cryptography is incorporated into space PKIs. To help pave the way for interoperability in federated space missions, a minimal certificate profile for space PKI is proposed.

In addition, the work introduces the first open-source native C509 toolkit that supports PQ algorithms and evaluates open-source and proprietary certificate parsers. While the IETF C509 draft proposal reports a size reduction of over 50%, our evaluation confirms approximately 40% savings for classical certificates generated according to our proposed minimal certificate profile. For PQ certificates, the savings plateau at around 200 bytes, rendering the size gains negligible. However, revocation lists consistently achieve a 60% reduction for 30,000 entries, independent of the cryptographic scheme (PQ or traditional). To quantify and compare the software implementation complexity of X.509 and C509, we conduct software complexity analysis using well-established heuristic metrics (e.g., cyclomatic complexity, Halstead metrics, logical lines of code). The findings further highlight the relative simplicity of the C509 parser implementation in software. Defining a standardised certificate profile for federated space would advance interoperability; however, adopting C509 requires carefully balancing modest PQ size savings against software simplification and the uncertainties associated with a draft standard. ... Read more

Probabilistic programming offers an intuitive and expressive way to define statistical models, rendering it particularly effective in modeling problems where uncertainty plays a crucial role.
As adoption increases and models become more expressive, the challenge of effective inference becomes increasingly pronounced.
Effective inference often requires tailoring algorithms to the structure of the underlying model. While many probabilistic programming systems allow users to implement custom inference strategies via programmable inference, this process remains largely manual and heavily reliant on domain-specific expertise, particularly for sampling-based methods.
This paper investigates the use of Satisfiability Modulo Theories (SMT) to automate the generation of tailored, observation-aware proposals for guiding inference within Metropolis-Hastings in Gen, a probabilistic programming system. By reformulating the search for high-likelihood traces as a constraint optimization problem, this work explores whether SMT-based solutions can improve proposal quality and convergence. Empirical results indicate that SMT-derived traces offer a promising starting point for inference but are less effective as an active search heuristic. These findings suggest a new direction for automated, structure-aware proposal generation in probabilistic programming. ... Read more

... Read more

This thesis introduces Lazy Linear Generation (LLG), a novel conflict analysis and learning framework for Constraint Programming (CP) that incorporates cutting planes reasoning. By leveraging cutting planes, our approach learns potentially stronger linear constraints than traditional clausal learning, allowing for more pruning of the search space while benefiting from strong CP propagation.

LLG generates linear explanations for both propagations and conflicts, which are then used in linear inequality-based conflict analysis. When cutting planes reasoning fails to derive a linear constraint, we employ Lazy Clause Generation (LCG) as a fallback mechanism. We present linear explanations for various arithmetic constraints, including less-than-or-equal, not-equal, absolute value, maximum, integer multiplication, truncating division, element, and reified constraints. Additionally, we introduce techniques for dynamically generating auxiliary Boolean variables to encode conditions within linear explanations.

We evaluate an LLG prototype on 952 benchmark instances, demonstrating a median conflict reduction of 10%, increasing to 60% for the 25th percentile. Our results confirm that linear inequalities enable stronger reasoning than clauses and show that integrating CP propagators with linear conflict analysis outperforms employing a fully linear model. Furthermore, we show that a clausal fallback mechanism is crucial when linear analysis fails.

While further research and engineering efforts are required for full integration into CP solvers, our findings underscore the potential of linear learning in CP, paving the way for more effective conflict analysis and solving. ... Read more

Program synthesis aims to solve problems through coding by removing the need to write the programs yourself.
Given the grammar and problem specification, it aims to find a program that adheres to your problem specification.
This is done by iterating over many failing programs until a solution that adheres to the problem specification is found.
Conflict analysis automatically takes these failing solutions and learns new constraints to make the search more efficient.
Unfortunately, many conflict analysis techniques are heavily specialized.
They are difficult to apply to diverse problems or when trying to use a different search algorithm.
In this work, we present a modular framework in which these techniques can be implemented in a generalized way and applied independently to different problems and solvers, while having the ability to share generated constraints and parsed information.
We identify two distinct conflict types and show how to use semantics in conflict analysis effectively.
The framework is evaluated on two diverse domains; it prunes up to 96\% of the search space, where combining techniques can further improve its average effectiveness.
Domain applicability for the techniques has to be considered for optimal framework performance.
Compared to an enumeration solver, the framework shows marginal improvements on a real-world benchmark.
While the framework's overhead needs improvement, its modularity allows for comparison between solvers, problems, and conflict analysis techniques. ... Read more