C 프로그램에서 메모리 접근은 항상 할당된 메모리의 내부에 국한되야 한다. Airac5는 주어진 C 프로그램의 모든 실행 상황을 분석해서, 할당된 메모리를 벗어나서 접근하는 경우(buffer overrun)들을 미리 모두 찾아준다.

프로그램을 실행시킬 수 있는 환경이 준비될 때 까지 오류 검출이 늦춰지는 것은 바람직하지 않다. 테스트는 또 유한개의 입력에 대해서만 제대로 작동된다는 것을 확인할 수 있을 뿐이다. 가능한 입력이 무수히 많다면 테스트는 모든 상황을 커버할 수 없다.

정적 프로그램 분석(static program analysis) 기술은 다양한 이름으로 다양한 수준에서 다양한 필요에 맞추어 고안된 많은 기술들을 모두 포섭한다: "static analysis", "abstract interpretation", "type system", "software model checking", "data-flow analysis", "program logics and proof system" 등.

이 기술은 지난 30년 동안 연구가 무르익어 이제 비로서 실제 오류검증에 적용되기 시작하였다. 우리는 지난 10년 이상 이 분야 연구를 수행해왔고, 지난해 부터 상용을 목표로 개발해 온 시스템이 Airac5이다. 요약해석(abstract interpretation) 기술을 기반으로 한다.

Airac5는 실행시키지 않고 모든 오류들을 소스를 분석해서 찾아준다. "static program analysis"기술의 특징이다.

Coverity의 제품은 목표한 오류(buffer overrun)를 모두 찾아주지도 못하고 허위경보도 있다. Polyspace의 제품은 분석비용이 크고 허위경보가 많다. Airac5는 Coverity가 찾아내는 오류를 포함해서 Coverity가 놓치는 것까지 모두 찾아주고, Polyspace보다는 분석비용과 허위경보가 적다.

Airac5 홈을 방문하면 Airac5 자체의 성능뿐 아니라 Coverity와의 비교 성능을 살펴볼 수 있다.

이러한 허위경보를 0개로 줄이는 것은 불가능하다. 오류라고 판정된 지점마다 허위경보인지 아닌지를 사람이 확인하는 과정은 필요하다.