PONSINI , Olivier

Omnipresence of computer systems in modern technological applications makes the question of their reliability essential. In this thesis, we investigate equational logic as a foundation for the verification of programs written in an imperative language. Our approach aims at automating the verification of program properties while offering a...

Programs with floating-point computations are tricky to develop because floating-point arithmetic differs from real arithmetic and has many counterintuitive properties. A classical approach to verify such programs consists in estimating the precision of floating-point computations with respect to the same sequence of operations in an idealized...

Abstract interpretation based value analysis is a classical approach for verifying programs with floating-point computations. However, state-of-the-art tools compute an over-approximation of the variable values that can be very coarse. In this paper, we show that constraint solvers can significantly refine the approximations computed with...

Static value analysis is a classical approach for verifying programs with floating-point computations. Value analysis mainly relies on abstract interpretation and over-approximates the possible values of program variables. State-of-the-art tools may however compute over-approximations that can be rather coarse for some very usual program...

Static value analysis is a classical approach for verifying programs with floating-point computations. Value analysis mainly relies on abstract interpretation and over-approximates the possible values of program variables. State-of-the-art tools may however compute over-approximations that can be rather coarse for some very usual program...

Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may dif-fer from the path corresponding to the same computation with real numbers. State-of-the-art tools compute an...

Loop invariants play a major role in program verification and drastically speed up processes like automatic test case generation. Though various techniques have been applied to automatic loop invariants generation, most interesting ones often generate only candidate invariants. Thus, a key issue, to take advantage of these invariants in a...

Safety property checking is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for...

Safety property checking is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for...

International audience

This technical report provides all the source code of the Flasher Manager as well as of the test programs. The Flasher Manager is an industrial application from a car manufacturer that is embedded as a C program in a car computer. The benchmarks are based on four safety properties specified by the Flasher Manager designers.

International audience