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

특히, 기존의 C 프로그램의 치명적인 오류들이 너무 늦게(테스트 중에) 발견되는 고비용을 개선하고 싶은 경우, 혹은 무결점 C 프로그램들을 짧은 시간안에 자주 개발해내야 하는 경우에 유용한 시스템이다.

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

특히, 그 확인 과정이 또 다른 소프트웨어(프로그램 분석기)를 통해서 완전히 자동으로 이루어진다. 분석기 소프트웨어에 입력으로 들어가는 것은, 검증할 소프트웨어 소스이다.

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

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

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

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