Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

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

(1)
1

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.

Dates and versions

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

Identifiers

Cite

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⟩

Collections

CEA DRT LIST
48 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More