smackers/smack모듈형 소프트웨어 검증 툴체인으로, C 프로그램의 유계 및 실험적 무계 단언 검사를 위해 LLVM IR을 Boogie 중간 검증 언어로 변환합니다.
SMACK은 모듈식 소프트웨어 검증 도구 체인이자, 자체-완결형 소프트웨어 검증기입니다. 입력 프로그램의 단언문(assertion)을 검증하는 데 사용할 수 있습니다. 기본 모드에서는 루프 반복 및 재귀 깊이에 주어진 경계까지 단언문을 검증하며, 무한 검증을 위한 실험적 지원도 포함하고 있습니다. SMACK은 동적 메모리 할당, 포인터 연산, 비트 연산 등 C 언어의 복잡한 기능을 처리합니다.
내부적으로 SMACK은 LLVM 컴파일러의 널리 사용되는 중간 표현(IR)을 Boogie 중간 검증 언어(IVL)로 변환하는 변환기입니다. LLVM IR을 소싱함으로써 점점 더 많은 컴파일러 프론트엔드, 최적화, 분석을 활용할 수 있습니다. 현재 SMACK은 Clang 컴파일러를 통해 C 언어만 지원하지만, 추가 언어 지원을 위해 작업 중입니다. Boogie를 타겟팅하면 검증, 모델 검사, 추상 해석 알고리즘의 구현을 단순화하는 표준 플랫폼을 활용할 수 있습니다. 현재 SMACK은 Boogie 및 Corral 검증기를 활용합니다.
시스템 요구 사항, 설치, 사용법 및 기타 모든 내용은 아래를 참조하십시오.
SMACK 사용 경험을 듣는 데 매우 관심이 있습니다. 피드백이 있으시면 Zvonimir, Michael 또는 Shaobo에게 연락 주시기 바랍니다.
일반적인 질문은 먼저 FAQ를 참조하십시오.
그 외에 문제가 있거나 누락된 부분이 있으면 이슈를 열어주십시오.
업데이트 소식을 받으려면 SMACK의 Github 페이지를 지켜봐 주십시오.
SMACK 프로젝트는 National Science Foundation, VMware, Amazon, Microsoft Research의 자금 지원을 일부 받았습니다. 또한 University of Utah의 Emulab 인프라를 사용하여 SMACK의 광범위한 벤치마킹을 수행합니다.
