Moving Beyond Specification Validation to Specification Refinement with Mutation Verification
Archie Licudi, Adam Jones
For mutation verification of Dafny code, we evaluate the usage of constraint-solving based filtering of equivalent mutants and LLM analysis of legitimate alive mutants for automating the process of refining the specifications of verified Dafny code from mutations.
This work presents an automated specification refiner that incorporates a mutation generator and a root cause analyzer. Notably, it leverages mutation verification not only to identify weak specifications but also to automatically refine them. The hybrid symbolic-and-LLM architecture is highly effective, utilizing inexpensive solver calls to filter false positives prior to engaging computationally expensive LLM reasoning. Future work could extend this pipeline by integrating other forms of lightweight testing alongside mutation testing.
Mutation analysis is a great way to find bugs in specs and code. This sprint starts from mutdafny and proposes a significant enhancement: remove the mutations that are not useful or are duplicates, and also propose spec refinements. This has the potential to vastly reduce the need for human intervention. Going forward, it would be interesting to see whether logic-based filtering methods can be used instead of using an LLM as a judge, which might increase the soundness (this is proposed in the report but I couldn't see an implementation yet). I imagine further benchmarking would also be needed before deployment, in particular are the spec refinements useful or do they lead to overfitting? But it is on an interesting trajectory.
Cite this work
@misc {
title={
(HckPrj) Moving Beyond Specification Validation to Specification Refinement with Mutation Verification
},
author={
Archie Licudi, Adam Jones
},
date={
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


