COLLAVIZZA , Hélène

This report is the user manual of TotemBioNet available at : https://gitlab.com/totembionet/totembionet. TotemBionet is a tool dedicated to parameter identification for Biological Regulatory Networks (BRN), using the discrete formalism of René Thomas. Given a BRN and some properties on the dynamics of the system, TotemBionet outputs all the...

This habilitation thesis presents my contributions to the formal verification of processors and programs, and to constraint programming. Formal verification of hardware and software is crucial for the safety of critical systems, is an important economic issue and remains a challenge for research. The formal methods we explored for the...

A novel approach to program verification combining constraint programming methods with theorem proving is proposed. Starting from an initial symbolic state and precondition, a program is symbolically executed along all feasible paths and then a post-condition is proved or refuted on the final states. Symbolic execution is by mecha-nised...

International audience

We introduce in this paper LocFaults, a new flow-driven and constraint-based approach for error localization. The input is a faulty program for which a counter-example and a postcondition are provided. To identify helpful informa-tion for error location, we generate a constraint system for the paths of the control flow graph for which at most k...

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...

On ne compte plus le nombre de fois où les chercheurs en méthodes formelles pour le génie logiciel ont entendu cette plaisanterie : « Les méthodesformelles ont toujours été l'avenir de l'informatique... et le resteront toujours ! ». Dans ce chapitre nous montrons que les méthodes formelles sont le présent de l'analyse des réseaux de régulation...

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...

Dans cet exposé, nous présentons notre algorithme amélioré de localisation d'erreurs a partir de contre-exemples, LocFaults, basé sur la programmation par contraintes et dirigé par les flots. Cet algorithme analyse les chemins du CFG (Control Flow Graph) du programme erroné pour calculer les sous-ensembles d'instructions suspectes permettant de...

We introduce in this paper a new CP-based approach to support errors location in a program for which a counter-example is available, i.e. an instantiation of the input variables that violates the post-condition. To provide helpful information for error location, we generate a constraint system for the paths of the CFG (Control Flow Graph) for...

Ce chapitre démontre que la modélisation des réseaux de régulation biologiques est grandement facilitée par des méthodes symboliques de vérification formelle comme le model-checking et les preuves en logique de Hoare. Il présente une méthodologie complète de modélisation formelle où les approches logiques classiques du génie logiciel s'adaptent...

We introduce in this paper a new CP-based approach to support errors location in a program for which a counter-example is available, i.e. an instantiation of the input variables that violates the post-condition. To provide helpful information for error location, we generate a constraint system for the paths of the CFG (Control Flow Graph) for...

International audience

This paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores to represent both the specification and the program and explores execution paths of bounded length nondeterministically....

This paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores to represent the specification and the program and explores execution paths nondeterministically. The input program is...