CONAN

Model Checking and Synthesis for Concurrent Software

Coordinatore	UNIVERZITA KOMENSKEHO V BRATISLAVE    more  Organization address address: SAFARIKOVO NAM 6 city: Bratislava 1 postcode: 81499 contact info Titolo: Dr. Nome: Rastislav Cognome: Kralovic Email: send email Telefono: +421 260295470 Fax: +421 2 65427041
Nazionalità Coordinatore	Slovakia [SK]
Totale costo	100˙000 €
EC contributo	100˙000 €
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-2010-RG
Funding Scheme	MC-IRG
Anno di inizio	2013
Periodo (anno-mese-giorno)	2013-09-01   -   2017-08-31

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	UNIVERZITA KOMENSKEHO V BRATISLAVE  Organization address address: SAFARIKOVO NAM 6 city: Bratislava 1 postcode: 81499 contact info Titolo: Dr. Nome: Rastislav Cognome: Kralovic Email: send email Telefono: +421 260295470 Fax: +421 2 65427041	SK (Bratislava 1)	coordinator	100˙000.00

Mappa

 Word cloud

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

 Obiettivo del progetto (Objective)

'Methods for systems and software engineering have steadily improved, but are being outrun by rapidly increasing system complexity. Much of this complexity is caused by the increasing parallelism (concurrency) and ubiquity (embeddedness) of systems. In this project, called ConAn (for CONcurrency ANalysis), we focus on design and analysis methods for concurrent software. Concurrent programming is the area of software development where even experts make subtle programming errors. Furthermore, concurrent programs are difficult to debug and test, because their behavior is nondeterministic and therefore irreproducible. We will focus on three specific areas: first, we will develop a verification tool for concurrent data structure implementations. Second, we will leverage the verification models and algorithms to develop synthesis methods for concurrent programs which are correct by construction. Third, we will develop a more quantitative analysis based on a flexible performance model for concurrent programs which is suitable for formal analysis of programs, as well as theory, algorithms and tools based on this model. The model will allow us to make the output of the verification tool more informative and to synthesize concurrent programs with better performance.'