11 papers
An AI Approach to Verified Production Cryptographic Libraries
Chuyue Sun, Su Fong, Zhiyi Kuang +5
Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isola…
Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu +2
The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue…
The Luna Bound Propagator for Formal Analysis of Neural Networks
Henry LeCates, Haoze Wu
The parameterized CROWN analysis, a.k.a., alpha-CROWN has emerged as a practically successful abstract interpretation method for neural network verification. However, existing impl…
Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
Anjiang Wei, Tianran Sun, Tarun Suresh +3
Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLM…
Enhancing and Reporting Robustness Boundary of Neural Code Models for Intelligent Code Understanding
Tingxu Han, Wei Song, Weisong Sun +6
With the development of deep learning, Neural Code Models (NCMs) such as CodeBERT and CodeLlama are widely used for code understanding tasks, including defect detection and code cl…
Incremental Neural Network Verification via Learned Conflicts
Raya Elsaleh, Liam Davis, Haoze Wu +1
Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same netw…