STATOR

STATic analysis with ORiginal methods

Coordinatore	UNIVERSITE JOSEPH FOURIER GRENOBLE 1    more Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie.
Nazionalità Coordinatore	France [FR]
Totale costo	1˙472˙495 €
EC contributo	1˙472˙495 €
Programma	FP7-IDEAS-ERC Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013)
Code Call	ERC-2012-StG_20111012
Funding Scheme	ERC-SG
Anno di inizio	2013
Periodo (anno-mese-giorno)	2013-01-01   -   2017-12-31

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	UNIVERSITE JOSEPH FOURIER GRENOBLE 1  Organization address address: "Avenue Centrale, Domaine Universitaire 621" city: GRENOBLE postcode: 38041 contact info Titolo: Dr. Nome: David Pascal Cognome: Monniaux Email: send email Telefono: +33 456520368 Fax: +33 456520344	FR (GRENOBLE)	hostInstitution	1˙472˙495.00
2	UNIVERSITE JOSEPH FOURIER GRENOBLE 1  Organization address address: "Avenue Centrale, Domaine Universitaire 621" city: GRENOBLE postcode: 38041 contact info Titolo: Mr. Nome: Yann Cognome: Le Roux Email: send email Telefono: 33476514488 Fax: 33476635956	FR (GRENOBLE)	hostInstitution	1˙472˙495.00

Mappa

 Word cloud

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

 Obiettivo del progetto (Objective)

'Since the beginning of computing, software has had bugs. If a word processor crashes, consequences are limited. If a networked application has security bugs (e.g. buffer overflows), important information (e.g. financial or medical) can leak. More importantly, today's planes are flown by computers, voting machines as well medical devices such as infusion pumps are computerized, and surgeries are performed by robots. Clearly, it is in the best interest of society that such software is bug-free.

BUGS ARE NOT A FATALITY!

Traditionally, software is tested, i.e. run on a limited number of test cases. Yet, testing cannot prove the absence of bugs in untested configurations. Formal methods, producing mathematical proofs of correctness, have long been proposed as a means to give strong assurance on software. They unfortunately had a (not entirely undeserved) reputation for not scaling up to real software. Faster, automated static analysis methods were however produced in the 2000s, which could cope with some specific classes of applications: predicate abstraction, based on decision procedures (e.g. Microsoft's device driver verifier) and abstract interpretation (e.g. Polyspace and Astrée, for automotive, aerospace etc.). Yet such systems are still unusable on more common programs: they reject some program constructs, they give too many false alarms (about nonexistent problems) and/or they take too much time and memory. In the recent years, I and others proposed techniques combining decision procedures and classical abstract interpretation, so as to decrease false alarms while keeping costs reasonable. These techniques are still in their infancy. The purpose how STATOR is to develop new combination techniques, so as to break the precision/efficiency barrier. Since the only way to see if a technique really works is to implement and try it, STATOR will produce a practical static analysis tool and experiment it on real programs.'