COVERIF Project Meetings

Meeting 1 (4th April, 2016):
Meeting 2 (23rd September, 2016):

  • Filling the gap between the standard splitting strategy and
  • In Constraint Programming (CP), to solve a Constraint Satisfaction Problem (CSP),
    solving methods alternate two phases: propagation and exploration. In continuous
    solving, the propagation phase computes an over-approximation of the solutions and
    the information that can be gathered during this phase are lost in the exploration
    phase. We propose a new splitting strategy, relying on the propagation phase.
  • A Concoction of Zonotope Abstraction and Constraint Programming
    for finding an Invariant
  • Synthesizing an invariant is a key concept in formal verification ensuring
    correctness of programs and finding bugs, e.g., the program variables
    staying within some bounds. The standard method for finding an invariant
    is to look for inductive invariant, which is a stronger form of invariant.
    This work deals with the challenges associated while combining abstract
    interpretation (zonotopes) and constraint programming for infering
    inductive invariants.
  • Estimation de WCET : analyse haut-niveau avec Interprétation abstraite et
    Programmation par contraintes
  • Nous nous intéressons au problème du
    WCET qui consiste à calculer ou estimer le pire temps d’exécution d’un programme. Nous propo-
    sons une méthode qui mélange analyse statique et programmation par contraintes. L’originalité
    de la méthode est de traduire différentes informations venant d’analyses du programme en pro-
    blèmes de satisfaction de contraintes dont il faut compter les solutions. La méthode proposée
    adapte un solveur de contraintes, utilise un interprète abstrait et reformule les contraintes pour
    résoudre le problème. La méthode a été implémentée avec l’analyseur statique SawjaCard et le
    solveur de contraintes AbSolute avec des résultats prometteurs.
  • Estimation de WCET : analyse haut-niveau avec Interprétation abstraite et
    Programmation par contraintes
  • On finding program input values maximizing the rounding-off error
    Evaluating expressions on floating point numbers can produce results which are far from the
    expected result on real numbers. Such a behaviour is one of the main failures of programs
    handling floating point numbers. We present a new method for generating a critical test cases.
    Our method try to maximize the rounding error for a given expression using a greedy algorithm.
    The bulk of our contribution is the maximization of the rounding error on elementary operations.