CwicSpec
Aditya Thalang
We built a prototype that conjectures candidate specifications for C functions by generating inputs, observing outputs with KLEE, and searching for equivalences between expressions. Inspired by QuickSpec, the project explores whether theory exploration can be applied to C programs. Our implementation is limited by insufficient search-space pruning.
Thank you for this work!
So much software running today is still based on C –in a Mythos world is has become increasingly important that SWE task e.g. to fix up zero-day problems can be addressed swiftly and thoroughly. I'd recommend adding your project's relevance to wider AI safety to strengthen your framing.
The methods and findings section are very compact: I'd recommend expanding them with more key insights on e.g. the development process, insights the example functions you ran and results overview, etc.
Honest limitations section.
This project has a clear vision and correctly identifies a high-value target in this space. Applying theory exploration to C is an ambitious choice but unfortunately the scope seems too large to make reasonable progress over the course of a hackathon. A much narrower approach focused on MVP / quick wins would have helped with faster understanding and iteration on tractable parts of the problem-space.
The authors presented their claims and process candidly and concisely. A ~null result is useful content to produce and may guide future exploration of the domain. However, the results were extremely sparse, making it difficult to understand progress made in this hackathon. I would have liked to see motivating examples which might show promise, or even rough-and-ready analysis of scaling and traits of success/failure attempts.
Cite this work
@misc {
title={
(HckPrj) CwicSpec
},
author={
Aditya Thalang
},
date={
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


