VERCORS

Verification of Concurrent Data Structures

Coordinatore	UNIVERSITEIT TWENTE    more Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie.
Nazionalità Coordinatore	Netherlands [NL]
Totale costo	1˙306˙500 €
EC contributo	1˙306˙500 €
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-2010-StG_20091028
Funding Scheme	ERC-SG
Anno di inizio	2011
Periodo (anno-mese-giorno)	2011-02-01   -   2016-01-31

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	UNIVERSITEIT TWENTE  Organization address address: DRIENERLOLAAN 5 city: ENSCHEDE postcode: 7522 NB contact info Titolo: Dr. Nome: Marieke Cognome: Huisman Email: send email Telefono: 31534894662 Fax: 31534893247	NL (ENSCHEDE)	hostInstitution	1˙306˙500.00
2	UNIVERSITEIT TWENTE  Organization address address: DRIENERLOLAAN 5 city: ENSCHEDE postcode: 7522 NB contact info Titolo: Mr. Nome: B.J. Cognome: Pals Email: send email Telefono: 31534893702	NL (ENSCHEDE)	hostInstitution	1˙306˙500.00

Mappa

 Word cloud

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

 Obiettivo del progetto (Objective)

'Increasing performance demands, application complexity and explicit multi-core parallelism makes concurrency omnipresent in software applications. However, due to the complex interferences between threads in an application, concurrent software is also notoriously hard to get correct. Instead of spending large amounts of money to fix incorrect software, formal techniques are needed to reason about the behaviour of concurrent programs.

In earlier work, we developed a variant of permission-based separation logic that is particularly suited to reason about multithreaded Java programs with dynamic thread creation and termination, and reentrant locks. The VerCors project will extend expressiveness of the logic, to specify and verify concurrent data structures. The verification logic will be parameterised over the locking policy, so that a high-level specification of the behaviour of a data structure can be reused for different implementations. Thus the implementation of a concurrent data structure can be changed, without affecting correctness of the applications using it.

The logic will also be parameterised with concurrency and synchronisation primitives, so that a logic for a different programming language can be defined as an instance of the general logic. It will also be adapted to reason about programs with benign data races, i.e., data races where the same value is written simultaneously by different threads. Also techniques to generate part of the specifications automatically will be developed. Finally, the logic will be adapted to a distributed setting, where data consistency between the different sites has to be maintained.

All results will be integrated in a tool set that generates and proves proof obligations automatically. It will be validated on realistic case studies.'