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

E. Goubault (1)

1 DILS - Département Ingénierie Logiciels et Systèmes

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.

Keywords: Abstract domains; Abstract interpretations; Finite precision; Functional abstractions; Functional properties; Modular verification; Numerical programs; Test generations; Abstracting; Automotive industry; Semantics; Static analysis

Domains: Computer Science [cs]

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⟩