Publications

An extended empirical study evaluating LLM-generated specifications for the VeriFast static verifier, following up on our earlier FORGE 2025 work with a broader set of models and a deeper analysis of specification quality.

Cross-regional LLM inference is bottlenecked by the network cost of shuttling activations between distant data centers. This paper introduces a learned activation-compression approach that reduces that cross-region communication cost while preserving inference quality, enabling more network-efficient multi-region deployment of large models.

Static verification tools like VeriFast require developers to hand-write formal specifications, which is a major barrier to adoption. This paper evaluates whether GPT-4o can generate fully accurate specifications that VeriFast can verify, progressing from baseline prompt engineering to chain-of-thought (CoT) reasoning, prompt chaining, and few-shot prompting. We categorized the VeriFast benchmark suite, built tailored input datasets for testing, and designed a qualitative analysis methodology to assess output correctness, syntactic validity, and model failure modes — offering an early look at how far off-the-shelf LLMs are from generating machine-checkable proofs.