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...
Ce papier présente un nouvel algorithme pour la résolution d'une sous-classe de problèmes contraints quantifiés sur le continu (QCSP) pour lesquels les quantificateurs existentiels précèdent les quantificateurs universels. Cette classe de QCSPs possède un remarquable potentiel d'applications dans les domaines de l'ingénierie et de la...
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 significantly differ from the path corresponding to the same computation with real numbers. As a consequence, developers do...
La réduction basé sur l'optimalité (ou RBO) est une technique qui a été proposée pour améliorer les algorithmes d'optimisation globale. Elle cherche à profiter des bornes connues du domaine de la fonction objectif pour tenter de réduire les bornes des domaines des variables et, ainsi, accélérer le processus de recherche d'un optimum global....
Interval methods have shown their ability to locate and prove the existence of a global optima in a safe and rigorous way. Unfortunately, these methods are rather slow. Efficient solvers for optimization problems are based on linear relaxations. However, the latter are unsafe, and thus may overestimate, or, worst, underestimate the very global...
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...
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 differ from the path corresponding to the same computation with real numbers. A common practice when validating such...
This paper introduces a new algorithm for solving a sub-class of quantified constraint satisfaction problems (QCSP) where existential quantifiers precede universally quantified inequalities on continuous domains. This class of QCSPs has numerous applications in engineering and design. We propose here a new generic branch and prune algorithm for...
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...
Les méthodes classiques de résolution de CSPs numériques sont basées sur un algorithme combinant une technique de bissection et un filtrage par consistance locale. En général, le filtrage est basé sur la Hull-consistance ou la Box-consistance. Les algorithmes de filtrage correspondants identifient souvent des trous dans les domaines,...