Astrée Static Analyzer
Abstract interpretation kullanarak belirli C program sınıflarında run-time error yokluğunu kanıtlamayı hedefleyen statik analizör.
Teknik Bağlam
Astrée, gerçek zamanlı ve safety-critical gömülü C yazılımı için geliştirilen abstract interpretation tabanlı bir analizördür. Hedefi yalnız olası hata örüntüsü bulmak değil, tanımlı program sınıfı ve varsayımlar altında belirli run-time error türlerinin yokluğunu kanıtlamaktır.
Analiz; interval ve ilişkisel sayısal soyutlamalar, fixed-point hesabı ve convergence tekniklerini birleştirir. Sound over-approximation hata kaçırmamayı hedeflerken false alarm üretebilir.
Sınırlar
Garantinin kapsamı desteklenen C özelliklerine ve çevre varsayımlarına bağlıdır. Resmi Astrée açıklaması hedeflenen program sınıfında recursion ve dynamic memory allocation bulunmaması gibi sınırlar tanımlar.