Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT

Résumé

This invited lecture is a survey of our work over the last 12 years or so, dealing with the precise analysis of numerical programs, essentially control programs such as the ones found in the aerospace, nuclear and automotive industry. Our approach is now based on a rather generic abstract domain, based on "zonotopes" or "affine forms" [7], but with some specificities. For instance, our zonotopic domain provides a functional abstraction [16,13], i.e. an abstraction of the input-output relationships between values of variables, allowing for test generation and modular verification [21]. Also, our domain deals with the real number and the finite precision (for instance, floating-point or fixed-point) semantics [14,17]. It is used in practice in FLUCTUAT [20,9,4] to prove some functional properties of programs, generate (counter-) examples, identify the discrepancy between the real number and the finite precision semantics and its origin etc.

Dates et versions

cea-01834987 , version 1 (11-07-2018)

Identifiants

Citer

E. Goubault. Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. Static Analysis. SAS 2013. Lecture Notes in Computer Science, Jun 2013, Seattle, WA, United States. pp.1-3, ⟨10.1007/978-3-642-38856-9_1⟩. ⟨cea-01834987⟩
57 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More