ššš 3 Papers accepted @ FLoC 2026!! ššš
Excited to share that three of our papers have been accepted at FLoC 2026, covering automated feedback for Prolog education, data-driven mutation testing for Prolog, and ā¦
Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT
In this paper, we study a neuro-symbolic approach in which an LLM translates a natural language description of an optimisation problem into executable Python code using PySAT. The ā¦
From Brittle LLM Code Reasoning to MaxSAT-Based Verified Repairs @ UCL
In this talk, we examine the limitations of Large Language Models (LLMs) in semantic code reasoning, showing that their predictions may change under semantics-preserving code ā¦
Towards Assessing and Repairing LLM-Generated Code via Model Checking and MaxSAT-Based Fault Localisation @ Dagstuhl 2026
LLMs for code often lack true semantic understanding, evidenced by their instability under semantics-preserving transformations, and we address this by integrating formal methods ā¦
PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C @ P-AI-FM@AAAI 2026
In this talk I will present PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model ā¦
PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C
In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking ā¦
š Paper accepted @ the Post-AI Formal Methods Workshop @ AAAI 2026! š
Iām excited to share that our paper on PyVeritas has been accepted to the P-AI-FM-26 Workshop @ AAAI 2026! š
MENTOR: Automated Feedback for Introductory Programming Exercises
This PhD thesis presents MENTOR, a semantic automated program repair (APR) framework designed to provide Automated Feedback for Introductory Programming Exercises.
Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization
In this paper, we propose a novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance APR for IPAs. Our method ā¦
Model-Based Diagnosis for Software
Localising system faults has long been recognised as one of the most time-consuming and costly tasks in software engineering. Given a buggy system, fault localisation (FL) refers ā¦
š Paper accepted @ AAAI 2025!! š
I am very happy to share that our paper that combines the strengths of both MaxSAT-based fault localisation and Large Language Models, via zero-shot learning, to enhance automated ā¦
Automated Feedback for Introductory Programming Exercises
Delivering valuable and personalised feedback to students remains one of the greatest challenges in programming education, particularly in courses with large enrollments. Providing ā¦
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases @ FM 2024
In this talk I will introduce a novel fault localization approach for C programs with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and ā¦
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
This paper introduces a novel fault localization approach for C programs with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and ā¦
User partitioning for Maximum Satisfiability
The Maximum Satisfiability (MaxSAT) problem is the optimisation variant of the Satisfiability (SAT) problem. Solving MaxSAT efficiently often involves partitioning the set of soft ā¦
UpMax: User partitioning for MaxSAT @ SAT 2023
In this talk I will present a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.