DATAVERIF

Temporal Reasoning with Data for Verification

Coordinatore	CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE    more  Organization address address: Rue Michel -Ange 3 city: PARIS postcode: 75794 contact info Titolo: Mr. Nome: Brice Cognome: Kerber Email: send email Telefono: +33 1 47407546 Fax: +33 1 47407521
Nazionalità Coordinatore	France [FR]
Totale costo	372˙353 €
EC contributo	372˙353 €
Programma	FP7-PEOPLE Specific programme "People" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013)
Code Call	FP7-PEOPLE-2011-IOF
Funding Scheme	MC-IOF
Anno di inizio	2012
Periodo (anno-mese-giorno)	2012-08-01   -   2015-07-31

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE  Organization address address: Rue Michel -Ange 3 city: PARIS postcode: 75794 contact info Titolo: Mr. Nome: Brice Cognome: Kerber Email: send email Telefono: +33 1 47407546 Fax: +33 1 47407521	FR (PARIS)	coordinator	372˙353.60

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'The development of formal methods for the verification of computer systems is recognized as a grand challenge by many research institutions. A successful approach for the verification of systems consists in modelling the system to be verified by a mathematical structure and in expressing behavioral properties in a logical formalism. The assumption that programs are finite-state is usually too restrictive and model-checking techniques for infinite-state systems have flourished these last 20 years. Our research program is motivated by the following assessment: most of model-checking techniques to verify infinite-state systems are mainly interested on the control and less on the data values stored by local or global program variables. In this project, the applicant shall develop verification techniques for systems heavily manipulating data, will design relevant formal specification languages to express properties on data, develop algorithms using SMT solvers that are essential for computer-aided verification. This latter method is mastered by the members of the host institution, Analysis of Computer Systems Group at New York University CS Department. In view of expanding the applicant's skills and competencies, the research training objectives are mainly to get a new expertise in an emerging technology mixing verification and automated deduction, to reach a position of professional maturity by initiating a new research team in the return host dedicated to SMT techniques and to provide transfer of knowledge by the supervision of early-stage researchers and by proposing new curriculum in master programmes.'