VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Created by
Haebom
Category
Empty
저자
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
VeriStruct: AI-Assisted Automated Verification for Data Structure Modules
개요
VeriStruct는 Verus에서 단일 함수에서 더 복잡한 데이터 구조 모듈로 AI 기반 자동 검증을 확장하는 새로운 프레임워크입니다. VeriStruct는 플래너 모듈을 사용하여 추상화, 타입 불변량, 사양 및 증명 코드를 체계적으로 생성합니다. LLM이 Verus의 주석 구문과 검증 관련 의미를 오해하는 문제를 해결하기 위해 VeriStruct는 프롬프트 내에 구문 지침을 포함하고, 주석 오류를 자동으로 수정하는 복구 단계를 포함합니다. 11개의 Rust 데이터 구조 모듈에 대한 평가에서 VeriStruct는 11개 중 10개에서 성공했으며, 총 129개 함수 중 128개(99.2%)를 성공적으로 검증했습니다.
시사점, 한계점
•
AI 기반 자동 검증을 데이터 구조 모듈로 확장하는 새로운 프레임워크 개발
•
LLM의 Verus 주석 구문 및 검증 의미 이해도 개선
•
11개의 Rust 데이터 구조 모듈 중 10개에서 성공적인 검증 달성 (99.2% 함수 검증 성공)
