코어와 언어 구현 구분
공통 코어에 메모리 모델 구현과 소스 언어를 GIL로 옮기는 컴파일러를 제공하면 특정 언어용 구성을 만들 수 있다. 따라서 프레임워크 자체의 기능과 개별 언어 지원의 범위는 구별해야 한다.
프로그램의 부분을 조합하기
조합적 분석은 프로그램의 부분에 관한 추론을 결합하는 접근이다. Gillian은 분리 논리의 아이디어에서 영향을 받은 기호 실행 기반을 사용한다. 어떤 실행이 올바른지뿐 아니라 잘못된 동작에 관한 추론도 관심 대상으로 삼는다.
구성별 의미 확인
저장소에는 CompCert-C와 ES5 JavaScript를 위한 구성, 연구와 교육용 작은 언어의 구성이 포함된다. 이름에 특정 언어가 있다는 사실만으로 최신 언어 전체를 처리한다고 가정하면 안 된다. 사용하는 구성의 의미론과 지원 기능을 먼저 확인한다.
관련 문서
Viper 검증 기반 / VeriFast / KLEE / Boogie