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

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

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

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

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

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

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

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

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

International audience

This report describes experimental results for a set of benchmarks on program verification. It compares the capabilities of CPBVP "Constraint Programming framework for Bounded Program Verification" [4] with the following frameworks: ESC/Java, CBMC, Blast, EUREKA and Why.

International audience

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

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

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

When designing a biological regulatory network, new information or wet experiments can require adding variables or interactions, inside a previously validated model. They can result in complete reconsiderations of established behaviours. Fortunately, formal methods allow for fully automated verification of properties, and TotemBioNet is an...

International audience

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

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.

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