Developing correct concurrent data structures under weak memory models presents significant challenges due to subtle concurrency errors arising from relaxed ordering guarantees and complexities in Safe Memory Reclamation. Existing synthesis methods largely assume sequential consistency, overlooking critical reorderings allowed by realistic architectures.

This thesis introduces a synthesis-verification pipeline that iteratively generates concurrent data structures from partial code specifications using Large Language Models. The pipeline is expanded by integrating an advanced model checker, GenMC, enhanced specifically to verify SMR correctness under weak memory through automaton-based hazard pointer verification. This integration provides memory safety guarantees across diverse execution scenarios.

We evaluate our approach using established concurrent data structure benchmarks, demonstrating rapid convergence to correct implementations, outperforming state-of-the-art methods. These results highlight the pipeline’s effectiveness and scalability, illustrating its potential to support researchers in developing novel, reliable concurrent data structures under weak memory models.

This research paper focuses on the complex domain of alert-driven attack graphs. SAGE is a tool which generates such attack graphs (AGs) by using a suffix-based probabilistic deterministic finite automaton (S-PDFA). One of the substantial properties of this algorithm is to detect infrequent severe alerts while maintaining the context of attacks via the help of sink states and state IDs. This is a modelling assumption that we validate by answering the question driving this research: How does allowing the sink states to merge with other sink states affect the generated alert-driven attack graphs? Our research used a transparent methodology to obtain size, complexity and completeness statistics of the two algorithms. Afterwards, outstanding values in size and complexity allow us to filter insightful attack graphs, subject to head-to-head comparisons concerning their interpretability. We discovered that many remarkable changes happen in the outputted attack graphs, leading to an evident decrease in interpretability and increased loss of context. Concurrently, we do not detect substantial changes in size, complexity and completeness, leading us to believe that it is possible to unlock SAGE's full potential by adding specific thresholds for merging sink states. One proposed constraint is allowing only the merges of sinks at equal distance to the victim node. This alteration leads to similar results in all metrics, including interpretability, where some AGs show improvements.