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

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834987
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:41 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

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⟩

Share

Metrics

Record views

42