중간 언어의 역할
서로 다른 언어의 프로그램을 각각 별도의 논리 엔진으로 분석하는 대신, 검증에 필요한 정보를 Viper 표현으로 옮길 수 있다. 프런트엔드는 원래 언어의 규칙을 해석하고, 뒤쪽 검증기는 변환된 프로그램의 조건을 처리한다.
메모리를 다루는 관점
값이 무엇인지뿐 아니라 누가 그 위치를 읽거나 바꿀 수 있는지도 표현한다. 이러한 권한 정보는 변경 가능한 자료구조와 공유 상태를 추론하는 데 활용된다. 수학적 자료형, 사용자 정의 술어와 순수 함수도 명세 작성에 사용한다.
검증 기반과 완성된 분석기
Viper를 쓴다는 사실만으로 원래 언어의 모든 기능이 지원되지는 않는다. 번역 과정과 프런트엔드의 지원 범위를 함께 살펴야 한다. 프로그램을 직접 중간 언어로 작성해 새로운 검증 기법을 시험하는 용도로도 활용할 수 있다.