Search

http://link.springer.com/article/10.1007/s10515-014-0154-2; International audience; 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 expressions. In this paper, we show that constraint solvers can significantly refine approximations computed with abstract interpretation tools. More precisely, we introduce a hybrid approach combining abstract interpretation and constraint programming techniques in a single static and automatic analysis. This hybrid approach benefits of the strong points of abstract interpretation and constraint programming techniques, and thus, it is more effective than static analysers and constraint solvers, when used separately. We compared the efficiency of the system we developed---named rAiCp--with state-of-the-art static analyzers: rAiCp produces substantially more precise approximations and is able to check program properties on both academic and industrial benchmarks.

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 program verification and counterexample generation on real applications. We introduce DPVS (Dynamic Post-condition Variable driven Strategy), a new backjumping strategy we developed to handle an industrial application from a car manufacturer, the Flasher Manager. This backjumping strategy is used to search a faulty path and to collect the constraints of such a path. The simplified control flow graph (CFG) of the program is explored in a backward way, starting from the post-condition and jumping to the most promising node where the variables of the post-condition are defined. In other words, the constraints are collected by exploring the CFG in a dynamic and non-sequential backward way. The Flasher Manager application has been designed and simulated using the Simulink platform. However, this module is concretely embedded as a C program in a car computer, thus we have to check that the safety properties are preserved on this C code. We report experiments on the Flasher Manager with our constraint-based bounded model checker, and with CBMC, a state-of-the-art bounded model checker. Experiments show that DPVS and CBMC have similar performances on one property of the Flasher Manager; DPVS outperforms CBMC to find a counterexample for two properties; two of the properties of the Flasher Manager remain intractable for CBMC and DPVS.

This paper describes SOSSubC: a system for automatically translating programs written in SubC, a simple imperative language, into a set of first-order equations. This set of equations represents a SubC program and has a precise mathematical meaning; moreover, the standard techniques for mechanizing equational reasoning can be used for verifying properties of programs. Part of the system itself is formulated abstractly as a set of first-order rewrite rules. Then, the rewrite rules are proven to be terminating and confluent. This means that our system produces, for a given SubC program, a unique set of equations. In our work, simple imperative programs are equational theories of a logical system within which proofs can be derived.

International audience; 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 over-approximation of the error introduced by floating-point oper-ations with respect to the same sequence of operations in an idealized semantics of real numbers. Thus, totally inappropri-ate behaviors of a program may be dreaded but the developer does not know whether these behaviors will actually occur, or not. We introduce here a new constraint-based approach that searches for input values hitting the part of the over-approximation where errors due to floating-point arithmetic would lead to inappropriate behaviors. Preliminary results of experiments on small programs with classical floating-point errors are very encouraging. * This work was partially supported by ANR VACSIM (ANR-11-INSE-0004), ANR AEOLUS (ANR-10-SEGI-0013), and OSEO ISI PAJERO projects.

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. Constraint solvers have recently been used to significantly refine the approximations computed by such tools. In this paper, we introduce a hybrid approach that combines abstract interpretation and constraint programming techniques in a single static and automatic analysis. First experiments showed that this approach can successfully analyze programs that could not be handled by abstract interpretation or constraint programming tools alone.